Theorems · Definition · measure theory
MeasurableSet
{α : Type u_1} → [MeasurableSpace α] → Set α → PropMeasurableSet s means that s is measurable (in the ambient measure space on α)
- Cited by
- 3,075 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 definitions · uses no axioms
- Assumes
- MeasurableSpace
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.
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasurableSpace.MeasurableSet'proof · cited by 4
Cited by3,241
Results whose statement or proof uses this declaration.
- Measurableproof · cited by 1,499
- MeasureTheory.NullMeasurableSetproof · cited by 337
- MeasureTheory.Measure.extstatement and proof · cited by 308
- MeasureTheory.Measure.withDensityproof · cited by 265
- Measurable.compproof · cited by 234
- MeasurableSet.univstatement and proof · cited by 178
- MeasurableSet.complstatement · cited by 172
- MeasurableSet.interstatement and proof · cited by 167
- MeasureTheory.Measure.restrict_applystatement and proof · cited by 159
- measurable_constproof · cited by 156
- MeasurableSet.nullMeasurableSetstatement and proof · cited by 155
- MeasureTheory.Measure.map_applystatement and proof · cited by 139
Showing the 200 most cited of 3,241.