English
If f and g are USCOn on s, their sum is USCOn on s when addition is continuous.
Русский
Если f и g — USCOn на s, то их сумма — USCOn на s при непрерывном сложении.
LaTeX
$$$hf : UpperSemicontinuousOn f s,\\ hg : UpperSemicontinuousOn g s\\Rightarrow\\; UpperSemicontinuousOn (\\lambda z => f z + g z) s$$$
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 : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s) :
UpperSemicontinuousOn (fun z => f z + g z) s :=
hf.add' hg fun _x _hx => continuous_add.continuousAt
