restrictₗ — Mathlib

English

Restriction to i is a linear map: for any v,w and c, (restrict i)(v+w) = (restrict i)v + (restrict i)w and (restrict i)(c • v) = c • (restrict i)v.

Русский

Ограничение до i является линейным отображением: (restrict i)(v+w) = restrict i v + restrict i w и (restrict i)(c • v) = c • restrict i v.

LaTeX

$$$ (v + w) \\restriction i = v \\restriction i + w \\restriction i \\land (c \\cdot v) \\restriction i = c \\cdot (v \\restriction i) $$$

Lean4

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

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