Theorems · Theorem · measure theory

MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure

∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
  (s : Set α),
  MeasurableSet s → MeasureTheory.VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure

Defined in: Mathlib.MeasureTheory.VectorMeasure.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Realstatement · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasurableSetstatement and proof · cited by 3,075
MeasureTheory.Measure.restrictstatement and proof · cited by 1,646
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
MeasureTheory.Measure.realproof · cited by 530
MeasureTheory.VectorMeasurestatement · cited by 451
MeasureTheory.VectorMeasure.restrictstatement · cited by 139
MeasureTheory.VectorMeasure.extproof · cited by 65
MeasureTheory.Measure.toSignedMeasurestatement and proof · cited by 36

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.Measure.toSignedMeasure_restrict_subproof · cited by 1
MeasureTheory.Measure.sub_toSignedMeasure_eq_toSignedMeasure_subproof · cited by 0