dist_le_zero

Mathlib.Topology.MetricSpace.Defs

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

English

In any metric space, dist(x,y) ≤ 0 if and only if x = y.

Русский

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

LaTeX

$$$dist\;x\;y \le 0 \leftrightarrow x = y$$$

Lean4

@[simp]
theorem dist_le_zero {x y : γ} : dist x y ≤ 0 ↔ x = y := by
  simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y

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

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

Разделы

Аффилиация

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