Commit 2026-03-20 14:17 ad8b1b5f

View on Github →

feat: cof α = cof β given a strictly monotonic function f : α → β with cofinal range (#36703) We use this to prove cof (f a) = cof a for a normal function f, without having to go through the bespoke fundamental sequence API.

Estimated changes

Modified Mathlib/Order/IsNormal.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Order.cof_congr_of_strictMono

modified theorem Order.le_cof_iff

added theorem Order.le_lift_cof_iff

added theorem Order.lift_cof_congr_of_strictMono

added theorem Ordinal.cof_Iio

deleted theorem Ordinal.cof_eq_of_isNormal

added theorem Ordinal.cof_iSup_Iio

deleted theorem Ordinal.cof_le_of_isNormal

added theorem Ordinal.cof_map_of_isNormal

modified theorem Ordinal.cof_ord_le

added theorem Ordinal.le_cof_map_of_isNormal