Commit 2026-06-03 11:16 cadd9146

View on Github →

feat: a cofinal set has a cofinal subset of order type (cof α).ord (#39789)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

added theorem Order.cof_eq_of_isCofinal

Modified Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

modified theorem Ordinal.exists_ord_cof_eq

added theorem Ordinal.exists_ord_cof_eq_of_isCofinal

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem OrderIso.ordinalType_congr

added theorem RelIso.ordinalType_congr

deleted theorem RelIso.ordinal_type_eq