mapGm — Mathlib

English

View map as an additive monoid homomorphism: the operation v ↦ v.map f defines a homomorphism from VectorMeasure α M to VectorMeasure β M.

Русский

Смотреть на map как отображение-мономод или маркера: отображение v ↦ v.map f задаёт гомоморфизм между векторными мерами.

LaTeX

$$$$ \\text{mapGm}(f): \\; \\text{VectorMeasure}(\\alpha, M) \\to \\text{VectorMeasure}(\\beta, M) $$\n$$ \\text{toFun } v = v.map f, \\; \\text{map_zero' } = \\text{map_zero } f, \\; \\text{map_add' } = \\text{map_add } f. $$$$

Lean4

/-- `VectorMeasure.map` as an additive monoid homomorphism. -/
@[simps]
def mapGm (f : α → β) : VectorMeasure α M →+ VectorMeasure β M
    where
  toFun v := v.map f
  map_zero' := map_zero f
  map_add' _ _ := map_add _ _ f

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