upperSemicontinuousAt_sum — Mathlib

English

If f_i are USCAt at x for i ∈ a, then the finite sum ∑_{i∈a} f_i is USCAt x.

Русский

Если f_i — USCAt в x для каждого i ∈ a, то конечная сумма ∑_{i∈a} f_i — USCAt x.

LaTeX

$$$ha : \\forall i, i\\in a \\Rightarrow UpperSemicontinuousAt (f i) x\\Rightarrow\\; UpperSemicontinuousAt (\\sum i∈a, f i) x$$$

Lean4

theorem upperSemicontinuousAt_sum {f : ι → α → γ} {a : Finset ι} (ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x) :
    UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x :=
  by
  simp_rw [← upperSemicontinuousWithinAt_univ_iff] at *
  exact upperSemicontinuousWithinAt_sum ha

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