uniformity_edist — Mathlib

English

In a pseudometric space α, the uniform structure equals the infimum over ε>0 of the principal filters on the sets where edist(x,y) < ε.

Русский

В псевдометрическом пространстве α равномерная структура равна инфимума по ε>0 от примарных фильтров на множествах { (x,y) : edist(x,y) < ε }.

LaTeX

$$$\\mathcal{U}(α) = \\bigwedge_{\\varepsilon>0} 𝓟\\{ (x,y) ∈ α×α \\mid \\operatorname{edist}(x,y) < ε\\}.$$$

Lean4

theorem uniformity_edist : 𝓤 α = ⨅ ε > 0, 𝓟 {p : α × α | edist p.1 p.2 < ε} := by
  simp only [PseudoMetricSpace.uniformity_dist, dist_nndist, edist_nndist, Metric.uniformity_edist_aux]
    -- see Note [lower instance priority]

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