Theorems · Definition · measure theory
MeasureTheory.Measure.Subtype.measureSpace
{δ : Type u_4} → [MeasureTheory.MeasureSpace δ] → {p : δ → Prop} → MeasureTheory.MeasureSpace (Subtype p)In a measure space, one can restrict the measure to a subtype to get a new measure space.
Not registered as an instance, as there are other natural choices such as the normalized restriction
for a probability measure, or the subspace measure when restricting to a vector subspace. Enable
locally if needed with attribute [local instance] Measure.Subtype.measureSpace.
- Defined in
- Mathlib.MeasureTheory.Measure.Restrict
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasureTheory.MeasureSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasureTheory.MeasureSpace.volumeproof · cited by 1,323
- MeasureTheory.Measure.comapproof · cited by 96
- MeasureTheory.MeasureSpacestatement and proof · cited by 51
Cited by10
Results whose statement or proof uses this declaration.
- Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIccstatement · cited by 2
- volume_set_coe_defstatement · cited by 2
- volume_image_subtype_coestatement · cited by 1
- MeasureTheory.integral_subtypestatement · cited by 1
- MeasureTheory.Measure.Subtype.volume_defstatement · cited by 1
- MeasurableSet.map_coe_volumestatement · cited by 0
- volume_preimage_coestatement · cited by 0
- MeasureTheory.Measure.volume_subtype_coe_eq_zero_of_volume_eq_zerostatement · cited by 0
- MeasureTheory.Measure.volume_subtype_coe_le_volumestatement · cited by 0
- MeasureTheory.Measure.Subtype.volume_univstatement · cited by 0