English
Let f i : α → γ be USCWithinAt on s at x for all i in a finite set a. Then the sum over i in a of f i is USCWithinAt on s at x.
Русский
Пусть для каждого i из конечного множества a функция f i: α → γ имеет верхнюю полупрерывность внутри s в x. Тогда сумма по i в a функций f i имеет верхнюю полупрерывность внутри s в x.
LaTeX
$$$ha : \\forall i \\in a, UpperSemicontinuousWithinAt (f i) s x\\Rightarrow\\; UpperSemicontinuousWithinAt (\\lambda z => \\sum_{i\\in a} f i z) s 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 : UpperSemicontinuousWithinAt f s x) (hg : UpperSemicontinuousWithinAt g s x) :
UpperSemicontinuousWithinAt (fun z => f z + g z) s x :=
hf.add' hg continuous_add.continuousAt
