coeFnAddMonoidHom — Mathlib

English

The map that assigns to each vector measure its pointwise values on sets, i.e. v ↦ (i ↦ v(i)), is an additive monoid homomorphism.

Русский

Отображение, отправляющее векторную меру v в функцию i ↦ v(i), является гомоморфизмом аддитивного моноида.

LaTeX

$$$\mathrm{coeFnAddMonoidHom}: VectorMeasure(\alpha, M) \to+ (Set(\alpha) \to M)$ with toFun = (⇑), map_zero' = 0, map_add' = +$$

Lean4

/-- `(⇑)` is an `AddMonoidHom`. -/
@[simps]
def coeFnAddMonoidHom : VectorMeasure α M →+ Set α → M
    where
  toFun := (⇑)
  map_zero' := coe_zero
  map_add' := coe_add

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