Commit 2026-05-10 00:45 175f378e

View on Github →

chore: split SetTheory.Cardinal.Cofinality (#38363) We split this file into a Basic file with only the basic results on Order.cof, and an Ordinal file for the interactions with ordinals. This avoids an import cycle in a subsequent PR. The module docstrings were rewritten, but no theorems were changed.

Estimated changes

added def Order.cof
added theorem Order.cof_eq
added theorem Order.cof_eq_aleph0
added theorem Order.cof_eq_one
added theorem Order.cof_eq_one_iff
added theorem Order.cof_eq_zero
added theorem Order.cof_eq_zero_iff
added theorem Order.cof_le
added theorem Order.cof_le_one_iff
added theorem Order.cof_nat
added theorem Order.cof_ne_one
added theorem Order.cof_ne_one_iff
added theorem Order.cof_ne_zero
added theorem Order.cof_ne_zero_iff
added theorem Order.le_cof_iff
added theorem Order.le_lift_cof_iff
added theorem Order.one_lt_cof
added theorem Order.one_lt_cof_iff
added theorem OrderIso.cof_congr
deleted theorem GaloisConnection.cof_le
deleted theorem Order.aleph0_le_cof_iff
deleted def Order.cof
deleted theorem Order.cof_eq
deleted theorem Order.cof_eq_aleph0
deleted theorem Order.cof_eq_one
deleted theorem Order.cof_eq_one_iff
deleted theorem Order.cof_eq_zero
deleted theorem Order.cof_eq_zero_iff
modified theorem Order.cof_int
deleted theorem Order.cof_le
deleted theorem Order.cof_le_cardinalMk
deleted theorem Order.cof_le_one_iff
deleted theorem Order.cof_lt_aleph0_iff
deleted theorem Order.cof_nat
deleted theorem Order.cof_ne_one
deleted theorem Order.cof_ne_one_iff
deleted theorem Order.cof_ne_zero
deleted theorem Order.cof_ne_zero_iff
deleted theorem Order.le_cof_iff
deleted theorem Order.le_lift_cof_iff
deleted theorem Order.one_lt_cof
deleted theorem Order.one_lt_cof_iff
deleted theorem OrderIso.cof_congr
deleted theorem OrderIso.lift_cof_congr