α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.131928
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (s : Finset ι), ∑ i in s, f i x') s x
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.131928
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') s x
simp_rw [ENNReal.tsum_eq_iSup_sum]
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.131928
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (fun x' => ∑ i in b, f i x') s x
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.131928
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ (s : Finset ι), ∑ i in s, f i x') s x
refine lowerSemicontinuousWithinAt_iSup fun b => ?_
no goals
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.131928
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
b : Finset ι
⊢ LowerSemicontinuousWithinAt (fun x' => ∑ i in b, f i x') s x
exact lowerSemicontinuousWithinAt_sum fun i _hi => h i