Fundamental sequences

A fundamental sequence for a countable limit ordinal o is a strictly monotone function ℕ → Iio o with cofinal range. We can generalize this notion to arbitrary ordinals by setting the domain as Iio o.cof.card. Note that for a countable limit ordinal, one has o.cof.card = ω.

Main results

• Ordinal.exists_isFundamentalSeq: every ordinal has a fundamental sequence.

structure Ordinal.IsFundamentalSeq {a o : Ordinal.{u_1}} (f : ↑(Set.Iio a) → ↑(Set.Iio o)) : Prop

A fundamental sequence for o is a strictly monotonic function Iio o.cof.ord → Iio o with cofinal range. We provide a = o.cof.ord explicitly to avoid type rewrites.

• le_ord_cof : a ≤ o.cof.ord

  This condition alongside the others is enough to conclude o.cof.ord = a, see IsFundamentalSeq.ord_cof_eq.

• strictMono : StrictMono f

  A fundamental sequence is strictly monotonic.

• isCofinal_range : IsCofinal (Set.range f)

  A fundamental sequence for o has cofinal range, i.e. its least strict upper bound equals the ordinal o. See IsFundamentalSeq.iSup_add_one_eq and IsFundamentalSeq.iSup_eq.

theorem Ordinal.IsFundamentalSeq.iSup_add_one_eq {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} (hf : IsFundamentalSeq f) : ⨆ (i : ↑(Set.Iio a)), ↑(f i) + 1 = o

theorem Ordinal.IsFundamentalSeq.ord_cof {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} (hf : IsFundamentalSeq f) : o.cof.ord = a

theorem Ordinal.IsFundamentalSeq.iSup_eq {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} (hf : IsFundamentalSeq f) (ha : 1 < a) : ⨆ (i : ↑(Set.Iio a)), ↑(f i) = o

theorem Ordinal.IsFundamentalSeq.id {o : Ordinal.{u_1}} (ho : o ≤ o.cof.ord) : IsFundamentalSeq id

A regular ordinal o has a fundamental sequence given by all smaller ordinals.

theorem Ordinal.IsFundamentalSeq.zero (f : ↑(Set.Iio 0) → ↑(Set.Iio 0)) : IsFundamentalSeq f

The empty function is a fundamental sequence for 0.

theorem Ordinal.IsFundamentalSeq.add_one (o : Ordinal.{u_1}) : IsFundamentalSeq fun (x : ↑(Set.Iio 1)) => ⟨o, ⋯⟩

The length one sequence (o) is a fundamental sequence for o + 1.

theorem Ordinal.IsFundamentalSeq.comp {a b o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : ↑(Set.Iio b) → ↑(Set.Iio a)} (hf : IsFundamentalSeq f) (hg : IsFundamentalSeq g) : IsFundamentalSeq (f ∘ g)

theorem Ordinal.IsFundamentalSeq.comp_isNormal {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)} {g : Ordinal.{u_1} → Ordinal.{u_1}} (hg : Order.IsNormal g) (hf : IsFundamentalSeq f) (ho : Order.IsSuccLimit o) : IsFundamentalSeq fun (i : ↑(Set.Iio a)) => ⟨g ↑(f i), ⋯⟩

If f is a fundamental sequence for a limit ordinal o and g is normal, then g ∘ f is a fundamental sequence for g o.

theorem Ordinal.exists_isFundamentalSeq {a o : Ordinal.{u_1}} (ha : o.cof.ord = a) : ∃ (f : ↑(Set.Iio a) → ↑(Set.Iio o)), IsFundamentalSeq f

Every ordinal has a fundamental sequence.

Deprecated material

@[deprecated Ordinal.IsFundamentalSeq (since := "2026-03-23")]

def Ordinal.IsFundamentalSequence (a o : Ordinal.{u}) (f : (b : Ordinal.{u}) → b < o → Ordinal.{u}) : Prop

A fundamental sequence for a is an increasing sequence of length o = cof a that converges at a. We provide o explicitly in order to avoid type rewrites.

@[deprecated Ordinal.IsFundamentalSeq.ord_cof (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.cof_eq {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : a.cof.ord = o

@[deprecated Ordinal.IsFundamentalSeq.strictMono (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.strict_mono {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {i j : Ordinal.{u}} (hi : i < o) (hj : j < o) : i < j → f i hi < f j hj

@[deprecated Ordinal.IsFundamentalSeq.iSup_add_one_eq (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.blsub_eq {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : o.blsub f = a

@[deprecated Ordinal.IsFundamentalSeq (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.ord_cof {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) : a.IsFundamentalSequence a.cof.ord fun (i : Ordinal.{u}) (hi : i < a.cof.ord) => f i ⋯

@[deprecated Ordinal.IsFundamentalSeq.id (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.id_of_le_cof {o : Ordinal.{u}} (h : o ≤ o.cof.ord) : o.IsFundamentalSequence o fun (a : Ordinal.{u}) (x : a < o) => a

@[deprecated Ordinal.IsFundamentalSeq.zero (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.zero {f : (b : Ordinal.{u_1}) → b < 0 → Ordinal.{u_1}} : IsFundamentalSequence 0 0 f

@[deprecated Ordinal.IsFundamentalSeq.add_one (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.succ {o : Ordinal.{u}} : (Order.succ o).IsFundamentalSequence 1 fun (x : Ordinal.{u}) (x_1 : x < 1) => o

@[deprecated Ordinal.IsFundamentalSeq.strictMono (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.monotone {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {i j : Ordinal.{u}} (hi : i < o) (hj : j < o) (hij : i ≤ j) : f i hi ≤ f j hj

@[deprecated Ordinal.IsFundamentalSeq.comp (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.trans {a o o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hf : a.IsFundamentalSequence o f) {g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}} (hg : o.IsFundamentalSequence o' g) : a.IsFundamentalSequence o' fun (i : Ordinal.{u}) (hi : i < o') => f (g i hi) ⋯

@[deprecated Ordinal.IsFundamentalSeq (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.lt {a o : Ordinal.{u_1}} {s : (p : Ordinal.{u_1}) → p < o → Ordinal.{u_1}} (h : a.IsFundamentalSequence o s) {p : Ordinal.{u_1}} (hp : p < o) : s p hp < a

@[deprecated Ordinal.exists_isFundamentalSeq (since := "2026-03-23")]

theorem Ordinal.exists_fundamental_sequence (a : Ordinal.{u}) : ∃ (f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}), a.IsFundamentalSequence a.cof.ord f

Every ordinal has a fundamental sequence.

@[deprecated Ordinal.IsFundamentalSeq.comp_isNormal (since := "2026-03-23")]

theorem Ordinal.IsFundamentalSequence.of_isNormal {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) {a o : Ordinal.{u}} (ha : Order.IsSuccLimit a) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : a.IsFundamentalSequence o g) : (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) => f (g b hb)

@[deprecated Ordinal.IsFundamentalSequence.of_isNormal (since := "2025-12-25")]

theorem Ordinal.IsNormal.isFundamentalSequence {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) {a o : Ordinal.{u}} (ha : Order.IsSuccLimit a) {g : (b : Ordinal.{u}) → b < o → Ordinal.{u}} (hg : a.IsFundamentalSequence o g) : (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) => f (g b hb)

Alias of Ordinal.IsFundamentalSequence.of_isNormal.