uniformity_basis_dist_lt — Mathlib

English

A constant-size diagonal neighborhood forms an entourage of the uniformity: for any ε > 0, the set { (a,b) | dist(a,b) < ε } belongs to the uniformity.

Русский

Окружение диагонали постоянного размера является entourages униформности: для любого ε>0 множество { (a,b) | dist(a,b) < ε } принадлежит униформности.

LaTeX

$$$$ \{ (a,b) \in \alpha \times \alpha \mid \operatorname{dist}(a,b) < \varepsilon \} \in \mathcal{U}(\alpha) \quad (\varepsilon > 0). $$$$

Lean4

theorem uniformity_basis_dist_lt {R : ℝ} (hR : 0 < R) :
    (𝓤 α).HasBasis (fun r : ℝ => 0 < r ∧ r < R) fun r => {p : α × α | dist p.1 p.2 < r} :=
  Metric.mk_uniformity_basis (fun _ => And.left) fun r hr =>
    ⟨min r (R / 2), ⟨lt_min hr (half_pos hR), min_lt_iff.2 <| Or.inr (half_lt_self hR)⟩, min_le_left _ _⟩

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