English
The finite sum of lower semicontinuous functions is lower semicontinuous (primed with ContinuousAdd).
Русский
Конечная сумма лс-функций — лс (с непрерывным сложением).
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
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`. -/
theorem add {f g : α → γ} (hf : LowerSemicontinuousOn f s) (hg : LowerSemicontinuousOn g s) :
LowerSemicontinuousOn (fun z => f z + g z) s :=
hf.add' hg fun _x _hx => continuous_add.continuousAt
