dist_ne_zero

Mathlib.Topology.MetricSpace.Defs

URI: https://scilib.ai/kg/mathlib#dist_ne_zero

English

Distance is nonzero if and only if the points are distinct.

Русский

Расстояние не равно нулю тогда, когда точки различны.

LaTeX

$$$\\operatorname{dist}(x,y) \\neq 0 \\iff x \\neq y$.$$

Lean4

theorem dist_ne_zero {x y : γ} : dist x y ≠ 0 ↔ x ≠ y := by simpa only [not_iff_not] using dist_eq_zero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru