uniformity_basis_edist_nnreal_le — Mathlib

English

Let α be a pseudo-emetric space. The uniformity on α has a basis consisting of sets { (x,y) ∈ α×α : edist(x,y) ≤ ε } 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) \le \varepsilon\}. $$$

Lean4

theorem uniformity_basis_edist_nnreal_le :
    (𝓤 α).HasBasis (fun ε : ℝ≥0 => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 ≤ ε} :=
  EMetric.mk_uniformity_basis_le (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⟩

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