cycleGraph_neighborFinset — Mathlib

English

In the cycle graph on n+2 vertices, the neighborFinset of v is exactly {v-1, v+1}.

Русский

В графе цикла на n+2 вершинах множество соседей Finset вершины v равно {v−1, v+1}.

LaTeX

$$$ (cycleGraph\ (n + 2)).neighborFinset\ v = \{v - 1, v + 1\} $$$

Lean4

theorem cycleGraph_neighborFinset {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).neighborFinset v = {v - 1, v + 1} :=
  by simp [neighborFinset, cycleGraph_neighborSet]

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