card_colorClasses_le — Mathlib

English

The number of color classes does not exceed the number of colors: card(C.colorClasses) ≤ card(α).

Русский

Число цветовых классов не превосходит число цветов: card(C.colorClasses) ≤ card(α).

LaTeX

$$$|C.colorClasses| \\le |\\alpha|$$$

Lean4

theorem card_colorClasses_le [Fintype α] [Fintype C.colorClasses] : Fintype.card C.colorClasses ≤ Fintype.card α :=
  by
  simp only [colorClasses]
  convert Setoid.card_classes_ker_le C

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