circulantGraph_adj_translate — Mathlib

English

Adjacency in a circulant graph is invariant under simultaneous translation of both endpoints by the same group element d.

Русский

Смежность в циркулярном графе сохраняется при одновременном переносе обеих вершин на одно и то же элемент группы d.

LaTeX

$$(circulantGraph s).Adj(u + d)(v + d) ↔ (circulantGraph s).Adj u v$$

Lean4

theorem circulantGraph_adj_translate {s : Set G} {u v d : G} :
    (circulantGraph s).Adj (u + d) (v + d) ↔ (circulantGraph s).Adj u v := by simp

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