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.

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
• isLUB_image_Iio_of_isSuccLimit {a : α} (ha : IsSuccLimit a) : IsLUB (f '' Set.Iio a) (f a)

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

This condition is the LHS of the IsLUB (f '' Iio a) (f a) predicate.

theorem Order.IsNormal.of_succ_lt {α : Type u_1} {β : Type u_2} {f : α → β} [LinearOrder α] [LinearOrder β] [SuccOrder α] [WellFoundedLT α] (hs : ∀ (a : α), f a < f (succ a)) (hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Set.Iio a) (f a)) : IsNormal f

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