α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (⨆ (s : Finset α), ∑ a in s, f a) = ⨆ (i : ι), ∑ a in s i, f a
α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (∑' (a : α), f a) = ⨆ (i : ι), ∑ a in s i, f a
rw [ENNReal.tsum_eq_iSup_sum]
α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (⨆ (i : ι), ∑ a in s i, f a) = ⨆ (s : Finset α), ∑ a in s, f a
α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (⨆ (s : Finset α), ∑ a in s, f a) = ⨆ (i : ι), ∑ a in s i, f a
symm
α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (⨆ (i : ι), (fun t => ∑ a in t, f a) (s i)) = ⨆ (s : Finset α), ∑ a in s, f a
α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (⨆ (i : ι), ∑ a in s i, f a) = ⨆ (s : Finset α), ∑ a in s, f a
change (⨆ i : ι, (fun t : Finset α => ∑ a in t, f a) (s i)) = ⨆ s : Finset α, ∑ a in s, f a
no goals
α : Type u_2
β : Type ?u.234540
γ : Type ?u.234543
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s✝ : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ (⨆ (i : ι), (fun t => ∑ a in t, f a) (s i)) = ⨆ (s : Finset α), ∑ a in s, f a
exact (Finset.sum_mono_set f).iSup_comp_eq hs