toCore_toTopologicalSpace — Mathlib

English

The operation of turning a UniformSpace into its core and back to topology yields the original topology.

Русский

Преобразование UniformSpace в его ядро и обратно в топологию восстанавливает исходную топологию.

LaTeX

$$$\\text{toCore_toTopologicalSpace }(u) : u.toCore.toTopologicalSpace = u.toTopologicalSpace$$$

Lean4

theorem toCore_toTopologicalSpace (u : UniformSpace α) : u.toCore.toTopologicalSpace = u.toTopologicalSpace :=
  TopologicalSpace.ext_nhds fun a ↦ by rw [u.nhds_eq_comap_uniformity, u.toCore.nhds_toTopologicalSpace]

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