English
For any x, y of shape ds, the CP-rank behaves additively: CPRankMax m x and CPRankMax n y imply CPRankMax (m + n) (x + y).
Русский
CPRankMax по x и y суммарно ведут к CPRankMax (m+n) (x+y).
LaTeX
$$$$ \\text{CPRankMax } m x \\land \\text{CPRankMax } n y \\Rightarrow \\text{CPRankMax } (m+n) (x+y) $$$$
Lean4
theorem cprankMax_add [Mul α] [AddMonoid α] :
∀ {m : ℕ} {n : ℕ} {x : Holor α ds} {y : Holor α ds}, CPRankMax m x → CPRankMax n y → CPRankMax (m + n) (x + y)
| 0, n, x, y, hx, hy => by
match hx with
| CPRankMax.zero => simp only [zero_add, hy]
| m + 1, n, _, y, CPRankMax.succ _ x₁ x₂ hx₁ hx₂, hy =>
by
suffices CPRankMax (m + n + 1) (x₁ + (x₂ + y)) by simpa only [add_comm, add_assoc, add_left_comm] using this
apply CPRankMax.succ
· assumption
· exact cprankMax_add hx₂ hy
