tendstoLocallyUniformlyOn_sUnion — Mathlib

English

If S is a collection of open sets and each yields locally uniform convergence, then their union’s locally uniform convergence holds.

Русский

Если семейство открытых множеств S образует локальную равномерную сходимость по каждому, то их sUnion обладает локальной равномерной сходимостью.

LaTeX

$$$$\operatorname{tendstoLocallyUniformlyOn}_{S}(F,f,p,\bigcup S_i)$$$$

Lean4

theorem tendstoLocallyUniformlyOn_sUnion (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s)
    (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p (⋃₀ S) :=
  by
  rw [sUnion_eq_biUnion]
  exact tendstoLocallyUniformlyOn_biUnion hS h

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