antidiagonal_succ — Mathlib

English

For any n, antidiagonal(n+1) equals (0, n+1) cons mapped over antidiagonal(n).

Русский

Для любого n антидиагональ n+1 равна конструктору (0, n+1) :: (antidiagonal(n)).map(Prod.map Nat.succ id).

LaTeX

$$$\\forall {\\n : \\mathbb{N}}, \\mathrm{antidiagonal}(n+1) = (0, n+1) :: (\\mathrm{antidiagonal}(n)).map(Prod.map Nat.succ 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, range_succ_eq_map, map_cons, Nat.add_succ_sub_one, Nat.add_zero, id, Nat.sub_zero, map_map,
    Prod.map_apply]
  apply congr rfl (congr rfl _)
  ext; simp

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