dist_pos

Mathlib.Topology.MetricSpace.Defs

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

English

In any metric space, dist(x,y) > 0 iff x ≠ y.

Русский

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

LaTeX

$$$0 < dist\;x\;y \leftrightarrow x \neq y$$$

Lean4

@[simp]
theorem dist_pos {x y : γ} : 0 < dist x y ↔ x ≠ y := by simpa only [not_le] using not_congr dist_le_zero

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

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

Разделы

Аффилиация

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