dist_eq_of_dist_zero — Mathlib

English

In a pseudometric space, if dist(y,z)=0 then dist(x,y)=dist(x,z) for any x.

Русский

В псевдометрическом пространстве, если dist(y,z)=0, то для любого x выполняется dist(x,y)=dist(x,z).

LaTeX

$$$\operatorname{dist}(y,z)=0 \Rightarrow \operatorname{dist}(x,y)=\operatorname{dist}(x,z)$$$

Lean4

theorem dist_eq_of_dist_zero (x : α) {y z : α} (h : dist y z = 0) : dist x y = dist x z :=
  dist_comm y x ▸ dist_comm z x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (h ▸ abs_dist_sub_le y z x))

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