antidiagonal_succ' — Mathlib

English

A variant: antidiagonal(n+1) equals cons (n+1,0) and a transformed copy of antidiagonal(n).

Русский

Вариант: anti diagonal(n+1) равна cons (n+1,0) и преобразованная копия antidiagonal(n).

LaTeX

$$$\operatorname{antidiagonal}(n+1) = \operatorname{cons} (n+1,0) (\operatorname{antidiagonal}(n)).map (\mathrm{Embedding.prodMap} (\mathrm{Embedding.refl} _) (\langle \mathrm{Nat.succ}, \mathrm{Nat.succ_injective} \rangle))$$$

Lean4

theorem antidiagonal_succ' (n : ℕ) :
    antidiagonal (n + 1) =
      cons (n + 1, 0) ((antidiagonal n).map (Embedding.prodMap (Embedding.refl _) ⟨Nat.succ, Nat.succ_injective⟩))
        (by simp) :=
  by
  apply eq_of_veq
  rw [cons_val, map_val]
  exact Multiset.Nat.antidiagonal_succ'

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