Commit 2024-11-17 07:50 59e75948

View on Github →

chore(SetTheory/Cardinal/Cofinality): golf lift_cof (#18047) We also drop some redundant TC assumptions in RelIso.cof_eq_lift and RelIso.cof_eq.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Order.le_cof

modified theorem RelIso.cof_eq

modified theorem RelIso.cof_eq_lift

modified theorem RelIso.cof_le

deleted theorem RelIso.cof_le_lift