card_parts_le_card

Mathlib.Order.Partition.Finpartition

URI: https://scilib.ai/kg/mathlib#Finpartition.card_parts_le_card

English

Русский

LaTeX

$$$|s| \\bmod |P.parts| \\le |P.parts|$$

Lean4

theorem card_parts_le_card : #P.parts ≤ #s := by
  rw [← card_bot s]
  exact card_mono bot_le

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru