Commit 2022-12-02 01:48 73a64196

View on Github →

feat: has_le.le.not_lt_iff_eq (#768) Matches https://github.com/leanprover-community/mathlib/pull/17734

Estimated changes

Modified Mathlib/Order/Basic.lean

added theorem LE.le.ge_iff_eq

added theorem LE.le.gt_iff_ne

modified theorem LE.le.le_iff_eq

modified theorem LE.le.lt_iff_ne

added theorem LE.le.not_gt_iff_eq

added theorem LE.le.not_lt_iff_eq