Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-01 05:59 232c15e5

View on Github →

feat(set_theory/game/pgame): Add missing basic API (#13744)

Estimated changes

Modified src/set_theory/game/pgame.lean

added theorem pgame.half_left_moves

modified theorem pgame.half_move_left

modified theorem pgame.half_move_right

added theorem pgame.half_right_moves

added theorem pgame.le_zero_of_is_empty_left_moves

added theorem pgame.left_moves_of_lists

modified def pgame.of_lists

added theorem pgame.of_lists_move_left'

added theorem pgame.of_lists_move_left

added theorem pgame.of_lists_move_right'

added theorem pgame.of_lists_move_right

modified theorem pgame.one_left_moves

modified theorem pgame.one_move_left

modified theorem pgame.one_right_moves

added theorem pgame.right_moves_of_lists

modified def pgame.star

added theorem pgame.star_left_moves

added theorem pgame.star_move_left

added theorem pgame.star_move_right

added theorem pgame.star_right_moves

added def pgame.to_of_lists_left_moves

added def pgame.to_of_lists_right_moves

added theorem pgame.zero_le_of_is_empty_right_moves

added theorem pgame.zero_le_one

modified theorem pgame.zero_left_moves

modified theorem pgame.zero_lt_one

modified theorem pgame.zero_right_moves