add — Mathlib

English

The sum of two lower semicontinuous functions is lower semicontinuous.

Русский

Сумма двух лс-функций остаётся лс.

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 : LowerSemicontinuousAt f x) (hg : LowerSemicontinuousAt g x) :
    LowerSemicontinuousAt (fun z => f z + g z) x :=
  hf.add' hg continuous_add.continuousAt

Похожие утверждения