Commit 2025-08-13 10:56 4be5ac8d

feat: some measure-theoretic properties of the unitInterval (#27748) In particular, this shows that the coercion (↑) : I → ℝ is a measure-preserving map to the restriction of Lebesgue measure to the unit interval, constructs unitInterval.symm as a measurable equivalence, and proves that it is measure-preserving on I.