Theorems · Theorem · measure theory
MeasurableEquiv.coe_toLp
∀ (p : ENNReal) (X : Type u_1) [inst : MeasurableSpace X], ⇑(MeasurableEquiv.toLp p X) = WithLp.toLp p
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 102 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.
- DFunLike.coestatement · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- ENNRealstatement and proof · cited by 9,879
- WithLpstatement · cited by 345
- MeasurableEquivstatement · cited by 269
- MeasurableEquiv.toLpstatement · cited by 27
Cited by8
Results whose statement or proof uses this declaration.
- ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covarianceproof · cited by 4
- EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpproof · cited by 4
- MeasureTheory.charFunDual_pi'proof · cited by 1
- MeasureTheory.charFunDual_prod'proof · cited by 1
- MeasureTheory.charFun_eq_pi_iffproof · cited by 1
- MeasureTheory.charFun_eq_prod_iffproof · cited by 1
- MeasureTheory.charFunDual_eq_pi_iff'proof · cited by 1
- MeasureTheory.charFunDual_eq_prod_iff'proof · cited by 1