English
For n ∈ ℕ, antidiagonal(n+2) is built from (0,n+2) and (n+2,0) together with the image of antidiagonal(n) under the coordinate-wise successor map, finishing with a final element.
Русский
Для целого n+2 антидиагональ строится из (0,n+2) и (n+2,0) и отображения антидиагонали n в пару (i+1,j+1), завершая последовательность.
LaTeX
$$$\\operatorname{antidiagonal}(n+2) = \\operatorname{cons}(0,n+2) \\bigl( \\operatorname{cons}(n+2,0) \\bigl( (\\operatorname{antidiagonal}(n)).map (\\operatorname{Embedding.prodMap} \\langle Nat.succ, Nat.succ\\_injective \\rangle \\langle Nat.succ, Nat.succ\\_injective \\rangle) \\bigr) \\bigr) .$$
Lean4
theorem antidiagonal_succ_succ' {n : ℕ} :
antidiagonal (n + 2) =
cons (0, n + 2)
(cons (n + 2, 0)
((antidiagonal n).map (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ ⟨Nat.succ, Nat.succ_injective⟩)) <|
by simp)
(by simp) :=
by
simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]
rfl
