English
For a pseudometric space α, the uniform structure is the bottom (discrete) if and only if there exists r > 0 such that for all distinct x,y, dist(x,y) ≥ r.
Русский
Для псевдометрического пространства α равномерная структура является нулевой (дискретной) тогда и только тогда, существует r > 0 такое, что для любых различны́х x и y выполняется dist(x,y) ≥ r.
LaTeX
$$$\\bigl(\\text{toUniformSpace } \\alpha = ⊥\\bigr) \\iff \\exists r \\in \\mathbb{R},\\ r > 0 \\wedge \\text{Pairwise } (r \\le \\operatorname{dist}(\\cdot, \\cdot) : \\alpha \\to \\alpha \\to \\mathbb{R}).$$$
Lean4
/-- (Pseudo) metric space has discrete `UniformSpace` structure
iff the distances between distinct points are uniformly bounded away from zero. -/
protected theorem uniformSpace_eq_bot :
‹PseudoMetricSpace α›.toUniformSpace = ⊥ ↔ ∃ r : ℝ, 0 < r ∧ Pairwise (r ≤ dist · · : α → α → Prop) := by
simp only [uniformity_basis_dist.uniformSpace_eq_bot, mem_setOf_eq, not_lt]
