α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.107722
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) univ x
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.107722
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun z => ∑ i in a, f i z) x
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
no goals
α : Type u_2
inst✝⁵ : TopologicalSpace α
β : Type ?u.107722
inst✝⁴ : Preorder β
f✝ g : α → β
x : α
s t : Set α
y z : β
ι : Type u_1
γ : Type u_3
inst✝³ : LinearOrderedAddCommMonoid γ
inst✝² : TopologicalSpace γ
inst✝¹ : OrderTopology γ
inst✝ : ContinuousAdd γ
f : ι → α → γ
a : Finset ι
ha : ∀ (i : ι), i ∈ a → LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun z => ∑ i in a, f i z) univ x
exact lowerSemicontinuousWithinAt_sum ha