uniformity_pseudoedist — Mathlib

English

The uniformity of α is the biinfimum of principal filters generated by { p : α×α | edist p.1 p.2 < ε } as ε → 0+.

Русский

Равномерность пространства α равна biInf главных фильтров, порождаемых множествами { p : α×α | edist p.1 p.2 < ε } при ε → 0+.

LaTeX

$$$ 𝓤 α = ⨅ ε > 0, 𝓟 \{ p : α × α \mid edist p.1 p.2 < ε \} $$$

Lean4

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

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