theorem Cardinal.mk_bUnion_le' {ι : Type u} {α : Type u} (s : Set ι) (f : (i : ι) → i ∈ s → Set α) : Cardinal.mk ↑(⋃ (i : ι), ⋃ (hi : i ∈ s), f i hi) ≤ Cardinal.mk ↑s * ⨆ (i : ↑s), Cardinal.mk ↑(f ↑i ⋯)

theorem Cardinal.nonempty_compl_of_mk_lt_mk {α : Type u} {s : Set α} (h : Cardinal.mk ↑s < Cardinal.mk α) : sᶜ.Nonempty