colorClasses — Mathlib

English

The set of all color classes of a coloring is the kernel's classes of the coloring relation.

Русский

Множество всех классoв цвета определяется как классов ядра соответствующего отображения окраски.

LaTeX

$$$\\mathrm{colorClasses} = (\\mathrm{Setoid.ker} C).\\mathrm{classes}$$$

Lean4

/-- The set containing all color classes. -/
def colorClasses : Set (Set V) :=
  (Setoid.ker C).classes

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