toFinsupp_concat_eq_toFinsupp_add_single

English

The toFinsupp of xs ++ [x] equals toFinsupp xs plus the single x embedded at position xs.length.

Русский

toFinsupp xs ++ [x] равно toFinsupp xs плюс единичный на позиции xs.length, вставленный в список.

LaTeX

$$$$ \\operatorname{toFinsupp}(xs ++ [x]) = \\operatorname{toFinsupp} xs + \\mathsf{Finsupp}.single\\, xs.length\\, x. $$$$

Lean4

theorem toFinsupp_concat_eq_toFinsupp_add_single {R : Type*} [AddZeroClass R] (x : R) (xs : List R)
    [DecidablePred fun i => getD (xs ++ [x]) i 0 ≠ 0] [DecidablePred fun i => getD xs i 0 ≠ 0] :
    toFinsupp (xs ++ [x]) = toFinsupp xs + Finsupp.single xs.length x := by
  classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single, addLeftEmbedding_apply, add_zero]

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