restrictGm — Mathlib

English

For any vector measure v, the restriction to a set i defines an additive monoid homomorphism v ↦ v|i. In particular, (v + w)|i = v|i + w|i and 0|i = 0.

Русский

Для любой векторной меры v отображение v ↦ v|i является гомоморфизмом аддитивного моноида. В частности, (v + w)|i = v|i + w|i и 0|i = 0.

LaTeX

$$$ (v+w) \\restriction i = v \\restriction i + w \\restriction i \\;\\land\\; 0 \\restriction i = 0 $$$

Lean4

/-- `VectorMeasure.restrict` as an additive monoid homomorphism. -/
@[simps]
def restrictGm (i : Set α) : VectorMeasure α M →+ VectorMeasure α M
    where
  toFun v := v.restrict i
  map_zero' := restrict_zero
  map_add' _ _ := restrict_add _ _ i

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