English
The uniform convergence topology indeed yields the same notion of convergence as TendstoUniformly; explicitly, for F : ι → UniformFun α β and f : UniformFun α β, Tendsto F p (𝓝 f) iff TendstoUniformly (toFun ∘ F) (toFun f) p.
Русский
Топология равномерной конвергенции действительно задает ту же концепцию сходимости, что и TendstoUniformly.
LaTeX
$$$$ \text{Tendsto } F p \; (\mathcal N f) \iff \text{ TendstoUniformly } (toFun \circ F) (toFun f) p. $$$$
Lean4
/-- Pre-composition by any function is uniformly continuous for the uniform structures of
uniform convergence.
More precisely, for any `f : γ → α`, the function `(· ∘ f) : (α →ᵤ β) → (γ →ᵤ β)` is uniformly
continuous. -/
protected theorem precomp_uniformContinuous {f : γ → α} : UniformContinuous fun g : α →ᵤ β => ofFun (toFun g ∘ f) := by
-- Here we simply go back to filter bases.
rw [UniformContinuous, (UniformFun.hasBasis_uniformity α β).tendsto_iff (UniformFun.hasBasis_uniformity γ β)]
exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩
