mathlib3

f1091b38 - feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373)

feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373) We move `mk_subtype_le` and `mk_set_le` earlier within the file in order to better accomodate for the new result, `bdd_above_iff_small`. We need this result right above the `Sup` stuff, as we'll make heavy use of it in a following refactor for `cardinal.sup`.