English
The antidiagonal of n+1 is obtained by prepending (0,n+1) and mapping the previous diagonal forward in the first coordinate.
Русский
Антидиагональ(n+1) получаем добавлением (0,n+1) слева и отображением предыдущей диагонали в первый координат.
LaTeX
$$$\operatorname{antidiagonal}(n+1) = \{(0,n+1)\} \cup (\operatorname{antidiagonal}(n)).map (\mathrm{Embedded.prodMap} (\langle \mathrm{Nat.succ}, \mathrm{Nat.succ_injective} \rangle) (\mathrm{Embedding.refl} _))$$$
Lean4
theorem antidiagonal_succ (n : ℕ) :
antidiagonal (n + 1) =
cons (0, n + 1) ((antidiagonal n).map (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ (Embedding.refl _)))
(by simp) :=
by
apply eq_of_veq
rw [cons_val, map_val]
apply Multiset.Nat.antidiagonal_succ
