neg — Mathlib

English

The negation of a vector measure is again a vector measure.

Русский

Отрицание векторной меры вновь является векторной мерой.

LaTeX

$$$v \mapsto (-v)$ preserves the vector measure structure: -VectorMeasure α M$$

Lean4

/-- The negative of a vector measure is a vector measure. -/
def neg (v : VectorMeasure α M) : VectorMeasure α M
    where
  measureOf' := -v
  empty' := by simp
  not_measurable' _ hi := by rw [Pi.neg_apply, neg_eq_zero, v.not_measurable hi]
  m_iUnion' _ hf₁ hf₂ := HasSum.neg <| v.m_iUnion hf₁ hf₂

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