restrict_neg — Mathlib

English

Negation commutes with restriction: the restriction of −v to i equals the negation of the restriction of v to i.

Русский

Отрицание коммутирует с ограничением: ограничение −v на i равно отрицанию ограничения v на i.

LaTeX

$$$ (-v) \\restriction i = -\\bigl( v \\restriction i \\bigr) $$$

Lean4

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

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