English
The sum of two upper semicontinuous functions is upper semicontinuous within a set, given a continuous addition map.
Русский
Сумма двух верхних полупрерывных функций является верхней полупрерывной внутри множества при непрерывности сложения.
LaTeX
$$$hf : UpperSemicontinuousWithinAt f s x,\\ hg : UpperSemicontinuousWithinAt g s x\\Rightarrow\\; \\text{UpperSemicontinuousWithinAt } (\\lambda z => f z + g z) s x$$$
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 : UpperSemicontinuousAt f x) (hg : UpperSemicontinuousAt g x)
(hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) : UpperSemicontinuousAt (fun z => f z + g z) x :=
by
simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
exact hf.add' hg hcont
