tendstoLocallyUniformlyOn_biUnion

English

If each S_i is open and TendstoLocallyUniformlyOn on S_i, then TendstoLocallyUniformlyOn on the bi-union of all S_i.

Русский

Если каждый S_i является открытым и обладает локальной равномерной сходимостью, то локальная равномерная сходимость на объединении по всем S_i сохраняется.

LaTeX

$$$$\forall i, IsOpen(S_i) \to (\forall i, TendstoLocallyUniformlyOn(F,f,p,S_i)) \Rightarrow TendstoLocallyUniformlyOn(F,f,p(\bigcup_i S_i)).$$$$

Lean4

theorem tendstoLocallyUniformlyOn_biUnion {s : Set γ} {S : γ → Set α} (hS : ∀ i ∈ s, IsOpen (S i))
    (h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)) : TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i) :=
  tendstoLocallyUniformlyOn_iUnion (fun i => isOpen_iUnion (hS i)) fun i ↦ tendstoLocallyUniformlyOn_iUnion (hS i) (h i)

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