mathlib
68dc07f6 - refactor(set_theory/game/pgame): rename and add theorems like `-y ≤ -x ↔ x ≤ y` (#14653)

Commit
3 years ago
refactor(set_theory/game/pgame): rename and add theorems like `-y ≤ -x ↔ x ≤ y` (#14653) For `*` in `le`, `lf`, `lt`, we rename `neg_*_iff : -y * -x ↔ x * y` to `neg_*_neg_iff`, and add the theorems `neg_*_iff : -y * x ↔ x * -y`. We further add many missing corresponding theorems for equivalence and fuzziness.
Author
Parents
Loading