α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.133405
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') univ x
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.133405
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' => ∑' (i : ι), f i x') x
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
no goals
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type ?u.133405
inst✝ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_2
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ∑' (i : ι), f i x') univ x
exact lowerSemicontinuousWithinAt_tsum h