toSignedMeasure_sub_apply — Mathlib

English

Applying toSignedMeasure to a subtraction of measures equals subtraction of their signed measures on measurable sets.

Русский

Применение toSignedMeasure к разности мер равно разности их подписанных мер на измеримых множествах.

LaTeX

$$$ (\mu.toSignedMeasure - \nu.toSignedMeasure)(i) = \mu.real(i) - \nu.real(i) $ for measurable i$$

Lean4

theorem toSignedMeasure_sub_apply {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {i : Set α}
    (hi : MeasurableSet i) : (μ.toSignedMeasure - ν.toSignedMeasure) i = μ.real i - ν.real i := by
  rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi, Measure.toSignedMeasure_apply_measurable hi]

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