replaceTopology_eq — Mathlib

English

If U equals the topology induced by the uniform structure of m, then replacing the topology yields the same space: m.replaceTopology H = m.

Русский

Если U равно топологии, порождаемой равномерной структурой m, то m.replaceTopology H = m.

LaTeX

$$$m.replaceTopology H = m$ whenever $H : U = m.toUniformSpace.toTopologicalSpace$.$$

Lean4

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

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