Theorems · Theorem · logic and foundations
Ordinal.lift_cof_iSup_add_one
∀ {β : Type v} [inst : LinearOrder β] [Small.{u, v} β] {f : β → Ordinal.{u}},
StrictMono f → Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)- Cited by
- 4 results in Mathlib
- Foundations
- Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrderSmall
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- Set.Elemproof · cited by 7,166
- Set.rangeproof · cited by 4,705
- Cardinalstatement and proof · cited by 2,598
- iSupstatement and proof · cited by 2,415
- Ordinalstatement and proof · cited by 1,688
- Set.Iioproof · cited by 1,166
- StrictMonostatement and proof · cited by 706
- LT.lt.trans_leproof · cited by 678
- Cardinal.liftstatement and proof · cited by 583
- Smallstatement and proof · cited by 369
- Set.mem_range_selfproof · cited by 328
Cited by4
Results whose statement or proof uses this declaration.
- Ordinal.sSup_add_one_lt_of_lt_cofproof · cited by 2
- Ordinal.cof_iSup_Iio_add_oneproof · cited by 2
- Ordinal.lift_cof_iSupproof · cited by 1
- Ordinal.cof_iSup_add_oneproof · cited by 0