toFinsupp_singleton — Mathlib

English

The image of a singleton multiset under toFinsupp is the corresponding singleton function with value 1.

Русский

Образ тождественного мультимножества через toFinsupp равен соответствующей одиночной функции с значением 1.

LaTeX

$$$\mathrm{toFinsupp}({a}) = \mathrm{Finsupp.single}(a,1)$$$

Lean4

@[simp]
theorem toFinsupp_singleton (a : α) : toFinsupp ({ a } : Multiset α) = Finsupp.single a 1 := by ext;
  rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]

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