English
If hf and hg are lower semicontinuous, then their sum is lower semicontinuous.
Русский
Если hf и hg — нижние полупрерывные, сумма также нижняя полупрерывная.
LaTeX
$$$\\text{LowerSemicontinuous } f \\Rightarrow \\text{LowerSemicontinuous } g \\Rightarrow \\text{LowerSemicontinuous } (f+g)$$$
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 : LowerSemicontinuousAt f x) (hg : LowerSemicontinuousAt g x)
(hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) : LowerSemicontinuousAt (fun z => f z + g z) x :=
by
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
exact hf.add' hg hcont
