Theorems · Theorem · measure theory
WithLp.measurable_ofLp
∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X], Measurable WithLp.ofLp
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
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.
- MeasurableSpacestatement and proof · cited by 13,106
- ENNRealstatement and proof · cited by 9,879
- Measurablestatement · cited by 1,499
- WithLpstatement · cited by 345
- WithLp.ofLpstatement and proof · cited by 323
- comap_measurableproof · cited by 9
Cited by6
Results whose statement or proof uses this declaration.
- MeasurableEquiv.toLpproof · cited by 27
- ProbabilityTheory.variance_eval_multivariateGaussianproof · cited by 1
- ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_evalproof · cited by 0
- ProbabilityTheory.measurePreserving_eval_multivariateGaussianproof · cited by 0
- ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_evalproof · cited by 0