Commit 2025-08-20 18:51 f0454a43

View on Github →

feat: aleph and beth are normal functions (#27015) By using Order.IsNormal, we can state (and use!) these results directly, instead of having to go through ord.

Estimated changes

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem ciInf_Ici

added theorem ciSup_Iic

Modified Mathlib/Order/IsNormal.lean

added theorem Order.IsNormal.apply_of_isSuccLimit

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

modified theorem Cardinal.aleph_limit

modified theorem Cardinal.beth_limit

added theorem Cardinal.isNormal_aleph

modified theorem Cardinal.isNormal_beth

added theorem Cardinal.isNormal_preAleph

modified theorem Cardinal.isNormal_preBeth