English
The natural map from bounded continuous functions to uniformly continuous functions is inducing; i.e., the topology on α →ᵇ β is the initial topology induced by the map to α →ᵤ β.
Русский
Естественный отображение из области ограниченных непрерывных функций в множество равномерно непрерывных функций индуцирует топологию; то есть топология на α →ᵇ β — начальная топология, индуцированная этим отображением.
LaTeX
$$IsInducing (UniformFun.ofFun ∘ (λ f: α →ᵇ β, f))$$
Lean4
/-- The topology on `α →ᵇ β` is exactly the topology induced by the natural map to `α →ᵤ β`. -/
theorem isInducing_coeFn : IsInducing (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) → α →ᵤ β) :=
by
rw [isInducing_iff_nhds]
refine fun f => eq_of_forall_le_iff fun l => ?_
rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly, UniformFun.tendsto_iff_tendstoUniformly]
simp [comp_def]
-- TODO: upgrade to `IsUniformEmbedding`
