English
There is a construction that replaces the topology on a type by the topology induced by the seminorm/core distance, provided the topologies match, preserving the pseudo-metric structure.
Русский
Существует конструкция, которая заменяет топологию на основе топологии, индуцированной нормой/ядром расстояния, при совпадении топологий, сохраняя псевдометрическую структуру.
LaTeX
$$$$\text{Topology}(E) = \text{TopologicalSpace induced by the core distance}.$$$$
Lean4
/-- Produces a `PseudoEMetricSpace E` instance from a `SeminormedSpace.Core` on a type that
already has an existing topology. This requires a proof that the topology induced
by the norm is equal to the preexisting topology. See note [reducible non-instances]. -/
abbrev ofSeminormedSpaceCoreReplaceTopology {𝕜 E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
[T : TopologicalSpace E] (core : SeminormedSpace.Core 𝕜 E)
(H : T = (PseudoEMetricSpace.ofSeminormedSpaceCore core).toUniformSpace.toTopologicalSpace) : PseudoMetricSpace E :=
.replaceTopology (.ofSeminormedSpaceCore core) H
