toSignedMeasure_restrict_eq_restrict_toSignedMeasure

English

For any measurable set s, the restriction of μ's signed measure to s equals the signed measure of the restriction of μ to s.

Русский

Для любого измеримого множества s ограничение сигнальной меры μ до s равно сигнальной мере ограниченного до s множества μ.

LaTeX

$$$\mu^{\mathrm{toSignedMeasure}} \restriction s = (\mu \restriction s)^{\mathrm{toSignedMeasure}} \quad (\text{for } s \text{ measurable})$$$

Lean4

theorem toSignedMeasure_restrict_eq_restrict_toSignedMeasure (hs : MeasurableSet s) :
    μ.toSignedMeasure.restrict s = (μ.restrict s).toSignedMeasure :=
  by
  ext A hA
  simp [VectorMeasure.restrict_apply, toSignedMeasure_apply, hA, hs]

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