toJordanDecomposition_toSignedMeasure_sub

English

The Jordan decomposition of μ.toSignedMeasure − ν.toSignedMeasure equals jordanDecompositionOfToSignedMeasureSub μ ν.

Русский

Джорданово разложение μ.toSignedMeasure − ν.toSignedMeasure равно jordanDecompositionOfToSignedMeasureSub μ ν.

LaTeX

$$$(\mu^{\text{toSignedMeasure}} - \nu^{\text{toSignedMeasure}}).toJordanDecomposition = jordanDecompositionOfToSignedMeasureSub(\mu, \nu)$$$

Lean4

/-- The Jordan decomposition of `μ.toSignedMeasure - ν.toSignedMeasure` is `(μ - ν, ν - μ)`. -/
@[simp]
theorem toJordanDecomposition_toSignedMeasure_sub :
    (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = jordanDecompositionOfToSignedMeasureSub μ ν :=
  by
  apply JordanDecomposition.toSignedMeasure_injective
  rw [SignedMeasure.toSignedMeasure_toJordanDecomposition, jordanDecompositionOfToSignedMeasureSub_toSignedMeasure]

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