cycleGraph_adj — Mathlib

English

For cycle graph on n+2, two vertices u,v are adjacent exactly when their indices differ by 1 in either direction.

Русский

В цикл-графе на n+2 вершинах две вершины u и v смежны тогда, когда их индексы различаются на 1 в обе стороны.

LaTeX

$$(cycleGraph(n+2)).Adj u v ⇔ u - v = 1 ∨ v - u = 1$$

Lean4

theorem cycleGraph_adj {n : ℕ} {u v : Fin (n + 2)} : (cycleGraph (n + 2)).Adj u v ↔ u - v = 1 ∨ v - u = 1 :=
  by
  simp only [cycleGraph, circulantGraph_adj, Set.mem_singleton_iff, and_iff_right_iff_imp]
  intro _ _
  simp_all

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