Theorem Interval.coe_inf

Modification history

2024-06-07 23:31

Mathlib/Order/Interval/Basic.lean

chore(Order/Interval): use `WithBot` API (#13493)

Modified Interval.coe_inf View on Github →

2023-05-22 16:35

Mathlib/Order/Interval.lean

feat: port Order.Interval (#3360)

Added Interval.coe_inf View on Github →