toJordanDecomposition_neg — Mathlib

English

Negating a signed measure corresponds to negating its Jordan decomposition components.

Русский

Отрицание подписанной меры соответствует отрицанию ее разложения Йордана.

LaTeX

$$$$ (-s).toJordanDecomposition = - (s.toJordanDecomposition). $$$$

Lean4

theorem toJordanDecomposition_neg (s : SignedMeasure α) : (-s).toJordanDecomposition = -s.toJordanDecomposition :=
  by
  apply toSignedMeasure_injective
  simp [toSignedMeasure_neg]

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