linearMap_apply_apply — Mathlib

English

For a finite X, a finite Y, and f: X → Y, the y-th value of the image of s under linearMap R M f is the sum of s(x) over all x with f(x) = y.

Русский

Для конечных X, Y и f: X → Y значение в y функции, полученной применением линейного отображения к s, равно сумме s(x) по всем x, удовлетворяющим f(x) = y.

LaTeX

$$$(\mathrm{linearMap}\ R\ M\ f\, s)(y) = \sum_{x \in X \;:\; f(x)=y} s(x)$$$

Lean4

theorem linearMap_apply_apply [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) :
    linearMap R M f s y = (Finset.univ.filter (fun (x : X) ↦ f x = y)).sum s := by apply map_apply_apply

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