reachable

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Adj.reachable

English

If u is adjacent to v, then u is reachable from v (via the edge).

Русский

Если вершины u и v adjacent, то u достижим из v (через кратчайший путь длиной 1).

LaTeX

$$$\forall u,v,\; G.Adj u v \to G.Reachable u v.$$$

Lean4

protected theorem reachable {u v : V} (h : G.Adj u v) : G.Reachable u v :=
  h.toWalk.reachable

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

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

Разделы

Аффилиация

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