tendstoUniformlyOn_iff_tendstoUniformlyOnFilter

English

If TendstoUniformlyOn holds on a set s and s' ⊆ s, then it also holds on s'.

Русский

Если выполнима равномерная сходимость на множестве s, и s' ⊆ s, то она тоже выполняется на s'.

LaTeX

$$$$TendstoUniformlyOn(F,f,p,s)\\land s'\\subseteq s\\Rightarrow TendstoUniformlyOn(F,f,p,s').$$$$

Lean4

theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter :
    TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s) :=
  by
  simp only [TendstoUniformlyOn, TendstoUniformlyOnFilter]
  apply forall₂_congr
  simp_rw [eventually_prod_principal_iff]
  simp

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