Theorems · Theorem · measure theory
MeasureTheory.StronglyMeasurable.aestronglyMeasurable
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
{f : α → β}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable f μ- Cited by
- 94 results in Mathlib
- Foundations
- Depth 172 from the axioms, rests on 4,665 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
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.
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.aeproof · cited by 2,352
- MeasureTheory.AEStronglyMeasurablestatement · cited by 755
- MeasureTheory.StronglyMeasurablestatement and proof · cited by 363
- Filter.EventuallyEq.reflproof · cited by 108
Cited by94
Results whose statement or proof uses this declaration.
- Continuous.aestronglyMeasurableproof · cited by 70
- Measurable.aestronglyMeasurableproof · cited by 59
- MeasureTheory.aestronglyMeasurable_constproof · cited by 44
- MeasureTheory.AEEqFun.aestronglyMeasurableproof · cited by 26
- MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eqproof · cited by 12
- MeasureTheory.SimpleFunc.aestronglyMeasurableproof · cited by 11
- MeasureTheory.Integrable.trimproof · cited by 10
- MeasureTheory.condExp_ae_eq_condExpL1proof · cited by 9
- MeasureTheory.condExp_restrict_ae_eq_restrictproof · cited by 8
- MeasureTheory.Lp.mem_Lp_iff_memLpproof · cited by 8
- MeasureTheory.condExp_ae_eq_restrict_of_measurableSpace_eq_onproof · cited by 6
- MeasureTheory.condExp_condExp_of_leproof · cited by 6