Theorem Ordering.orElse_eq_lt

Modification history

2024-09-13 20:11

Mathlib/Order/Compare.lean

chore: deprecate `Ordering.orElse` for `.then` (#12068) …

Modified Ordering.orElse_eq_lt View on Github →

2022-11-18 04:44

Mathlib/Order/Compare.lean

feat: port Order.Compare (#569) …

Added Ordering.orElse_eq_lt View on Github →