Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-18 19:10 0a5b9eba

View on Github →

feat(set_theory/game/pgame): tweak lemmas (#14810) This PR does the following:

  • uncurry le_of_forall_lf and le_of_forall_lt.
  • remove lf_of_exists_le, as it's made redundant by lf_of_move_right_le and lf_of_le_move_left.
  • golfing.

Estimated changes

modified theorem pgame.le_of_forall_lf
modified theorem pgame.le_of_forall_lt
modified theorem pgame.lf_move_right_of_le
deleted theorem pgame.lf_of_exists_le
modified theorem pgame.lf_of_le_move_left
modified theorem pgame.lf_of_move_right_le
modified theorem pgame.move_left_lf_of_le