English
There is a basis of the uniformity indexed by natural numbers n with entourages { (a,b) | dist(a,b) < 1/n } for n large enough (positive).
Русский
Существует база униформности, индексируемая по натуральным числам n с окружностями { (a,b) | dist(a,b) < 1/n } для больших n.
LaTeX
$$$$ (\\mathcal{U}(\\alpha)) \\HasBasis (n: \\mathbb{N}) \\bigl( n \\mapsto \\{ (a,b) \\in \\alpha \\times \\alpha \\mid \\operatorname{dist}(a,b) < 1/n \\} \\bigr) $$$$
Lean4
theorem uniformity_basis_dist_inv_nat_pos :
(𝓤 α).HasBasis (fun n : ℕ => 0 < n) fun n : ℕ => {p : α × α | dist p.1 p.2 < 1 / ↑n} :=
Metric.mk_uniformity_basis (fun _ hn => div_pos zero_lt_one <| Nat.cast_pos.2 hn) fun _ ε0 =>
let ⟨n, hn⟩ := exists_nat_one_div_lt ε0
⟨n + 1, Nat.succ_pos n, mod_cast hn.le⟩