Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 11:13 9c40f30a

View on Github →

refactor(set_theory/game/*): fix theorem names (#14685) Some theorems about exists had forall in the name, other theorems about swapped ≤ or ⧏ used le and lf instead of ge and gf. We also golf le_of_forall_lt.

Estimated changes

added theorem has_le.le.not_gf
deleted theorem has_le.le.not_lf
added theorem pgame.le_of_forall_lt
modified theorem pgame.lf.not_equiv'
modified theorem pgame.lf.not_equiv
added theorem pgame.lf.not_ge
added theorem pgame.lf.not_gt
deleted theorem pgame.lf.not_le
deleted theorem pgame.lf.not_lt
added theorem pgame.lf_iff_exists_le
deleted theorem pgame.lf_iff_forall_le
modified theorem pgame.lf_irrefl
added theorem pgame.lf_of_exists_le
deleted theorem pgame.lf_of_forall_le
deleted theorem pgame.le_of_forall_lt
added theorem pgame.lt_iff_exists_le
deleted theorem pgame.lt_iff_forall_le
added theorem pgame.lt_of_exists_le
deleted theorem pgame.lt_of_forall_le