mathlib

fc09f947 - feat(set_theory): define `ω₁` and prove new lemma on cardinality of `Union`

feat(set_theory): define `ω₁` and prove new lemma on cardinality of `Union` I define `ω₁` as an ordinal (not as an `out`, cf. `measure_theory.card_measurable_space`). I prove a pair of lemmas using its cofinality. I add a lemma on the cardinality of ordinal-indexed `Union`s in preparation for material on the Borel hierarchy.