toJordanDecomposition_smul — Mathlib

English

Scaling a signed measure by a nonnegative scalar commutes with taking its Jordan decomposition.

Русский

Умножение подписанной меры на неотрицательный скаляр commute с разложением Йордана.

LaTeX

$$$$ (r \cdot s).toJordanDecomposition = r \cdot (s.toJordanDecomposition) $$$$

Lean4

theorem toJordanDecomposition_smul (s : SignedMeasure α) (r : ℝ≥0) :
    (r • s).toJordanDecomposition = r • s.toJordanDecomposition :=
  by
  apply toSignedMeasure_injective
  simp [toSignedMeasure_smul]

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