lowerSemicontinuous_sum — Mathlib

English

Let f_i: α → γ be defined for i in ι, and a finite set a ⊆ ι. If each f_i is lower semicontinuous, then the function z ↦ ∑_{i ∈ a} f_i(z) is lower semicontinuous.

Русский

Пусть f_i: α → γ определены для i из ι, а a ⊆ ι конечно. Если каждая f_i ниже полупрерывна, то z ↦ ∑_{i ∈ a} f_i(z) ниже полупрерывна.

LaTeX

$$$\\displaystyle \\Big(\\forall i,\\ \\text{LowerSemicontinuous}(f_i)\\Big) \\Rightarrow \\text{LowerSemicontinuous}\\Big( z \\mapsto \\sum_{i} f_i(z) \\Big)$$$

Lean4

theorem lowerSemicontinuous_sum {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, LowerSemicontinuous (f i)) :
    LowerSemicontinuous fun z => ∑ i ∈ a, f i z := fun x => lowerSemicontinuousAt_sum fun i hi => ha i hi x

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