α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : (#↑s) < (#α)
⊢ (#↑s) + (#↑(sᶜ)) = (#α)
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : (#↑s) < (#α)
⊢ (#↑(sᶜ)) = (#α)
refine' eq_of_add_eq_of_aleph0_le _ h2 (aleph0_le_mk α)
no goals
α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : (#↑s) < (#α)
⊢ (#↑s) + (#↑(sᶜ)) = (#α)
exact mk_sum_compl s