supportedEquivFinsupp_symm_single

English

The image of the supported submodule under lmapDomain equals the supported on the image set.

Русский

Образ подмодуля под действием lmapDomain равен поддерживаемому на образе множества.

LaTeX

$$$\mathrm{map}(\mathrm{lmapDomain}(M,R,f), \mathrm{supported}(M,R,s)) = \mathrm{supported}(M,R, f(s))$$$

Lean4

@[simp]
theorem supportedEquivFinsupp_symm_single (s : Set α) (i : s) (a : M) :
    ((supportedEquivFinsupp (R := R) s).symm (single i a) : α →₀ M) = single (↑i) a := by classical simp

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