English
The finite sum of a family of lower semicontinuous functions is lower semicontinuous.
Русский
Конечная сумма семейства функций с нижней полупрерывностью сохраняет её.
LaTeX
$$$\\forall a: Finset\\;\\forall i \\in a, \\text{LowerSemicontinuous } (f i) \\Rightarrow \\text{LowerSemicontinuous } (\\sum i∈a, f i)$$$
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 : LowerSemicontinuous f) (hg : LowerSemicontinuous g)
(hcont : ∀ x, ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) : LowerSemicontinuous fun z => f z + g z :=
fun x => (hf x).add' (hg x) (hcont x)
