not_adj_of_mem_colorClass — Mathlib

English

If v and w belong to the same color class, then v and w are not adjacent.

Русский

Если вершины v и w принадлежат одному цвету классу, то они не смежны.

LaTeX

$$$\\forall c:\\alpha\\, \\forall v,w:\\, V,\\; v \\in C.colorClass c \\rightarrow w \\in C.colorClass c \\rightarrow \\neg G.Adj v w$$$

Lean4

theorem not_adj_of_mem_colorClass {c : α} {v w : V} (hv : v ∈ C.colorClass c) (hw : w ∈ C.colorClass c) : ¬G.Adj v w :=
  fun h => C.valid h (Eq.trans hv (Eq.symm hw))

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