edist_mem_uniformity — Mathlib

English

For any ε > 0, the set { p ∈ α×α : edist(p.1,p.2) < ε } belongs to the uniformity 𝓤 α.

Русский

Для любого ε > 0 множество {p ∈ α×α : edist(p.1,p.2) < ε} принадлежит униформности 𝓤 α.

LaTeX

$$$ \{(x,y) \in \alpha \times \alpha : \operatorname{edist}(x,y) < \varepsilon\} \in \mathcal{U}(\alpha) \quad \text{for all } \varepsilon>0. $$$

Lean4

/-- Fixed size neighborhoods of the diagonal belong to the uniform structure -/
theorem edist_mem_uniformity {ε : ℝ≥0∞} (ε0 : 0 < ε) : {p : α × α | edist p.1 p.2 < ε} ∈ 𝓤 α :=
  mem_uniformity_edist.2 ⟨ε, ε0, id⟩

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