Commit 2022-05-30 17:48 ba22440f

View on Github →

feat(set_theory/cardinal/cofinality): use bounded and unbounded (#14438) We change ∀ a, ∃ b ∈ s, ¬ r b a to its def-eq predicate unbounded r s, and similarly for bounded r s.

Estimated changes

Modified src/set_theory/cardinal/cofinality.lean

modified theorem ordinal.cof_eq

modified theorem ordinal.cof_type_le

modified theorem ordinal.le_cof_type

modified theorem ordinal.lt_cof_type