uniformity_dist — Mathlib

English

The uniformity on the completion equals the infimum over ε>0 of principal filters of the sets {p: dist p.fst p.snd < ε}.

Русский

Однородность завершения равна инфимума по ε>0 главных фильтров от множеств {p | dist p.fst p.snd < ε}.

LaTeX

$$$\mathcal{U}(\mathrm{Completion}\,\alpha) = \inf_{\varepsilon>0} \mathcal{P}\{p\mid \operatorname{dist} p.1 p.2 < \varepsilon\}$$$

Lean4

protected theorem uniformity_dist : 𝓤 (Completion α) = ⨅ ε > 0, 𝓟 {p | dist p.1 p.2 < ε} := by
  simpa [iInf_subtype] using @Completion.uniformity_dist' α _

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