cycleGraph_neighborSet — Mathlib

English

Let the cycle graph on n+2 vertices be given. For every vertex v in Fin(n+2), the neighbor set is exactly {v-1, v+1}.

Русский

Пусть граф цикла на n+2 вершинах. Для каждой вершины v из Fin(n+2) множество соседей равно {v−1, v+1}.

LaTeX

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

Lean4

theorem cycleGraph_neighborSet {n : ℕ} {v : Fin (n + 2)} : (cycleGraph (n + 2)).neighborSet v = {v - 1, v + 1} :=
  by
  ext w
  simp only [mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff]
  rw [cycleGraph_adj, sub_eq_iff_eq_add', sub_eq_iff_eq_add', eq_sub_iff_add_eq, eq_comm]

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