uniformity_basis_edist' — Mathlib

English

A refined edist basis with a two-sided bound via exists_between construction.

Русский

Уточнённый базис edist через exists_between.

LaTeX

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

Lean4

theorem uniformity_basis_edist' (ε' : ℝ≥0∞) (hε' : 0 < ε') :
    (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => ε ∈ Ioo 0 ε') fun ε => {p : α × α | edist p.1 p.2 < ε} :=
  EMetric.mk_uniformity_basis (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 _ _⟩

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