Theorem RelIso.cof_eq_lift

Modification history

2026-03-15 22:43
Mathlib/SetTheory/Cardinal/Cofinality.lean
refactor: redefine `Order.cof` for a preorder (#35513) …
Deleted RelIso.cof_eq_liftView on Github →
2026-01-09 08:53
Mathlib/SetTheory/Cardinal/Cofinality.lean
chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)
Modified RelIso.cof_eq_liftView on Github →
2024-11-17 07:50
Mathlib/SetTheory/Cardinal/Cofinality.lean
chore(SetTheory/Cardinal/Cofinality): golf `lift_cof` (#18047) …
Modified RelIso.cof_eq_liftView on Github →
2023-02-24 13:27
Mathlib/SetTheory/Cardinal/Cofinality.lean
feat port: SetTheory.Cardinal.Cofinality (#2479)
Added RelIso.cof_eq_liftView on Github →