uniformity_basis_dist_le — Mathlib

English

The uniformity has a basis consisting of entourages { (a,b) | dist(a,b) ≤ ε } for ε > 0.

Русский

Униформность имеет базис из окружностей { (a,b) | dist(a,b) ≤ ε } для ε > 0.

LaTeX

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

Lean4

/-- Constant size closed neighborhoods of the diagonal form a basis
of the uniformity filter. -/
theorem uniformity_basis_dist_le : (𝓤 α).HasBasis ((0 : ℝ) < ·) fun ε => {p : α × α | dist p.1 p.2 ≤ ε} :=
  Metric.mk_uniformity_basis_le (fun _ => id) fun ε ε₀ => ⟨ε, ε₀, le_refl ε⟩

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