dist_ofPreNNDist_le — Mathlib

English

If a function d satisfies a triangle-like inequality with a bound, then d(x,y) ≤ 2 dist x y, where dist is the largest pseudometric bounded by d.

Русский

Если функция d удовлетворяет треугольному аналогичному неравенству, ограниченному, тогда d(x,y) ≤ 2 dist(x,y), где dist — наибольшая псевдометрическая величина, не превышающая d.

LaTeX

$$$\\forall d, dist, dist\\_self, dist\\_comm, hd, x,y:\\;\\uparrow(d\\,x\\,y) \\le 2 \\cdot dist\\;x\\;y$$$

Lean4

theorem dist_ofPreNNDist_le (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0) (dist_comm : ∀ x y, d x y = d y x)
    (x y : X) :
    @dist X (@PseudoMetricSpace.toDist X (PseudoMetricSpace.ofPreNNDist d dist_self dist_comm)) x y ≤ d x y :=
  NNReal.coe_le_coe.2 <| (ciInf_le (OrderBot.bddBelow _) []).trans_eq <| by simp

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