English
Let a be a finite subset of indices and suppose for every i ∈ a the function f_i: α → γ is lower semicontinuous on s. Then the function z ↦ ∑_{i ∈ a} f_i(z) is lower semicontinuous on s.
Русский
Пусть a — конечный индексный набор; если для каждого i ∈ a функция f_i: α → γ является нижней полупрерывной на множестве s, то z ↦ ∑_{i ∈ a} f_i(z) является нижней полупрерывной на s.
LaTeX
$$$\\displaystyle \\Big(\\forall i \\in a\\,,\\ LowerSemicontinuousOn(f_i, s)\\Big) \\Rightarrow LowerSemicontinuousOn\\Big( z \\mapsto \\sum_{i \\in a} f_i(z), s \\Big)$$$
Lean4
theorem lowerSemicontinuousOn_sum {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuousOn (f i) s) :
LowerSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s := fun x hx =>
lowerSemicontinuousWithinAt_sum fun i hi => ha i hi x hx
