map_apply_apply — Mathlib

English

A variant expression for FunOnFinite.map showing the same finite-sum decomposition.

Русский

Вариант выражения для FunOnFinite.map, демонстрирующий тот же разложение по конечной сумме.

LaTeX

$$$\big(\text{FunOnFinite.map } f \ s\ y\big) = \sum_{x \in \mathrm{univ}, f x = y} s x$$$

Lean4

theorem map_apply_apply [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) :
    map f s y = ∑ x with f x = y, s x :=
  by
  obtain ⟨s, rfl⟩ := Finsupp.equivFunOnFinite.surjective s
  dsimp [map]
  simp only [Equiv.symm_apply_apply]
  nth_rw 1 [← Finsupp.univ_sum_single s]
  rw [Finsupp.mapDomain_finset_sum]
  simp [Finset.sum_filter]
  congr
  aesop

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