English
If f and g are USCOn on s, then their pointwise sum is USCOn on s, given continuous addition.
Русский
Если f и g — USCOn на s, то их точечная сумма — тоже USCOn на s при непрерывном сложении.
LaTeX
$$$hf : UpperSemicontinuousOn f s,\\ hg : UpperSemicontinuousOn g s\\Rightarrow\\; \\text{UpperSemicontinuousOn } (\\lambda z => f z + g z) s$$$
Lean4
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`. -/
theorem add' {f g : α → γ} (hf : UpperSemicontinuous f) (hg : UpperSemicontinuous g)
(hcont : ∀ x, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) : UpperSemicontinuous fun z => f z + g z :=
fun x => (hf x).add' (hg x) (hcont x)
