English
If a pseudometric space α has a positive lower bound r for the distances between distinct points, then α has the discrete topology.
Русский
Если в псевдометрическом пространстве α расстояния между различными точками имеют положительную нижнюю границу r, то топология пространства дискретна.
LaTeX
$$$\\exists r>0\\; \\forall x\\neq y,\\ dist(x,y) \\ge r \\implies \\text{DiscreteTopology}(\\alpha).$$$
Lean4
/-- If the distances between distinct points in a (pseudo) metric space
are uniformly bounded away from zero, then the space has discrete topology. -/
theorem of_forall_le_dist {α} [PseudoMetricSpace α] {r : ℝ} (hpos : 0 < r)
(hr : Pairwise (r ≤ dist · · : α → α → Prop)) : DiscreteTopology α :=
⟨by rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]⟩
/- Instantiate a pseudometric space as a pseudoemetric space. Before we can state the instance,
we need to show that the uniform structure coming from the edistance and the
distance coincide. -/
