card_eq_of_mem_parts_equitabilise

Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

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

English

If t is a part of the equipartition of P, then its size is either m or m+1.

Русский

Размер любой части равновесного разбиения равен либо m, либо m+1.

LaTeX

$$$\\forall t\\in (P.equitabilise h).parts:\\;|t|\\in\\{m,\\;m+1\\}$$$

Lean4

theorem card_eq_of_mem_parts_equitabilise : t ∈ (P.equitabilise h).parts → #t = m ∨ #t = m + 1 :=
  (P.equitabilise_aux h).choose_spec.1 _

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

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

Разделы

Аффилиация

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