English
Let f_i be USCAt at x for all i in a finite index set a. Then the sum over i in a of f_i is USCAt x.
Русский
Пусть f_i имеют верхнюю полупрерывность в x для i из конечного множества a. Тогда сумма по i в a функций f_i имеет верхнюю полупрерывность в x.
LaTeX
$$$ha : \\forall i, i\\in a \\Rightarrow UpperSemicontinuousAt (f i) x\\Rightarrow\\; UpperSemicontinuousAt (\\lambda z => \\sum_{i\\in a} f i z) x$$$
Lean4
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`. -/
theorem add {f g : α → γ} (hf : UpperSemicontinuousAt f x) (hg : UpperSemicontinuousAt g x) :
UpperSemicontinuousAt (fun z => f z + g z) x :=
hf.add' hg continuous_add.continuousAt
