equivFunOnFinite_single — Mathlib

English

For DecidableEq α and Finite α, the equivalence between finitely supported finsupp and Pi-type sends single x m to the Pi-single x m.

Русский

При конечном алфавите α с допускаемой эквивалентностью, отображение между finsupp и Pi-представлением отправляет single x m в Pi.single x m.

LaTeX

$$$\mathrm{Finsupp}.\mathrm{equivFunOnFinite}(\mathrm{single}(x,m)) = \Pi.single(x,m)$$$

Lean4

@[simp]
theorem equivFunOnFinite_single [DecidableEq α] [Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m := by
  simp [Finsupp.single_eq_pi_single, equivFunOnFinite]

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