α : Type u_2
β : Type ?u.285208
γ : Type ?u.285211
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
ι : Type u_1
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ (∑' (x : ↑(⋃ (i : ι), t i)), f ↑x) ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
α : Type u_2
β : Type ?u.285208
γ : Type ?u.285211
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
ι : Type u_1
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ (∑' (x : ↑(⋃ (i : ι), t i)), f ↑x) ≤ ∑ i : ι, ∑' (x : ↑(t i)), f ↑x
rw [← tsum_fintype]
no goals
α : Type u_2
β : Type ?u.285208
γ : Type ?u.285211
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f✝ g : α → ℝ≥0∞
ι : Type u_1
inst✝ : Fintype ι
f : α → ℝ≥0∞
t : ι → Set α
⊢ (∑' (x : ↑(⋃ (i : ι), t i)), f ↑x) ≤ ∑' (b : ι) (x : ↑(t b)), f ↑x
exact tsum_iUnion_le_tsum f t