tendstoUniformly_iff_tendstoUniformlyOnFilter

English

TendstoUniformlyOn F f p s is equivalent to TendstoUniformlyOnFilter F f p (principal s).

Русский

Равномерная сходимость на s эквивалентна TendstoUniformlyOnFilter на principal s.

LaTeX

$$$$TendstoUniformlyOn(F,f,p,s)\\iff TendstoUniformlyOnFilter(F,f,p,\\mathcal{P}(s)).$$$$

Lean4

theorem tendstoUniformly_iff_tendstoUniformlyOnFilter : TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤ := by
  rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]

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