Commit 2026-03-17 22:36 f04df228

View on Github →

feat(SetTheory/Ordinal/Basic): the #s-th element of α is an upper-bound for the set's mex (#36539) This is a translation of card_typein_min_le_mk to be in terms of α.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.compl_ssubset_univ

modified theorem Set.not_top_subset

added theorem Set.not_univ_subset

added theorem Set.ssubset_univ_iff_nonempty_compl

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.not_lt_enum_ord_mk_min_compl

added theorem Ordinal.ord_mk_le_type

added theorem Ordinal.ord_mk_lt_type

modified theorem Ordinal.type_fintype