Def Interval

Modification history

2026-04-02 06:37
Mathlib/Order/Interval/Basic.lean
chore: use a type synonym instead of an abbrev for `Interval` (#37508) …
Added IntervalView on Github →
2024-05-07 01:05
Mathlib/Order/Interval/Basic.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted IntervalView on Github →
2023-08-10 19:52
Mathlib/Order/Interval.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified IntervalView on Github →
2023-05-22 16:35
Mathlib/Order/Interval.lean
feat: port Order.Interval (#3360)
Added IntervalView on Github →