English
If f and g are lower semicontinuous, then their pointwise sum is lower semicontinuous.
Русский
Если f и g лс, то их точечная сумма лс.
LaTeX
$$$\\text{LowerSemicontinuous } f \\land \\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 : LowerSemicontinuous f) (hg : LowerSemicontinuous g) :
LowerSemicontinuous fun z => f z + g z :=
hf.add' hg fun _x => continuous_add.continuousAt
