replaceTopology_eq — Mathlib

English

If two topologies correspond as described, replacing the topology yields the original metric space.

Русский

Если топологии соответствуют описанному равенству, замена топологии возвращает исходное метрическое пространство.

LaTeX

$$m.replaceTopology(H) = m$$

Lean4

theorem replaceTopology_eq {γ} [U : TopologicalSpace γ] (m : MetricSpace γ)
    (H : U = m.toPseudoMetricSpace.toUniformSpace.toTopologicalSpace) : m.replaceTopology H = m := by ext; rfl

Похожие утверждения