lmapDomain — Mathlib

English

For any f, lmapDomain M R f acts on f by applying mapDomain f to f; i.e., it is the action that maps a finitely supported function by changing its domain map.

Русский

Для любого f, lmapDomain M R f действует на f через mapDomain f: отображение изменяет область определения функции с конечной опорой.

LaTeX

$$$(lmapDomain\\ M\\ R\\ f)\\ l = mapDomain f\\ l$$$

Lean4

/-- Interpret `Finsupp.mapDomain` as a linear map. -/
def lmapDomain (f : α → α') : (α →₀ M) →ₗ[R] α' →₀ M
    where
  toFun := mapDomain f
  map_add' _ _ := mapDomain_add
  map_smul' := mapDomain_smul

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