Theorem Ordinal.cof_type_lt

Modification history

2026-03-15 22:43
Mathlib/SetTheory/Cardinal/Cofinality.lean
refactor: redefine `Order.cof` for a preorder (#35513) …
Deleted Ordinal.cof_type_ltView on Github →
2024-11-12 03:03
Mathlib/SetTheory/Cardinal/Cofinality.lean
refactor(SetTheory/Cardinal/Cofinality): deprecate `StrictOrder.cof` (#18043) …
Added Ordinal.cof_type_ltView on Github →