Commit 2026-03-23 01:32 f699e797

View on Github →

feat: cof α < ℵ₀ ↔ cof α ≤ 1 (#36976)

Estimated changes

Modified Mathlib/Order/Preorder/Finite.lean

added theorem Set.Finite.exists_subsingleton_isCofinal

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.le_one_iff

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Order.aleph0_le_cof_iff

added theorem Order.cof_le_one_iff

added theorem Order.cof_lt_aleph0_iff

added theorem Order.cof_ne_one

added theorem Order.cof_ne_one_iff

added theorem Order.one_lt_cof

added theorem Order.one_lt_cof_iff

added theorem Ordinal.aleph0_le_cof_iff

added theorem Ordinal.cof_lt_aleph0_iff

modified theorem Ordinal.cof_omega0

added theorem Ordinal.one_lt_cof_iff

Modified Mathlib/SetTheory/Cardinal/Regular.lean

modified theorem Cardinal.isRegular_cof