English
If x has CP-rank m and y has CP-rank n, then x + y has CP-rank at most m + n; more precisely, CPRankMax m x and CPRankMax n y imply CPRankMax (m + n) (x + y).
Русский
Если у x CP-ранг равен m, а у y CP-ранг равен n, то x + y имеет CP-ранг не больше m + n; то есть CPRankMax m x и CPRankMax n y приводят к CPRankMax (m + n) (x + y).
LaTeX
$$$$ CPRankMax m x \\rightarrow CPRankMax n y \\rightarrow CPRankMax (m + n) (x + y) $$$$
Lean4
theorem slice_sum [AddCommMonoid α] {β : Type} (i : ℕ) (hid : i < d) (s : Finset β) (f : β → Holor α (d :: ds)) :
(∑ x ∈ s, slice (f x) i hid) = slice (∑ x ∈ s, f x) i hid :=
by
letI := Classical.decEq β
refine Finset.induction_on s ?_ ?_
· simp [slice_zero]
· intro _ _ h_not_in ih
rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]
