Commit 2024-02-28 00:16 d67e1758

View on Github →

feat: MeasureSpace instance on unitInterval (#10452) Also shows that it is a probability measure, and that symm is measurable. This deprecates two duplicate theorems. Zulip

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/UnitInterval.lean

added theorem unitInterval.measurable_symm

added theorem unitInterval.volume_def

Modified Mathlib/Topology/UnitInterval.lean

deleted theorem unitInterval.bijective_symm

deleted theorem unitInterval.involutive_symm

added def unitInterval.symmHomeomorph

modified theorem unitInterval.symm_bijective

added theorem unitInterval.symm_involutive