antidiagonal_succ_succ' — Mathlib

English

A double-successor expansion: antidiagonal of n+2 is formed by adding (0, n+2) and (n+2, 0) and mapping the rest with both coordinates incremented.

Русский

Удвоенная рекурсия по антидиагонали: антидиагональ n+2 строится из (0, n+2), (n+2, 0) и отображения антидиагонали n с обоими координатами, увеличенными на единицу.

LaTeX

$$$\\mathrm{antidiagonal}(n+2) = (0,n+2) \\;\\uplus\\; (n+2,0) \\;\\uplus\\; (\\mathrm{antidiagonal}(n)).\\mathrm{map}(\\mathrm{Prod.map}(\\mathrm{Nat.succ}, \\mathrm{Nat.succ})).$$$

Lean4

theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ (antidiagonal n).map (Prod.map Nat.succ Nat.succ) :=
  by
  rw [antidiagonal_succ, antidiagonal_succ', map_cons, map_map, Prod.map_apply]
  rfl

Похожие утверждения