uniformity_eq_comap_nhds_zero — Mathlib

English

In a pseudometric space, the uniform structure is obtained as the comap of the distance-to-zero map from α×α to ℝ with the neighborhood of 0.

Русский

В псеметрическом пространстве выписанная равномерная структура получается как обратная композиция по отношению к карте расстояния между точками к нулю в ℝ, используя окрестности нуля.

LaTeX

$$$\mathcal U(\alpha) = \operatorname{comap}\bigl(\lambda p:(\alpha\times\alpha), \operatorname{dist}(p_1,p_2)\bigr)\bigl( \mathcal N(0) \bigr)$$$

Lean4

theorem uniformity_eq_comap_nhds_zero : 𝓤 α = comap (fun p : α × α => dist p.1 p.2) (𝓝 (0 : ℝ)) :=
  by
  ext s
  simp only [mem_uniformity_dist, (nhds_basis_ball.comap _).mem_iff]
  simp [subset_def, Real.dist_0_eq_abs]

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