of_dist_ne_zero

Mathlib.Combinatorics.SimpleGraph.Metric

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

English

If dist_G(u,v) ≠ 0, then u and v are reachable.

Русский

Если dist_G(u,v) ≠ 0, то u и v достижимы.

LaTeX

$$$$ \mathrm{dist}_G(u,v) \neq 0 \Rightarrow \mathrm{Reachable}(u,v) $$$$

Lean4

theorem of_dist_ne_zero (h : G.dist u v ≠ 0) : G.Reachable u v :=
  (dist_ne_zero_iff_ne_and_reachable.mp h).2

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

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

Разделы

Аффилиация

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