mem_colorClass — Mathlib

English

Let C be a coloring of G by α. Then each vertex v is contained in the color class corresponding to its color, i.e., v ∈ colorClass(C(v)).

Русский

Пусть C — раскраска графа G вершинами из α. Тогда вершина v принадлежит соответствующему ей цветному классу: v ∈ colorClass(C(v)).

LaTeX

$$$v \\in C.colorClass (C v)$$$

Lean4

theorem mem_colorClass (v : V) : v ∈ C.colorClass (C v) :=
  rfl

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