lowerSemicontinuousOn_tsum — Mathlib

English

Let f_i: α → ℝ≥0∞ be defined on s. If each f_i is LowerSemicontinuousOn (f_i) s, then tsum_i f_i is LowerSemicontinuousOn (f) s.

Русский

Пусть f_i: α → ℝ≥0∞ определены на s. Если каждая f_i лс на s, то tsum_i f_i лс на s.

LaTeX

$$$\\displaystyle \\Big(\\forall i,\\ LowerSemicontinuousOn(f_i,s)\\Big) \\Rightarrow \\ LowerSemicontinuousOn\\big( x \\mapsto \\sum_i f_i(x) , s \\big)$$$

Lean4

theorem lowerSemicontinuousOn_tsum {f : ι → α → ℝ≥0∞} (h : ∀ i, LowerSemicontinuousOn (f i) s) :
    LowerSemicontinuousOn (fun x' => ∑' i, f i x') s := fun x hx => lowerSemicontinuousWithinAt_tsum fun i => h i x hx

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