chunk — Mathlib

English

If m ≠ 0, then the number of parts of chunk hP G ε hU is 4^{|P.parts|}.

Русский

Если m ≠ 0, то число частей chunk hP G ε hU равно 4^{|P.parts|}.

LaTeX

$$$\#(\mathrm{chunk}\; hP\; G\; ε\; hU).\mathrm{parts} = 4^{\#P.parts}$$$

Lean4

/-- The portion of `SzemerediRegularity.increment` which partitions `U`. -/
noncomputable def chunk : Finpartition U :=
  if hUcard : #U = m * 4 ^ #P.parts + (card α / #P.parts - m * 4 ^ #P.parts) then
    (atomise U <| P.nonuniformWitnesses G ε U).equitabilise <| card_aux₁ hUcard
  else (atomise U <| P.nonuniformWitnesses G ε U).equitabilise <| card_aux₂ hP hU hUcard

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