pos_dist_of_ne

Mathlib.Combinatorics.SimpleGraph.Metric

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Reachable.pos_dist_of_ne

English

If G is connected and u ≠ v, then 0 < dist_G(u,v).

Русский

Если граф G связный и u ≠ v, то dist_G(u,v) > 0.

LaTeX

$$$$ G.Connected \Rightarrow (u \neq v \Rightarrow 0 < \mathrm{dist}_G(u,v)) $$$$

Lean4

protected theorem pos_dist_of_ne (h : G.Reachable u v) (hne : u ≠ v) : 0 < G.dist u v :=
  Nat.pos_of_ne_zero (by simp [h, hne])

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

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

Разделы

Аффилиация

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