edist_pos

Mathlib.Topology.EMetricSpace.Defs

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

English

For all x,y, 0 < edist x y iff x ≠ y.

Русский

Для любых x,y 0 < edist x y тогда и только тогда, когда x ≠ y.

LaTeX

$$$0 < \\mathrm{edist}(x,y) \\iff x \\neq y$$$

Lean4

@[simp]
theorem edist_pos {x y : γ} : 0 < edist x y ↔ x ≠ y := by simp [← not_le]

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

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

Разделы

Аффилиация

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