Theorems · Theorem · measure theory
MeasureTheory.ae_restrict_mem
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s- Defined in
- Mathlib.MeasureTheory.Measure.Restrict
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Filter.Eventuallystatement · cited by 3,134
- MeasurableSetstatement and proof · cited by 3,075
- MeasureTheory.aestatement · cited by 2,352
- MeasureTheory.Measure.restrictstatement · cited by 1,646
- MeasurableSet.nullMeasurableSetproof · cited by 155
- MeasureTheory.ae_restrict_mem₀proof · cited by 5
Cited by43
Results whose statement or proof uses this declaration.
- MeasureTheory.ae_restrict_of_forall_memproof · cited by 16
- Asymptotics.IsBigO.integrableAtFilterproof · cited by 7
- intervalIntegrable_congrproof · cited by 4
- ContinuousOn.integrableOn_of_subset_isCompactproof · cited by 3
- MeasureTheory.aecover_Ioi_of_Ioiproof · cited by 3
- MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'proof · cited by 3
- integrableOn_Ioi_rpow_iffproof · cited by 3
- intervalIntegral.integrableOn_Ioo_rpow_iffproof · cited by 3
- ApproximatesLinearOn.norm_fderiv_sub_leproof · cited by 3
- integrable_rpow_mul_exp_neg_mul_sqproof · cited by 2
- ContinuousOn.aestronglyMeasurable_of_subset_isCompactproof · cited by 2
- AntitoneOn.tsum_comp_add_le_integralproof · cited by 2