# Normal functions #

A normal function between well-orders is a strictly monotonic continuous function. Normal functions arise chiefly in the context of cardinal and ordinal-valued functions.

We opt for an equivalent definition that's both simpler and often more convenient: a normal function is a strictly monotonic function `f` such that at successor limits `a`, `f a` is the least upper bound of `f b` with `b < a`.

## TODO #

- Prove the equivalence with the standard definition (in some other file).
- Replace `Ordinal.IsNormal` by this more general notion.

source
structure Order.IsNormal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) :
Prop

A normal function between well-orders is a strictly monotonic continuous function.

- strictMono : StrictMono f
- mem_lowerBounds_upperBounds_of_isSuccLimit {a : α} (ha : IsSuccLimit a) : f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))

  This condition is the RHS of the `IsLUB (f '' Iio a) (f a)` predicate, which is sufficient since the LHS is implied by monotonicity.

Instances For

source
theorem Order.isNormal_iff' {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) :
IsNormal f ↔ StrictMono f ∧ ∀ {a : α}, IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))
source
theorem Order.isNormal_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} :
IsNormal f ↔ StrictMono f ∧ ∀ (o : α), IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a
source
theorem Order.IsNormal.isLUB_image_Iio_of_isSuccLimit {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : IsNormal f) {a : α} (ha : IsSuccLimit a) :
IsLUB (f '' Set.Iio a) (f a)
source
@[deprecated "use the default constructor of `IsNormal` directly" (since := "2025-07-08")]
theorem Order.IsNormal.of_mem_lowerBounds_upperBounds {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : StrictMono f) (hl : ∀ {a : α}, IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Set.Iio a))) :
IsNormal f
source
theorem Order.IsNormal.le_iff_forall_le {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
f a ≤ b ↔ ∀ a' < a, f a' ≤ b
source
theorem Order.IsNormal.lt_iff_exists_lt {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} :
b < f a ↔ ∃ a' < a, b < f a'
source
theorem Order.IsNormal.map_isSuccLimit {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : IsNormal f) (ha : IsSuccLimit a) :
IsSuccLimit (f a)
source
theorem Order.IsNormal.map_isLUB {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : IsNormal f) {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty) :
IsLUB (f '' s) (f a)
source
theorem InitialSeg.isNormal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsNormal ⇑f
source
theorem PrincipalSeg.isNormal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2) :
Order.IsNormal ⇑f.toRelEmbedding
source
theorem OrderIso.isNormal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ≃o β) :
Order.IsNormal ⇑f
source
theorem Order.IsNormal.id {α : Type u_1} [LinearOrder α] :
IsNormal id
source
theorem Order.IsNormal.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} [LinearOrder α] [LinearOrder β] [LinearOrder γ] (hg : IsNormal g) (hf : IsNormal f) :
IsNormal (g ∘ f)
source
theorem Order.IsNormal.of_succ_lt {α : Type u_1} {β : Type u_2} {f : α → β} [LinearOrder α] [LinearOrder β] [WellFoundedLT α] [SuccOrder α] (hs : ∀ (a : α), f a < f (succ a)) (hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Set.Iio a) (f a)) :
IsNormal f
source
theorem Order.IsNormal.ext {α : Type u_1} {β : Type u_2} {f : α → β} [LinearOrder α] [LinearOrder β] [WellFoundedLT α] [SuccOrder α] [OrderBot α] {g : α → β} (hf : IsNormal f) (hg : IsNormal g) :
f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)
source
theorem Order.IsNormal.map_sSup {α : Type u_1} {β : Type u_2} {f : α → β} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β] (hf : IsNormal f) {s : Set α} (hs : s.Nonempty) (hs' : BddAbove s) :
f (sSup s) = sSup (f '' s)
source
theorem Order.IsNormal.map_iSup {α : Type u_1} {β : Type u_2} {f : α → β} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β] {ι : Sort u_4} [Nonempty ι] {g : ι → α} (hf : IsNormal f) (hg : BddAbove (Set.range g)) :
f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
source
theorem Order.IsNormal.preimage_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β] (hf : IsNormal f) {x : β} (h₁ : (f ⁻¹' Set.Iic x).Nonempty) (h₂ : BddAbove (f ⁻¹' Set.Iic x)) :
f ⁻¹' Set.Iic x = Set.Iic (sSup (f ⁻¹' Set.Iic x))
source
theorem Order.IsNormal.apply_of_isSuccLimit {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [ConditionallyCompleteLinearOrderBot α] [ConditionallyCompleteLinearOrder β] (hf : IsNormal f) (ha : IsSuccLimit a) :
f a = ⨆ (b : ↑(Set.Iio a)), f ↑b