English
Let x be a point in the domain. Suppose a is a finite index set and for every i in a the function f_i: α → γ is lower semicontinuous at x. Then the function z ↦ ∑_{i ∈ a} f_i(z) is lower semicontinuous at x.
Русский
Пусть x — точка области определения. Пусть a — конечный индексный набор, и для каждого i ∈ a функция f_i: α → γ является нижней полупрерывной в точке x. Тогда функция z ↦ ∑_{i ∈ a} f_i(z) ниже по полупрерывности в x.
LaTeX
$$$\\displaystyle \\Big(\\forall i \\in a\\,,\\ \\text{LowerSemicontinuousAt}(f_i,x)\\Big) \\Rightarrow \\text{LowerSemicontinuousAt}\\Big( z \\mapsto \\sum_{i \\in a} f_i(z) , x \\Big)$$$
Lean4
theorem lowerSemicontinuousAt_sum {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousAt (f i) x) :
LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x :=
by
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
exact lowerSemicontinuousWithinAt_sum ha
