nonempty_path

Mathlib.Combinatorics.Quiver.ConnectedComponent

URI: https://scilib.ai/kg/mathlib#Quiver.IsStronglyConnected.nonempty_path

English

If the quiver is strongly connected, then for any pair i, j there exists a path from i to j.

Русский

Если кьювер сильносвязный, то для любых вершин i, j существует путь i → j.

LaTeX

$$$ IsStronglyConnected(V) \\rightarrow \\forall i,j:\\ V, \\text{Nonempty}(\\text{Path}(i,j)) $$$

Lean4

theorem nonempty_path (h : IsStronglyConnected V) (i j : V) : Nonempty (Path i j) :=
  h i j

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

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

Разделы

Аффилиация

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