edist_eq_zero_iff

Mathlib.Combinatorics.SimpleGraph.Metric

URI: https://scilib.ai/kg/mathlib#SimpleGraph.edist_eq_zero_iff

English

For any u,v,w, edist u w ≤ edist u v + edist v w.

Русский

Для любых вершин u,v,w неравенство треугольника для edist: edist u w ≤ edist u v + edist v w.

LaTeX

$$$ G.edist u w \le G.edist u v + G.edist v w $$$

Lean4

@[simp]
theorem edist_eq_zero_iff : G.edist u v = 0 ↔ u = v := by apply Iff.intro <;> simp [edist, ENat.iInf_eq_zero]

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

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

Разделы

Аффилиация

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