English
Let f_i : α → γ be finitely many functions indexed by i in a finite set a. If each f_i is upper semicontinuous on s, then the finite sum z ↦ ∑_{i∈a} f_i(z) is upper semicontinuous on s.
Русский
Пусть f_i : α → γ для конечного множества индексов i∈a. Если каждый f_i является верхней полупрерывной на s, то сумма z ↦ ∑_{i∈a} f_i(z) также верхнеполупрерывна на s.
LaTeX
$$$$\\left(\\forall i \\in a,\\ \\operatorname{UpperSemicontinuousOn}(f_i, s)\\right) \\Rightarrow \\operatorname{UpperSemicontinuousOn}\\left(z \\mapsto \\sum_{i \\in a} f_i(z), s\\right)$$$$
Lean4
theorem upperSemicontinuousOn_sum {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s) :
UpperSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s := fun x hx =>
upperSemicontinuousWithinAt_sum fun i hi => ha i hi x hx
