Commit 2024-09-17 09:07 ae7e4991

View on Github →

feat(SetTheory/Ordinal/Arithmetic): the complement of a small set of ordinals is unbounded (#16875)

Estimated changes

Modified Mathlib/Logic/Small/Set.lean

added theorem small_univ_iff

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Ordinal.not_bddAbove_compl_of_small