cycleGraph_adj' — Mathlib

English

For cycleGraph n, two vertices u,v are adjacent exactly when (u − v).val equals 1 or (v − u).val equals 1.

Русский

Для cycleGraph n смежность выполняется тогда, когда (u − v).val = 1 или (v − u).val = 1.

LaTeX

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

Lean4

theorem cycleGraph_adj' {n : ℕ} {u v : Fin n} : (cycleGraph n).Adj u v ↔ (u - v).val = 1 ∨ (v - u).val = 1 := by
  match n with
  | 0 => exact u.elim0
  | 1 => simp [cycleGraph_one_adj]
  | n + 2 => simp [cycleGraph_adj, Fin.ext_iff]

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