uniformity_edist — Mathlib

English

The uniformity on γ is generated by the extended distance: 𝓤 γ = ⨅ ε > 0, 𝓟 {p : γ×γ | edist p.1 p.2 < ε}.

Русский

Уоднообразование на γ задаётся через расширенное расстояние: 𝓤 γ = ⨅ ε > 0, 𝓟 {p : γ×γ | edist p.1 p.2 < ε}.

LaTeX

$$$\\mathcal{U}(\\gamma) = \\bigwedge_{\\varepsilon>0} \\mathcal{P}\\{p \\in \\gamma \\times \\gamma \\mid \\mathrm{edist}(p_1,p_2) < \\varepsilon\\}$$$

Lean4

/-- Reformulation of the uniform structure in terms of the extended distance -/
theorem uniformity_edist : 𝓤 γ = ⨅ ε > 0, 𝓟 {p : γ × γ | edist p.1 p.2 < ε} :=
  PseudoEMetricSpace.uniformity_edist

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