upperSemicontinuousWithinAt_sum — Mathlib

English

Let f_i be USCAt at x for i in a finite set a. Then the sum over i of f_i is USCAt x.

Русский

Пусть для каждого i из конечного множества a функция f_i имеет верхнюю полупрерывность в x. Тогда сумма по i функций f_i имеет верхнюю полупрерывность в x.

LaTeX

$$$ha : \\forall i, i\\in a \\Rightarrow UpperSemicontinuousAt (f i) x\\Rightarrow\\; UpperSemicontinuousAt (\\lambda z => \\sum_{i\\in a} f i z) x$$$

Lean4

theorem upperSemicontinuousWithinAt_sum {f : ι → α → γ} {a : Finset ι}
    (ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x) : UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x :=
  lowerSemicontinuousWithinAt_sum (γ := γᵒᵈ) ha

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