theorem Set.encard_iUnion_of_pairwiseDisjoint {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : univ.PairwiseDisjoint s) : (⋃ (i : ι), s i).encard = ∑' (i : ι), (s i).encard