Commit 2025-11-13 20:36 a118834e

View on Github →

feat(UnitInterval): x : I and its symmetric sum to 1 (#31396)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

Modified Mathlib/Topology/UnitInterval.lean

modified theorem unitInterval.coe_toNNReal

modified def unitInterval.toNNReal

added theorem unitInterval.toNNReal_add_toNNReal_symm

modified theorem unitInterval.toNNReal_continuous

added theorem unitInterval.toNNReal_one

added theorem unitInterval.toNNReal_symm_add_toNNReal

added theorem unitInterval.toNNReal_zero