α✝ β α : Type u
A : Set (Set α)
⊢ (#↑(⋃ (i : ↑A), ↑i)) ≤ (#↑A) * ⨆ (s : ↑A), #↑↑s
α✝ β α : Type u
A : Set (Set α)
⊢ (#↑(⋃₀ A)) ≤ (#↑A) * ⨆ (s : ↑A), #↑↑s
rw [sUnion_eq_iUnion]
no goals
α✝ β α : Type u
A : Set (Set α)
⊢ (#↑(⋃ (i : ↑A), ↑i)) ≤ (#↑A) * ⨆ (s : ↑A), #↑↑s
apply mk_iUnion_le