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.IsNormalby this more general notion.
structure
Order.IsNormal
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[LinearOrder β]
(f : α → β)
:
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
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 : α → β}
:
theorem
Order.IsNormal.isLUB_image_Iio_of_isSuccLimit
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[LinearOrder β]
{f : α → β}
(hf : IsNormal f)
{a : α}
(ha : IsSuccLimit a)
:
@[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
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 : β}
:
theorem
Order.IsNormal.lt_iff_exists_lt
{α : Type u_1}
{β : Type u_2}
{a : α}
{f : α → β}
[LinearOrder α]
[LinearOrder β]
(hf : IsNormal f)
(ha : IsSuccLimit a)
{b : β}
:
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)
:
theorem
InitialSeg.isNormal
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[LinearOrder β]
(f : InitialSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2)
:
theorem
PrincipalSeg.isNormal
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[LinearOrder β]
(f : PrincipalSeg (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2)
:
theorem
OrderIso.isNormal
{α : Type u_1}
{β : Type u_2}
[LinearOrder α]
[LinearOrder β]
(f : α ≃o β)
:
theorem
Order.IsNormal.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β}
{g : β → γ}
[LinearOrder α]
[LinearOrder β]
[LinearOrder γ]
(hg : IsNormal g)
(hf : IsNormal 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)
:
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))
: