nhds_eq_comap_uniformity' — Mathlib

English

The neighborhood of x equals the comap of the uniformity by the map y ↦ (y, x).

Русский

Окрестности x равны обратному изображению равномерности по отображению y ↦ (y, x).

LaTeX

$$$\mathcal N(x) = (\mathcal U(\alpha)).comap (\lambda y. (y, x))$$$

Lean4

theorem nhds_eq_comap_uniformity' {x : α} : 𝓝 x = (𝓤 α).comap fun y => (y, x) :=
  (nhds_basis_uniformity (𝓤 α).basis_sets).eq_of_same_basis <| (𝓤 α).basis_sets.comap _

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