Theorem OrderIso.lift_cof_eq

Modification history

2026-03-21 21:50
Mathlib/SetTheory/Cardinal/Cofinality.lean
chore: `OrderIso.cof_eq` → `OrderIso.cof_congr` (#36898) …
Deleted OrderIso.lift_cof_eqView on Github →
2026-03-15 22:43
Mathlib/SetTheory/Cardinal/Cofinality.lean
refactor: redefine `Order.cof` for a preorder (#35513) …
Added OrderIso.lift_cof_eqView on Github →