English
Let α be a finite type with a fixed equipartition P of the universe into parts, and let u be a subset. If |u| = m · 4^{|P.parts|} + a for some integers m and a, then |u| equals (4^{|P.parts|} − a)·m + a·(m+1).
Русский
Пусть α конечного типа, разбиение P разбиение универсума на части (равномерное). Пусть u — подмножество. Если размер u равен |u| = m · 4^{|P.parts|} + a, то тогда |u| = (4^{|P.parts|} − a) · m + a · (m+1).
LaTeX
$$$|u| = m \cdot 4^{|P.parts|} + a \Rightarrow |u| = (4^{|P.parts|} - a) \cdot m + a \cdot (m+1)$$$
Lean4
theorem card_aux₁ (hucard : #u = m * 4 ^ #P.parts + a) : (4 ^ #P.parts - a) * m + a * (m + 1) = #u := by
rw [hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), mul_comm]
