circulantGraph_eq_symm — Mathlib

English

Replacing s by s ∪ (-s) yields the same circulant graph.

Русский

Замена множества прыжков s на s ∪ (-s) даёт тот же циркулярный граф.

LaTeX

$$circulantGraph(s) = circulantGraph(s ∪ (-s))$$

Lean4

theorem circulantGraph_eq_symm : circulantGraph s = circulantGraph (s ∪ (-s)) :=
  by
  ext (u v : G)
  simp only [circulantGraph, fromRel_adj, Set.mem_union, Set.mem_neg, neg_sub, and_congr_right_iff, iff_self_or]
  intro _ h
  exact Or.symm h

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