lmap_of — Mathlib

English

Applying lmap to the pure element of M_i corresponds to the pure element of N_i after applying f_i.

Русский

Применение lmap к чистому элементу из M_i даёт чистый элемент в N_i после применения f_i.

LaTeX

$$$\\mathrm{lmap}\\ f\\ (\\mathrm{of}\\ M_i\\ x) = \\mathrm{of}\\ N_i\\ (f_i x).$$$

Lean4

@[simp]
theorem lmap_of [DecidableEq ι] (i : ι) (x : M i) : lmap f (of M i x) = of N i (f i x) :=
  DFinsupp.mapRange_single (hf := fun _ => map_zero _)

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