mathlib3

709a3b70 - feat(set_theory/cardinal_ordinal): `#(list α) ≤ max ω (#α)` (#12519)