pathGraph_adj — Mathlib

English

In the path graph on Fin n, two vertices u,v are adjacent exactly when their values differ by 1 in either direction.

Русский

В графе пути на Fin n две вершины соседние тогда и только тогда, когда их значения отличаются на 1 в любом направлении.

LaTeX

$$$(pathGraph n).Adj u v \iff u.val + 1 = v.val \lor v.val + 1 = u.val$$$

Lean4

theorem pathGraph_adj {n : ℕ} {u v : Fin n} : (pathGraph n).Adj u v ↔ u.val + 1 = v.val ∨ v.val + 1 = u.val :=
  by
  simp only [pathGraph, hasse]
  simp_rw [← Fin.coe_covBy_iff, covBy_iff_add_one_eq]

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