toFinsupp_cons_eq_single_add_embDomain

English

A cons is equal to the sum of the singleton at 0 and the embeddable toFinsupp of the rest.

Русский

Список вида a :: xs эквивалентен сумме единичного на 0 и встроенного toFinsupp xs.

LaTeX

$$$$ \\operatorname{toFinsupp}(x :: xs) = \\mathsf{single}\\,0\\,x + (\\operatorname{toFinsupp} xs).\\operatorname{embDomain} \\langle Nat.succ, Nat.succ_injective \\rangle. $$$$

Lean4

theorem toFinsupp_cons_eq_single_add_embDomain {R : Type*} [AddZeroClass R] (x : R) (xs : List R)
    [DecidablePred (getD (x :: xs) · 0 ≠ 0)] [DecidablePred (getD xs · 0 ≠ 0)] :
    toFinsupp (x :: xs) = Finsupp.single 0 x + (toFinsupp xs).embDomain ⟨Nat.succ, Nat.succ_injective⟩ := by
  classical
  convert toFinsupp_append [x] xs using 3
  · exact (toFinsupp_singleton x).symm
  · ext n
    exact add_comm n 1

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