add — Mathlib

English

The sum over a finite set of lower semicontinuous functions is lower semicontinuous.

Русский

Сумма по конечному набору функций лс сохраняется.

LaTeX

$$$\\forall f: Finset \\\\; (hf)\\; \\\\Rightarrow \\\\LowerSemicontinuousWithinAt(\\\\sum i ∈ a, f i)$$$

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

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