tendstoLocallyUniformlyOn_iUnion — Mathlib

English

If each open S_i admits locally uniform convergence and the union is open, then the union converges locally uniformly.

Русский

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

LaTeX

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

Lean4

theorem tendstoLocallyUniformlyOn_iUnion {ι' : Sort*} {S : ι' → Set α} (hS : ∀ i, IsOpen (S i))
    (h : ∀ i, TendstoLocallyUniformlyOn F f p (S i)) : TendstoLocallyUniformlyOn F f p (⋃ i, S i) :=
  (isOpen_iUnion hS).tendstoLocallyUniformlyOn_iff_forall_tendsto.2 fun _x hx =>
    let ⟨i, hi⟩ := mem_iUnion.1 hx
    (hS i).tendstoLocallyUniformlyOn_iff_forall_tendsto.1 (h i) _ hi

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