tendsto_iff_tendstoUniformly — Mathlib

English

The convergence in the uniform convergence topology is equivalent to convergence in TendstoUniformly under the pointwise embedding.

Русский

Сходимость в топологии равномерной конвергенции эквивалентна сходимости в TendstoUniformly после отображения в точечное произведение.

LaTeX

$$$$ \forall F: ι \to α \to^{u} β, \; \text{Tendsto } F p (\mathcal N f) \;\Leftrightarrow\; \text{TendstoUniformly } (toFun \circ F) (toFun f) p. $$$$

Lean4

/-- The topology of uniform convergence indeed gives the same notion of convergence as
`TendstoUniformly`. -/
protected theorem tendsto_iff_tendstoUniformly {F : ι → α →ᵤ β} {f : α →ᵤ β} :
    Tendsto F p (𝓝 f) ↔ TendstoUniformly (toFun ∘ F) (toFun f) p :=
  by
  rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]
  simp only [mem_setOf, UniformFun.gen, Function.comp_def]

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