Theorems · Definition · measure theory
MeasurableEquiv.funUnique
(α : Type u_8) → (β : Type u_9) → [Unique α] → [inst : MeasurableSpace β] → (α → β) ≃ᵐ β
If α has a unique term, then the type of function α → β is measurably equivalent to β.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniqueMeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- Uniquestatement and proof · cited by 400
- MeasurableEquivstatement · cited by 269
- MeasurableEquiv.piUniqueproof · cited by 6
Cited by10
Results whose statement or proof uses this declaration.
- MeasureTheory.volume_preserving_funUniquestatement · cited by 4
- MeasureTheory.hausdorffMeasure_realproof · cited by 2
- MeasurableEquiv.funUnique_symm_applystatement and proof · cited by 1
- Measure.ext_of_integral_mul_boundedContinuousFunctionproof · cited by 1
- MeasureTheory.measurePreserving_funUniquestatement · cited by 1
- MeasureTheory.hausdorffMeasure_measurePreserving_funUniquestatement · cited by 1
- MeasureTheory.integral_eq_of_hasDerivAt_off_countable_of_leproof · cited by 1
- MeasurableEquiv.funUnique_applystatement and proof · cited by 0
- torusIntegral_dim1proof · cited by 0