uniformSpace — Mathlib

English

The uniform structure on a field k is transferred to R via an absolute value abv, giving a uniform space on R with distance d(x,y)=abv(y−x).

Русский

Унитильная структура на поле k переносится на R через абсолютную величину abv, задавая равномерное пространство на R с расстоянием d(x,y)=abv(y−x).

LaTeX

$$$\\text{uniformSpace on } \\mathbb{R} \text{ given by } d(x,y)=|y-x| \\text{ (via } abv)$$$

Lean4

/-- The uniform structure coming from an absolute value. -/
def uniformSpace : UniformSpace R :=
  .ofFun (fun x y => abv (y - x)) (by simp) (fun x y => abv.map_sub y x)
    (fun _ _ _ => (abv.sub_le _ _ _).trans_eq (add_comm _ _)) fun ε ε0 =>
    ⟨ε / 2, half_pos ε0, fun _ h₁ _ h₂ => (add_lt_add h₁ h₂).trans_eq (add_halves ε)⟩

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