English
Let f_i : α → γ be functions for i in a finite index set, and suppose each f_i is upper semicontinuous. Then the function z ↦ ∑_{i∈a} f_i(z) is upper semicontinuous.
Русский
Пусть f_i : α → γ для i из конечного множества индексов. Если каждый f_i верхнеполупрерывен, то z ↦ ∑_{i∈a} f_i(z) верхнеполупрерывна.
LaTeX
$$$$\\left(\\forall i \\in a,\\ \\operatorname{UpperSemicontinuous}(f_i)\\right) \\Rightarrow \\operatorname{UpperSemicontinuous}\\left(z \\mapsto \\sum_{i \\in a} f_i(z)\\right).$$$$
Lean4
theorem upperSemicontinuous_sum {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuous (f i)) :
UpperSemicontinuous fun z => ∑ i ∈ a, f i z := fun x => upperSemicontinuousAt_sum fun i hi => ha i hi x
