English
Let α be a pseudo-emetric space. The uniformity on α has a basis consisting of sets of pairs whose extended distance is less than ε, for ε > 0.
Русский
Пусть α — псевдометрическое пространство. Униформность 𝓤(α) имеет базис, состоящий из пар {(x,y) ∈ α×α: edist(x,y) < ε} при ε > 0.
LaTeX
$$$ (\mathcal{U}_\alpha) \text{ has basis } \{V_\varepsilon\}_{\varepsilon>0},\quad V_\varepsilon = \{(x,y) \in \alpha \times \alpha : \operatorname{edist}(x,y) < \varepsilon\}. $$$
Lean4
theorem uniformity_basis_edist_nnreal :
(𝓤 α).HasBasis (fun ε : ℝ≥0 => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 < ε} :=
EMetric.mk_uniformity_basis (fun _ => ENNReal.coe_pos.2) fun _ε ε₀ =>
let ⟨δ, hδ⟩ := ENNReal.lt_iff_exists_nnreal_btwn.1 ε₀
⟨δ, ENNReal.coe_pos.1 hδ.1, le_of_lt hδ.2⟩
