English
The uniformity on α has a basis given by sets { (x,y) : edist(x,y) < (↑n)⁻¹ } for natural numbers n, i.e. distances smaller than 1/n.
Русский
Униформность на α имеет базис, заданный множествами { (x,y) : edist(x,y) < (↑n)⁻¹ } для натуральных n, т.е. расстояния меньше 1/n.
LaTeX
$$$ (\mathcal{U}_\alpha) \text{ has basis } \{V_n\}_{n \in \mathbb{N}},\quad V_n = \{(x,y) \in \alpha \times \alpha : \operatorname{edist}(x,y) < (\uparrow n)^{-1}\}. $$$
Lean4
theorem uniformity_basis_edist_inv_nat :
(𝓤 α).HasBasis (fun _ => True) fun n : ℕ => {p : α × α | edist p.1 p.2 < (↑n)⁻¹} :=
EMetric.mk_uniformity_basis (fun n _ ↦ ENNReal.inv_pos.2 <| ENNReal.natCast_ne_top n) fun _ε ε₀ ↦
let ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt (ne_of_gt ε₀)
⟨n, trivial, le_of_lt hn⟩
