∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, LowerSemicontinuousAt (f i) x) → LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x