pathGraph

Mathlib.Combinatorics.SimpleGraph.Hasse

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

English

The path graph on n vertices is defined as the Hasse diagram of the chain Fin n.

Русский

Граф пути на n вершинах определяется как диаграмма Хассе цепи Fin n.

LaTeX

$$$pathGraph(n) = hasse (Fin\ n)$$$

Lean4

/-- The path graph on `n` vertices. -/
def pathGraph (n : ℕ) : SimpleGraph (Fin n) :=
  hasse _

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

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

Разделы

Аффилиация

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