Theorems · Inductive type · logic and foundations
Ordinal.IsFundamentalSeq
{a o : Ordinal.{u_1}} → (↑(Set.Iio a) → ↑(Set.Iio o)) → PropA 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.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by15
Results whose statement or proof uses this declaration.
- Cardinal.isRegular_succproof · cited by 6
- Ordinal.IsFundamentalSeq.strictMonostatement and proof · cited by 4
- Ordinal.IsFundamentalSeq.iSup_add_one_eqstatement and proof · cited by 3
- Ordinal.IsFundamentalSeq.isCofinal_rangestatement and proof · cited by 3
- Ordinal.IsFundamentalSeq.ord_cofstatement and proof · cited by 3
- Ordinal.IsFundamentalSeq.le_ord_cofstatement and proof · cited by 1
- Ordinal.exists_isFundamentalSeqstatement · cited by 1
- Ordinal.IsFundamentalSeq.add_onestatement · cited by 0
- Ordinal.IsFundamentalSeq.casesOnstatement and proof · cited by 0
- Ordinal.IsFundamentalSeq.compstatement and proof · cited by 0
- Ordinal.IsFundamentalSeq.comp_isNormalstatement and proof · cited by 0
- Ordinal.IsFundamentalSeq.iSup_eqstatement and proof · cited by 0