restrict_add — Mathlib

English

Restriction distributes over addition: (v + w).restrict i = v.restrict i + w.restrict i.

Русский

Ограничение распределяется по сложению: (v + w).restrict i = v.restrict i + w.restrict i.

LaTeX

$$$$ (v + w).\\mathrm{restrict} i = v.\\mathrm{restrict} i + w.\\mathrm{restrict} i. $$$$

Lean4

@[simp]
theorem restrict_add (v w : VectorMeasure α M) (i : Set α) : (v + w).restrict i = v.restrict i + w.restrict i :=
  by
  by_cases hi : MeasurableSet i
  · ext j hj
    simp [restrict_apply _ hi hj]
  · simp [restrict_not_measurable _ hi]

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