mem_uniformity_edist — Mathlib

English

Membership in the uniformity U is characterized by existence of ε>0 with a distance bound for all pairs.

Русский

Членство в равномерности характеризуется существованием ε>0 с ограничением расстояния для всех пар.

LaTeX

$$$ s ∈ 𝓤 α \iff \exists ε > 0, \forall {a,b}, edist a b < ε \Rightarrow (a,b) ∈ s $$$

Lean4

/-- Characterization of the elements of the uniformity in terms of the extended distance -/
theorem mem_uniformity_edist {s : Set (α × α)} : s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s :=
  uniformity_basis_edist.mem_uniformity_iff

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