emetricSpace — Mathlib

English

An emetric space is built from ENormedSpace by edist(x,y) = e(x - y).

Русский

Эмерический потенциал задаётся через эnorm: edist(x,y) = e(x − y).

LaTeX

$$def emetricSpace : EMetricSpace V where edist x y := e (x - y)$$

Lean4

/-- Structure of an `EMetricSpace` defined by an extended norm. -/
@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07")]
abbrev emetricSpace : EMetricSpace V where
  edist x y := e (x - y)
  edist_self x := by simp
  eq_of_edist_eq_zero {x y} := by simp [sub_eq_zero]
  edist_comm := e.map_sub_rev
  edist_triangle x y
    z :=
    calc
      e (x - z) = e (x - y + (y - z)) := by rw [sub_add_sub_cancel]
      _ ≤ e (x - y) + e (y - z) := e.map_add_le (x - y) (y - z)

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