English
Given a pseudometric space m and a topological structure U, if U matches the topology induced by m via its uniform structure, one can replace topology without changing the space.
Русский
Для псевдометрического пространства m и топологической структуры U, если U совпадает с топологией, индуцированной равномерной структурой, то заменойTopology не меняем пространство.
LaTeX
$$$m.replaceTopology\\ H = m$ under the condition that topologies agree: $H : U = m.toUniformSpace.toTopologicalSpace$.$$
Lean4
/-- Build a new pseudo 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 : PseudoMetricSpace γ)
(H : U = m.toUniformSpace.toTopologicalSpace) : PseudoMetricSpace γ :=
@PseudoMetricSpace.replaceUniformity γ (m.toUniformSpace.replaceTopology H) m rfl
