uniformity_basis_dist — Mathlib

English

The uniformity on α has a basis consisting of entourages of the form { (a,b) ∈ α×α | dist a b < ε } for ε > 0.

Русский

Униформность на α имеет базис из окружностей вида { (a,b) ∈ α×α | dist(a,b) < ε } при ε > 0.

LaTeX

$$$$ (\mathcal{U}(\alpha)) \text{ has basis } (\varepsilon > 0) \mapsto \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) < \varepsilon \}. $$$$

Lean4

theorem uniformity_basis_dist : (𝓤 α).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {p : α × α | dist p.1 p.2 < ε} :=
  by
  rw [toUniformSpace_eq]
  exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

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