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.

See Order.isNormal_iff_strictMono_and_continuous for a proof that these notions are equivalent.

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.

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))

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

theorem Order.IsNormal.monotone {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : IsNormal f) : Monotone f

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)

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

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'

theorem Order.IsNormal.map_isSuccLimit {α : Type u_1} {β : Type u_2} {a : α} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : IsNormal f) (ha : IsSuccLimit a) : IsSuccLimit (f a)

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)

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

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

theorem OrderIso.isNormal {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α ≃o β) : Order.IsNormal ⇑f

theorem Order.IsNormal.id {α : Type u_1} [LinearOrder α] : IsNormal id

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)

theorem Order.IsNormal.to_Iio {α : Type u_1} {β : Type u_2} {f : α → β} [LinearOrder α] [LinearOrder β] (hf : IsNormal f) (a : α) : IsNormal fun (x : ↑(Set.Iio a)) => ⟨f ↑x, ⋯⟩

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

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)

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)

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)

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))

theorem Order.IsNormal.le_iff_le_sSup {α : Type u_1} {β : Type u_2} {f : α → β} [ConditionallyCompleteLinearOrder α] [ConditionallyCompleteLinearOrder β] (hf : IsNormal f) {x : α} {y : β} (h₁ : (f ⁻¹' Set.Iic y).Nonempty) (h₂ : BddAbove (f ⁻¹' Set.Iic y)) : f x ≤ y ↔ x ≤ sSup (f ⁻¹' Set.Iic y)

theorem Order.IsNormal.le_iff_le_sSup' {α : Type u_1} [ConditionallyCompleteLinearOrder α] [WellFoundedLT α] {f : α → α} (hf : IsNormal f) {x y : α} (h : (f ⁻¹' Set.Iic y).Nonempty) : f x ≤ y ↔ x ≤ sSup (f ⁻¹' Set.Iic y)

If f : α → α in a well-order, we can infer one of the hypotheses in Order.IsNormal.le_iff_le_sSup.

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