uniformity_basis_edist_le' — Mathlib

English

Alternative edist-based basis for the uniformity using ≤ bound and Ioo intervals.

Русский

Альтернативный базис edist через интервалы Ioo и ≤-ограничение.

LaTeX

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

Lean4

theorem uniformity_basis_edist_le' (ε' : ℝ≥0∞) (hε' : 0 < ε') :
    (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => ε ∈ Ioo 0 ε') fun ε => {p : α × α | edist p.1 p.2 ≤ ε} :=
  EMetric.mk_uniformity_basis_le (fun _ => And.left) fun ε ε₀ =>
    let ⟨δ, hδ⟩ := exists_between hε'
    ⟨min ε δ, ⟨lt_min ε₀ hδ.1, lt_of_le_of_lt (min_le_right _ _) hδ.2⟩, min_le_left _ _⟩

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