English
Construct a new metric space by replacing its topological structure with a given one, preserving the metric structure.
Русский
Построение нового метрического пространства путём замены топологической структуры на заданную, сохранив метрическую структуру.
LaTeX
$$ReplaceTopology\,{γ} [U: TopologicalSpace\ γ] (m: MetricSpace\ γ) (H: U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) : MetricSpace γ$$
Lean4
/-- Build a new metric space from an old one where the bundled topological structure is provably
(but typically non-definitionaly) equal to some given topological structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev replaceTopology {γ} [U : TopologicalSpace γ] (m : MetricSpace γ)
(H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) : MetricSpace γ :=
@MetricSpace.replaceUniformity γ (m.toUniformSpace.replaceTopology H) m rfl
