pos_dist_of_ne

Mathlib.Combinatorics.SimpleGraph.Metric

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

← MathLib Explorer

English

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

Русский

Если граф 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 (hconn : G.Connected) (hne : u ≠ v) : 0 < G.dist u v :=
  Nat.pos_of_ne_zero fun h ↦ False.elim <| hne <| (hconn.dist_eq_zero_iff).mp h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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