Theorems · Theorem · measure theory
MeasureTheory.volume_preserving_pi_empty
∀ {ι : Type u} (α : ι → Type v) [inst : Fintype ι] [inst_1 : IsEmpty ι]
[inst_2 : (i : ι) → MeasureTheory.MeasureSpace (α i)],
MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit)) MeasureTheory.volume
MeasureTheory.volume- Defined in
- Mathlib.MeasureTheory.Constructions.Pi
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Fintypestatement and proof · cited by 7,736
- MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
- IsEmptystatement and proof · cited by 759
- MeasurableEquivstatement · cited by 269
- MeasureTheory.MeasurePreservingstatement · cited by 259
- MeasureTheory.MeasureSpacestatement and proof · cited by 51
- MeasurableEquiv.ofUniqueOfUniquestatement · cited by 2
- MeasureTheory.measurePreserving_pi_emptyproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.