toFinsupp_single — Mathlib

English

The toFinsupp of a singleton in DFinsupp equals the corresponding singleton in Finsupp: (DFinsupp.single i m).toFinsupp = Finsupp.single i m.

Русский

Переобразование одиночной функции DFinsupp в Finsupp даёт соответствующую одиночную функцию: (DFinsupp.single i m).toFinsupp = Finsupp.single i m.

LaTeX

$$(DFinsupp.single i m).toFinsupp = Finsupp.single i m$$

Lean4

@[simp]
theorem toFinsupp_single (i : ι) (m : M) : (DFinsupp.single i m : Π₀ _ : ι, M).toFinsupp = Finsupp.single i m :=
  by
  ext
  simp [Finsupp.single_apply, DFinsupp.single_apply]

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