nhds_eq_comap_uniformity — Mathlib

English

The neighborhood filter at x is the comap of the uniformity by the map x ↦ (x, -).

Русский

Окрёжностный фильтр в точке x равен обратному образу равномерности по отображению x ↦ (x, -).

LaTeX

$$$\\forall x,\\ \\mathcal{N}(x) = (\\mathcal{U}\\;\\alpha).comap(\\mathrm{Prod.mk}\\ x)$$$

Lean4

theorem nhds_eq_comap_uniformity {x : α} : 𝓝 x = (𝓤 α).comap (Prod.mk x) :=
  UniformSpace.nhds_eq_comap_uniformity x

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