toJordanDecomposition_toSignedMeasure

English

Applying toSignedMeasure after toJordanDecomposition returns the original Jordan decomposition.

Русский

Применение toJordanDecomposition после toSignedMeasure возвращает исходное разложение Йордана.

LaTeX

$$$$ (j.toSignedMeasure).toJordanDecomposition = j. $$$$

Lean4

@[simp]
theorem toJordanDecomposition_toSignedMeasure (j : JordanDecomposition α) :
    j.toSignedMeasure.toJordanDecomposition = j :=
  (@toSignedMeasure_injective _ _ j j.toSignedMeasure.toJordanDecomposition (by simp)).symm

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