Theorems · Theorem · measure theory
MeasureTheory.SimpleFunc.stronglyMeasurable
∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] (f : MeasureTheory.SimpleFunc α β),
MeasureTheory.StronglyMeasurable ⇑f- Cited by
- 13 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.SimpleFuncstatement and proof · cited by 411
- MeasureTheory.StronglyMeasurablestatement · cited by 363
- tendsto_const_nhdsproof · cited by 330
Cited by13
Results whose statement or proof uses this declaration.
- MeasureTheory.SimpleFunc.aestronglyMeasurableproof · cited by 11
- MeasureTheory.integral_trimproof · cited by 6
- MeasureTheory.condExp_stronglyMeasurable_bilin_of_boundproof · cited by 3
- MeasureTheory.MemLp.induction_denseproof · cited by 2
- MeasureTheory.Lp.simpleFunc.inductionproof · cited by 2
- MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilinproof · cited by 2
- MeasureTheory.MemLp.inductionproof · cited by 1
- MeasureTheory.integral_trim_simpleFuncproof · cited by 1
- MeasureTheory.StronglyMeasurable.induction'proof · cited by 1
- MeasureTheory.Lp.simpleFunc.stronglyMeasurableproof · cited by 1
- MeasureTheory.VectorMeasure.variation_withDensity'proof · cited by 1
- ProbabilityTheory.strong_law_ae_of_measurableproof · cited by 1