antidiagonal_succ — Mathlib

English

For any n, the antidiagonal of n+1 consists of the pair (0, n+1) together with the map of the antidiagonal of n by (i,j) ↦ (i+1, j).

Русский

Для любого n антидиагональ n+1 состоит из пары (0, n+1) и отображения антидиагонали n через (i,j) ↦ (i+1, j).

LaTeX

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

Lean4

@[simp]
theorem antidiagonal_succ {n : ℕ} : antidiagonal (n + 1) = (0, n + 1) ::ₘ (antidiagonal n).map (Prod.map Nat.succ id) :=
  by simp only [antidiagonal, List.Nat.antidiagonal_succ, map_coe, cons_coe]

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