lowerSemicontinuousWithinAt_tsum — Mathlib

English

Let f_i: α → ℝ≥0∞. If each f_i is LowerSemicontinuousWithinAt (f_i) s x, then the series tsum_i f_i(x) is LowerSemicontinuousWithinAt at x on s.

Русский

Пусть f_i: α → ℝ≥0∞. Если для каждого i f_i лс внутри s в x, то tsum_i f_i(x) лс в x на s.

LaTeX

$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuousWithinAt(f_i,s,x)\\Big) \\Rightarrow \\ LowerSemicontinuousWithinAt\\Big( x' \\mapsto \\sum_{i} f_i(x') , s \\Big)\\; x$$$

Lean4

theorem lowerSemicontinuousWithinAt_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ∑' i, f i x') s x :=
  by
  simp_rw [ENNReal.tsum_eq_iSup_sum]
  refine lowerSemicontinuousWithinAt_iSup fun b => ?_
  exact lowerSemicontinuousWithinAt_sum fun i _hi => h i

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