English
The map toUniformOnFunIsCompact is an isUniformEmbedding, i.e., injective and preserves uniformity.
Русский
Отображение toUniformOnFunIsCompact является равномерно вложением: инъективно и сохраняет равномерность.
LaTeX
$$$$ IsUniformEmbedding (toUniformOnFunIsCompact) $$$$
Lean4
/-- Uniform space structure on `C(α, β)`.
The uniformity comes from `α →ᵤ[{K | IsCompact K}] β` (i.e., `UniformOnFun α β {K | IsCompact K}`)
which defines topology of uniform convergence on compact sets.
We use `ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn`
to show that the induced topology agrees with the compact-open topology
and replace the topology with `compactOpen` to avoid non-defeq diamonds,
see Note [forgetful inheritance]. -/
instance compactConvergenceUniformSpace : UniformSpace C(α, β) :=
.replaceTopology (.comap toUniformOnFunIsCompact inferInstance) <|
by
refine TopologicalSpace.ext_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_
simp_rw [← tendsto_id', tendsto_iff_forall_isCompact_tendstoUniformlyOn, nhds_induced, tendsto_comap_iff,
UniformOnFun.tendsto_iff_tendstoUniformlyOn]
rfl
