union — Mathlib

English

If s and s' are open and locally uniformly converge, then their union is locally uniformly convergent.

Русский

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

LaTeX

$$$$\text{IsOpen}(s) \land \text{IsOpen}(s') \land TendstoLocallyUniformlyOn(F,f,p,s) \land TendstoLocallyUniformlyOn(F,f,p,s') \Rightarrow TendstoLocallyUniformlyOn(F,f,p,s\cup s').$$$$

Lean4

theorem union (hs₁ : IsOpen s) (hs₂ : IsOpen s') (h₁ : TendstoLocallyUniformlyOn F f p s)
    (h₂ : TendstoLocallyUniformlyOn F f p s') : TendstoLocallyUniformlyOn F f p (s ∪ s') :=
  by
  rw [← sUnion_pair]
  refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_ <;> simp [*]

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