Theorem unitInterval.symm_bijective

Modification history

2024-02-28 00:16

Mathlib/Topology/UnitInterval.lean

feat: `MeasureSpace` instance on `unitInterval` (#10452) …

Modified unitInterval.symm_bijective View on Github →

2023-12-01 11:18

Mathlib/Topology/UnitInterval.lean

feat(*/Equiv/*): Add `symm_bijective` lemmas next to `symm_symm`s (#8444)

Added unitInterval.symm_bijective View on Github →