card_filter_equitabilise_big

Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

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

English

The number of parts of size m+1 in the equitabilised partition equals b.

Русский

Число частей размера m+1 в равновесном разбиении равно b.

LaTeX

$$$\\#\\{ u \\in (P.equitabilise h).parts:\\; |u|=m+1 \\} = b$$$

Lean4

theorem card_filter_equitabilise_big : #({u ∈ (P.equitabilise h).parts | #u = m + 1}) = b :=
  (P.equitabilise_aux h).choose_spec.2.2

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

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

Разделы

Аффилиация

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