Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 08:21 68033a22

View on Github →

feat(set_theory/ordinal_arithmetic): A set of ordinals is bounded above iff it's small (#11870)

Estimated changes

Modified src/logic/small.lean

added theorem small_subset

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.bdd_above_iff_small

added theorem ordinal.le_sup_shrink_equiv

added theorem ordinal.small_Iio

added theorem ordinal.sup_eq_Sup