α✝ β ι α : Type u
A : ι → Set α
s : Set ι
⊢ (#↑(⋃ (x : ↑s), A ↑x)) ≤ (#↑s) * ⨆ (x : ↑s), #↑(A ↑x)
α✝ β ι α : Type u
A : ι → Set α
s : Set ι
⊢ (#↑(⋃ (x : ι) (_ : x ∈ s), A x)) ≤ (#↑s) * ⨆ (x : ↑s), #↑(A ↑x)
rw [biUnion_eq_iUnion]
no goals
α✝ β ι α : Type u
A : ι → Set α
s : Set ι
⊢ (#↑(⋃ (x : ↑s), A ↑x)) ≤ (#↑s) * ⨆ (x : ↑s), #↑(A ↑x)
apply mk_iUnion_le