English
Sum of two upper semicontinuous_on functions is upper semicontinuous_on, assuming continuous addition.
Русский
Сумма двух функций с верхней полупрерывностью на множествах сохраняет свойство верхней полупрерывности на множестве при непрерывном сложении.
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 : UpperSemicontinuousOn f s) (hg : UpperSemicontinuousOn g s)
(hcont : ∀ x ∈ s, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
UpperSemicontinuousOn (fun z => f z + g z) s := fun x hx => (hf x hx).add' (hg x hx) (hcont x hx)
