toSignedMeasure_add — Mathlib

English

The signed measure of the sum of two finite measures is the sum of their signed measures.

Русский

Подписанная мера суммы двух конечных мер равна сумме их подписанных мер.

LaTeX

$$$ (\mu + \nu).toSignedMeasure = \mu.toSignedMeasure + \nu.toSignedMeasure $$$

Lean4

@[simp]
theorem toSignedMeasure_add (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure :=
  by
  ext i hi
  rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply, VectorMeasure.add_apply,
    toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi]

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