Theorem unitInterval.one_sub_le_one

Modification history

2026-10-06 22:43
Mathlib/Topology/UnitInterval.lean
chore: deprecate `plus` and `minus` in names (#44566) …
Added unitInterval.one_sub_le_oneView on Github →