Commit 2026-04-05 02:27 74df9fa9

View on Github →

chore(SetTheory/Cardinal/Cofinality): deprecate many lemmas on lsub/blsub (#36940) The intention is to get rid of Ordinal.lsub and Ordinal.blsub entirely, see #17033.

Estimated changes

Modified Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Modified Mathlib/Order/Filter/Cocardinal.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Ordinal.cof_lsub_le

deleted theorem Ordinal.iSup_lt

deleted theorem Ordinal.iSup_lt_ord

Modified Mathlib/SetTheory/Cardinal/Pigeonhole.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean