Theorem eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt

Modification history

2025-12-02 12:55
Mathlib/Order/Basic.lean
chore(Order/Basic): use `@[to_dual]` (#31903) …
Modified eq_iff_eq_of_lt_iff_lt_of_gt_iff_gtView on Github →
2024-01-12 12:47
Mathlib/Order/Basic.lean
feat(Order/Basic): Add `ltByCases` API (#9114) …
Added eq_iff_eq_of_lt_iff_lt_of_gt_iff_gtView on Github →