Theorems · Theorem · logic and foundations
Ordinal.ord_cof_eq
Deprecated since 2026-05-25Use Ordinal.exists_ord_cof_eq instead.
∀ (α : Type u) [inst : LinearOrder α] [inst_1 : WellFoundedLT α], ∃ s, IsCofinal s ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
Alias of Ordinal.exists_ord_cof_eq.
Every well-order has a cofinal subset of order type (cof α).ord.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrderWellFoundedLT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- LinearOrderstatement · cited by 8,572
- Set.Elemstatement · cited by 7,166
- Ordinalstatement · cited by 1,688
- WellFoundedLTstatement · cited by 491
- Cardinal.ordstatement · cited by 266
- Ordinal.typestatement · cited by 207
- IsWellOrderstatement · cited by 171
- Order.cofstatement · cited by 86
- IsCofinalstatement · cited by 84
- Ordinal.exists_ord_cof_eqproof · cited by 5
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.