English
The sum of two lower semicontinuous functions on a set s is lower semicontinuous on s.
Русский
Сумма двух функций в рамках множества s — нижняя полупрерывность на s.
LaTeX
$$$\\text{LowerSemicontinuousWithinAt } f s x \\land \\text{LowerSemicontinuousWithinAt } g s x \\Rightarrow \\text{LowerSemicontinuousWithinAt } (f+g) s x$$$
Lean4
/-- The sum of two lower semicontinuous functions is lower 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 : LowerSemicontinuousOn f s) (hg : LowerSemicontinuousOn g s)
(hcont : ∀ x ∈ s, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
LowerSemicontinuousOn (fun z => f z + g z) s := fun x hx => (hf x hx).add' (hg x hx) (hcont x hx)
