antidiagonal_succ_succ' — Mathlib

English

Antidiagonal(n+2) equals (0, n+2) cons mapped over antidiagonal(n) with Nat.succ on both coordinates, then appended with (n+2,0).

Русский

Антидиагональ n+2 равна (0, n+2) :: (antidiagonal n).map (Prod.map Nat.succ Nat.succ) ++ [(n+2, 0)].

LaTeX

$$$\\forall {\\n : \\mathbb{N}}, \\mathrm{antidiagonal}(n+2) = (0, n+2) :: (\\mathrm{antidiagonal}(n)).map(Prod.map Nat.succ Nat.succ) ++ [(n+2, 0)]$$$

Lean4

theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) = (0, n + 2) :: (antidiagonal n).map (Prod.map Nat.succ Nat.succ) ++ [(n + 2, 0)] :=
  by
  rw [antidiagonal_succ']
  simp only [antidiagonal_succ, map_cons, Prod.map_apply, id_eq, map_map, cons_append, cons.injEq,
    append_cancel_right_eq, true_and]
  ext
  simp

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