Commit 2023-12-19 12:55 98fe17fd

View on Github →

feat: MeasurableSpace instance for ULift (#8967)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem MeasurableEmbedding.borelSpace

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added def MeasurableEquiv.ulift.{u,

added theorem measurableSet_preimage_down

added theorem measurableSet_preimage_up

added theorem measurable_down

added theorem measurable_up