antidiagonal_succ' — Mathlib

English

Antidiagonal(n+1) equals antidiagonal(n).map(id, Nat.succ) concatenated with (n+1,0).

Русский

Антидиагональ n+1 равна антидиагонали n, отображённой через (id, Nat.succ), объединённой с (n+1,0).

LaTeX

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

Lean4

theorem antidiagonal_succ' {n : ℕ} :
    antidiagonal (n + 1) = (antidiagonal n).map (Prod.map id Nat.succ) ++ [(n + 1, 0)] :=
  by
  simp only [antidiagonal, range_succ, Nat.add_sub_cancel_left, map_append, append_assoc, Nat.sub_self,
    singleton_append, map_map, map]
  congr 1
  apply map_congr_left
  simp +contextual [le_of_lt, Nat.sub_add_comm]

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