Theorems · Definition · measure theory
MeasureTheory.StronglyMeasurable
{α : Type u_1} → {β : Type u_2} → [TopologicalSpace β] → [MeasurableSpace α] → (α → β) → PropA function is StronglyMeasurable if it is the limit of simple functions.
- Cited by
- 363 results in Mathlib
- Foundations
- Depth 21 from the axioms, rests on 229 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- Filter.atTopproof · cited by 2,405
- MeasureTheory.SimpleFuncproof · cited by 411
Cited by371
Results whose statement or proof uses this declaration.
- MeasureTheory.AEStronglyMeasurableproof · cited by 755
- MeasureTheory.StronglyMeasurable.aestronglyMeasurablestatement and proof · cited by 94
- MeasureTheory.StronglyAdaptedproof · cited by 81
- MeasureTheory.StronglyMeasurable.measurablestatement and proof · cited by 74
- MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mkstatement · cited by 71
- MeasureTheory.IsStronglyProgressiveproof · cited by 54
- MeasureTheory.StronglyMeasurable.comp_measurablestatement and proof · cited by 52
- Measurable.stronglyMeasurablestatement · cited by 47
- MeasureTheory.stronglyMeasurable_conststatement · cited by 47
- MeasureTheory.StronglyMeasurable.approxstatement and proof · cited by 40
- MeasureTheory.StronglyMeasurable.tendsto_approxstatement and proof · cited by 36
- MeasureTheory.stronglyMeasurable_condExpstatement and proof · cited by 35
Showing the 200 most cited of 371.