lowerSemicontinuousAt_tsum — Mathlib

English

If each f_i is LowerSemicontinuous (f_i), then the sum tsum_i f_i is LowerSemicontinuous.

Русский

Если каждая f_i лс, то tsum_i f_i лс.

LaTeX

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

Lean4

theorem lowerSemicontinuousAt_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ∑' i, f i x') x :=
  by
  simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *
  exact lowerSemicontinuousWithinAt_tsum h

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