Theorems · Theorem · measure theory
PiLp.volume_preserving_ofLp
∀ (ι : Type u_4) [inst : Fintype ι], MeasureTheory.MeasurePreserving WithLp.ofLp MeasureTheory.volume MeasureTheory.volume
A copy of EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp
for the canonical spelling of the equivalence.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fintype
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- ENNRealstatement · cited by 9,879
- Fintypestatement and proof · cited by 7,736
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- WithLpstatement · cited by 345
- WithLp.ofLpstatement · cited by 323
- MeasureTheory.MeasurePreservingstatement · cited by 259
- EuclideanSpace.volume_preserving_symm_measurableEquiv_toLpproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.