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 _) _ _ _ _ _