Commit 2022-04-21 12:09 f1091b38

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.