toTopologicalSpace — Mathlib

English

A uniform space core induces a natural topology whose neighborhoods are given by comaps of the uniformity via the map x ↦ (x, -).

Русский

Ядро равномерного пространства порождает естественную топологию; окрестности равны обратному образу равномерности по отображению x ↦ (x, -).

LaTeX

$$$\\text{toTopologicalSpace }(u) = \\mathsf{mkOfNhds}(x \\mapsto \\mathrm{comap}(\\mathrm{Prod.mk}\;x)\,u.uniformity)$$$

Lean4

/-- A uniform space generates a topological space -/
def toTopologicalSpace {α : Type u} (u : UniformSpace.Core α) : TopologicalSpace α :=
  .mkOfNhds fun x ↦ .comap (Prod.mk x) u.uniformity

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