toSignedMeasure_neg — Mathlib

English

Negation of a Jordan decomposition corresponds to negation of its signed measure.

Русский

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

LaTeX

$$$\mathrm{toSignedMeasure}(-j) = -\mathrm{toSignedMeasure}(j)$$$

Lean4

theorem toSignedMeasure_neg : (-j).toSignedMeasure = -j.toSignedMeasure :=
  by
  ext1 i hi
  rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi, toSignedMeasure_sub_apply hi, neg_sub,
    neg_posPart, neg_negPart]

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