colorable — Mathlib

English

If P is a partition with finitely many parts, then G is colorable with exactly the number of parts, i.e., Fintype.card P.parts.

Русский

Если разбиение P имеет конечное число частей, граф G можно раскрасить в количество цветов, равное числу частей разбиения.

LaTeX

$$[Fintype P.parts] → G.Colorable (Fintype.card P.parts)$$

Lean4

theorem colorable [Fintype P.parts] : G.Colorable (Fintype.card P.parts) :=
  P.toColoring.colorable

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