Commit 2025-04-08 12:42 04bc0659
View on Github →feat(Order/Interval): add strict inclusion lemmas for unbounded intervals (#23798) This PR adds several lemmas relating the strict containment of one-sided intervals to the strict inequality of their boundary.