uniformity_dist' — Mathlib

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

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