toJordanDecomposition_zero — Mathlib

English

The Jordan decomposition of the zero signed measure is the zero Jordan decomposition.

Русский

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

LaTeX

$$$$ (0 : SignedMeasure(\alpha)).toJordanDecomposition = 0. $$$$

Lean4

theorem toJordanDecomposition_zero : (0 : SignedMeasure α).toJordanDecomposition = 0 :=
  by
  apply toSignedMeasure_injective
  simp [toSignedMeasure_zero]

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