toJordanDecompositionEquiv — Mathlib

English

There is an Equivalence between SignedMeasure α and JordanDecomposition α given by the pair of maps toJordanDecomposition and toSignedMeasure.

Русский

Существует эквивалентность между SignedMeasure α и JordanDecomposition α, заданная парами отображения toJordanDecomposition и toSignedMeasure.

LaTeX

$$$$ \text{toJordanDecompositionEquiv}(\alpha) : \text{SignedMeasure}(\alpha) \simeq \text{JordanDecomposition}(\alpha). $$$$

Lean4

/-- `MeasureTheory.SignedMeasure.toJordanDecomposition` and
`MeasureTheory.JordanDecomposition.toSignedMeasure` form an `Equiv`. -/
@[simps apply symm_apply]
def toJordanDecompositionEquiv (α : Type*) [MeasurableSpace α] : SignedMeasure α ≃ JordanDecomposition α
    where
  toFun := toJordanDecomposition
  invFun := toSignedMeasure
  left_inv := toSignedMeasure_toJordanDecomposition
  right_inv := toJordanDecomposition_toSignedMeasure

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