mem_colorClasses — Mathlib

English

For any vertex v, the color class containing its color is a member of the collection of color classes: C.colorClass (C v) ∈ C.colorClasses.

Русский

Для любой вершины v цветовой класс, содержащий её цвет, принадлежит множеству colorClasses: C.colorClass (C v) ∈ C.colorClasses.

LaTeX

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

Lean4

theorem mem_colorClasses {v : V} : C.colorClass (C v) ∈ C.colorClasses :=
  ⟨v, rfl⟩

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