Theorem Ordering.orElse_eq_lt

Modification history

2025-03-21 01:28
Mathlib/Order/Compare.lean
chore: remove >6 month old deprecations in `SetTheory` (#23164) …
Deleted Ordering.orElse_eq_ltView on Github →
2024-09-13 20:11
Mathlib/Order/Compare.lean
chore: deprecate `Ordering.orElse` for `.then` (#12068) …
Modified Ordering.orElse_eq_ltView on Github →
2022-11-18 04:44
Mathlib/Order/Compare.lean
feat: port Order.Compare (#569) …
Added Ordering.orElse_eq_ltView on Github →