Theorems · Theorem · logic and foundations

Ordinal.IsFundamentalSeq.isCofinal_range

∀ {a o : Ordinal.{u_1}} {f : ↑(Set.Iio a) → ↑(Set.Iio o)}, Ordinal.IsFundamentalSeq f → 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.

Defined in: Mathlib.SetTheory.Ordinal.FundamentalSequence
Cited by: 3 results in Mathlib
Foundations: Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
Set.Elemstatement and proof · cited by 7,166
Set.rangestatement · cited by 4,705
Ordinalstatement and proof · cited by 1,688
Set.Iiostatement and proof · cited by 1,166
IsCofinalstatement · cited by 84
Ordinal.IsFundamentalSeqstatement and proof · cited by 13

Cited by3

Results whose statement or proof uses this declaration.

Ordinal.IsFundamentalSeq.iSup_add_one_eqproof · cited by 3
Ordinal.IsFundamentalSeq.compproof · cited by 0
Ordinal.IsFundamentalSeq.comp_isNormalproof · cited by 0