uniformity_basis_edist_le — Mathlib

English

A variant of the edist basis with a ≤ relation and ε bound.

Русский

Вариант базиса edist с ≤ и ε-ограничением.

LaTeX

$$$ (uniformity α).HasBasis (fun ε => ε ∈ Ioo 0 ∞) (fun ε => {p : α × α | edist p.1 p.2 ≤ ε}) $$$

Lean4

theorem uniformity_basis_edist_le : (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 ≤ ε} :=
  EMetric.mk_uniformity_basis_le (fun _ => id) fun ε ε₀ => ⟨ε, ε₀, le_refl ε⟩

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