pseudoMetricSpace — Mathlib

English

Instantiate the real numbers as a pseudometric space with distance dist(x,y) = |x−y|, satisfying the usual metric axioms.

Русский

Числа Реал заменяем на псевдометрическое пространство с расстоянием dist(x,y)=|x−y|, удовлетворяющим обычным аксиомам метрики.

LaTeX

$$$\\text{Real is a PseudoMetricSpace with } dist(x,y)=|x-y|.$$$

Lean4

/-- Instantiate the reals as a pseudometric space. -/
instance pseudoMetricSpace : PseudoMetricSpace ℝ
    where
  dist x y := |x - y|
  dist_self := by simp [abs_zero]
  dist_comm _ _ := abs_sub_comm _ _
  dist_triangle _ _ _ := abs_sub_le _ _ _

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