lowerSemicontinuous_tsum — Mathlib

English

Let f_i: α → ℝ≥0∞ be such that each is LowerSemicontinuous (f_i). Then the tsum f_i is LowerSemicontinuous.

Русский

Пусть f_i: α → ℝ≥0∞ лм. Тогда tsum f_i лс.

LaTeX

$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuous(f_i)\\Big) \\Rightarrow \\ LowerSemicontinuous\\Big( x \\mapsto \\sum_i f_i(x) \\Big)$$$

Lean4

theorem lowerSemicontinuous_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuous (f i)) :
    LowerSemicontinuous fun x' => ∑' i, f i x' := fun x => lowerSemicontinuousAt_tsum fun i => h i x

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