set_univ_walk_nonempty

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

← MathLib Explorer

English

If G is connected, then for any u,v there exists a walk from u to v.

Русский

Если граф G связан, то для любых вершин u и v существует ход от u к v.

LaTeX

$$$ G.Connected \\Rightarrow ∀ u v, (Set.univ : Set (G.Walk u v)).Nonempty $$$

Lean4

theorem set_univ_walk_nonempty (hconn : G.Connected) (u v : V) : (Set.univ : Set (G.Walk u v)).Nonempty :=
  hconn.preconnected.set_univ_walk_nonempty u v

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

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

Разделы

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

Аффилиация

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