color_classes_independent — Mathlib

English

Each color class is independent: no two vertices within the same color class are adjacent.

Русский

Каждый цветовой класс является независимым: внутри одного класса нет смежных вершин.

LaTeX

$$$\\forall c:\\alpha,\\; IsAntichain G.Adj (C.colorClass c)$$$

Lean4

theorem color_classes_independent (c : α) : IsAntichain G.Adj (C.colorClass c) := fun _ hv _ hw _ =>
  C.not_adj_of_mem_colorClass hv hw

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