cycleGraph_one_adj

Mathlib.Combinatorics.SimpleGraph.Circulant

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

English

For Fin 1, there are no adjacent distinct vertices; no edges exist.

Русский

Для Fin 1 вершин нет соседних пар вершин; ребер нет.

LaTeX

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

Lean4

theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v :=
  by
  rw [cycleGraph_one_eq_bot]
  exact id

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

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

Разделы

Аффилиация

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