cycleGraph_zero_adj

Mathlib.Combinatorics.SimpleGraph.Circulant

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

English

There is no adjacency in cycleGraph 0, i.e., no edges exist among vertices of Fin 0.

Русский

В cycleGraph 0 нет смежности, то есть ребер среди вершин Fin 0 не существует.

LaTeX

$$∀ u,v : Fin(0), ¬((cycleGraph 0).Adj u v)$$

Lean4

theorem cycleGraph_zero_adj {u v : Fin 0} : ¬(cycleGraph 0).Adj u v :=
  id

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

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

Разделы

Аффилиация

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