Theorems · Definition · measure theory
MeasureTheory.Measure.restrict
{α : Type u_2} → {_m0 : MeasurableSpace α} → MeasureTheory.Measure α → Set α → MeasureTheory.Measure αRestrict a measure μ to a set s.
- Defined in
- Mathlib.MeasureTheory.Measure.Restrict
- Cited by
- 1,646 results in Mathlib
- Foundations
- Depth 192 from the axioms, rests on 4,764 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.Measure.restrictₗproof · cited by 4
Cited by1,676
Results whose statement or proof uses this declaration.
- MeasureTheory.IntegrableOnproof · cited by 548
- intervalIntegralproof · cited by 546
- MeasureTheory.Measure.withDensityproof · cited by 265
- MeasureTheory.Measure.restrict_applystatement · cited by 159
- intervalIntegral.integral_of_lestatement and proof · cited by 83
- MeasureTheory.Measure.restrict_univstatement · cited by 76
- MeasureTheory.withDensity_applystatement · cited by 73
- MeasureTheory.ae_restrict_iff'statement · cited by 71
- StronglyMeasurableAtFilterproof · cited by 64
- MeasureTheory.Measure.restrict_le_selfstatement · cited by 57
- MeasureTheory.lintegral_indicatorstatement and proof · cited by 47
- MeasureTheory.ae_restrict_of_aestatement · cited by 46
Showing the 200 most cited of 1,676.