card_parts_equitabilise_subset_le

English

For any t in P.parts, the size of t minus the union of subparts inside t is at most m.

Русский

Для любой части t из P.parts величина |t \ t'| (где t' — объединение подчастей внутри t) не превосходит m.

LaTeX

$$$\\#\\Bigl(t \\setminus \\{u\\in (P.equitabilise h).parts\\ mid u\\subseteq t\\}.biUnion id\\Bigr) \\le m$ для всех $t\\in P.parts$$$

Lean4

theorem card_parts_equitabilise_subset_le :
    t ∈ P.parts → #(t \ {u ∈ (P.equitabilise h).parts | u ⊆ t}.biUnion id) ≤ m :=
  (Classical.choose_spec <| P.equitabilise_aux h).2.1 t

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