English
The uniformity on the completion equals an infimum over ε>0 of principal filters of the ε-ball congruences.
Русский
Одинаковость по завершению равна инфиминуму над ε>0 от главных фильтров по ε-балам расстояний.
LaTeX
$$$\mathcal{U}(\mathrm{Completion}\,\alpha) = \inf_{\varepsilon>0} \mathsf{principal}\{p\mid \operatorname{dist} p.1 p.2 < \varepsilon\}$$$
Lean4
/-- Reformulate `Completion.mem_uniformity_dist` in terms that are suitable for the definition
of the metric space structure. -/
protected theorem uniformity_dist' : 𝓤 (Completion α) = ⨅ ε : { ε : ℝ // 0 < ε }, 𝓟 {p | dist p.1 p.2 < ε.val} :=
by
ext s; rw [mem_iInf_of_directed]
· simp [Completion.mem_uniformity_dist, subset_def]
· rintro ⟨r, hr⟩ ⟨p, hp⟩
use ⟨min r p, lt_min hr hp⟩
simp +contextual