English
If f and g are upper semicontinuous within s at x, and the map (u,v) ↦ u+v is continuous at (f x, g x), then z ↦ f(z)+g(z) is upper semicontinuous within s at x.
Русский
Если f и g имеют верхнюю полупрерывность внутри s в x, и сумма в γ×γ непрерывна в (f x, g x), то z↦f(z)+g(z) имеет верхнюю полупрерывность внутри s в x.
LaTeX
$$$hf : UpperSemicontinuousWithinAt f s x,\\ hg : UpperSemicontinuousWithinAt g s x,\\ hcont : ContinuousAt (\\lambda p: γ×γ => p.1 + p.2) (f x, g 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 : UpperSemicontinuousWithinAt f s x) (hg : UpperSemicontinuousWithinAt g s x)
(hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
UpperSemicontinuousWithinAt (fun z => f z + g z) s x :=
LowerSemicontinuousWithinAt.add' (γ := γᵒᵈ) hf hg hcont
