jordanDecompositionOfToSignedMeasureSub_toSignedMeasure

English

The Jordan decomposition of the signed measure (μ.toSignedMeasure − ν.toSignedMeasure) equals jordanDecompositionOfToSignedMeasureSub μ ν.

Русский

Джорданово разложение знаковой меры (μ.toSignedMeasure − ν.toSignedMeasure) равно jordanDecompositionOfToSignedMeasureSub μ ν.

LaTeX

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

Lean4

theorem jordanDecompositionOfToSignedMeasureSub_toSignedMeasure :
    (jordanDecompositionOfToSignedMeasureSub μ ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure := by
  simp_rw [JordanDecomposition.toSignedMeasure, jordanDecompositionOfToSignedMeasureSub_posPart,
    jordanDecompositionOfToSignedMeasureSub_negPart, ← sub_toSignedMeasure_eq_toSignedMeasure_sub]

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