pathGraph_preconnected

Mathlib.Combinatorics.SimpleGraph.Hasse

URI: https://scilib.ai/kg/mathlib#SimpleGraph.pathGraph_preconnected

English

The path graph on n vertices is preconnected.

Русский

Граф пути на n вершинах предсоединен.

LaTeX

$$$(pathGraph n).Preconnected$$$

Lean4

theorem pathGraph_preconnected (n : ℕ) : (pathGraph n).Preconnected :=
  hasse_preconnected_of_succ _

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

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

Разделы

Аффилиация

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