Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-15 01:31 b8d8a5e4

View on Github →

refactor(set_theory/game/*): Fix bad notation < on (pre-)games (#13963) Our current definition for < on pre-games is, in the wider mathematical literature, referred to as ⧏ (less or fuzzy to). Conversely, what's usually referred to by < coincides with the relation we get from preorder pgame (which the current API avoids using at all). We rename < to ⧏, and add the basic API for both the new < and ⧏ relations. This allows us to define new instances on pgame and game that we couldn't before. We also take the opportunity to add some basic API on the fuzzy relation ∥. See the Zulip discussion.

Estimated changes

added theorem game.add_lf_add_left
added theorem game.add_lf_add_right
added def game.fuzzy
deleted theorem game.le_antisymm
deleted theorem game.le_refl
deleted theorem game.le_rfl
deleted theorem game.le_trans
added def game.lf
deleted theorem game.lt_or_eq_of_le
modified theorem game.not_le
added theorem game.not_lf
deleted theorem game.not_lt
deleted def game.partial_order
added theorem pgame.impartial.nonneg
added theorem pgame.impartial.nonpos
added theorem ordinal.to_pgame_lf
added theorem pgame.add_lf_add_left
added theorem pgame.add_lf_add_right
added theorem pgame.equiv.is_empty
added theorem pgame.equiv.not_fuzzy'
added theorem pgame.equiv.not_fuzzy
modified theorem pgame.equiv_rfl
added theorem pgame.fuzzy.not_equiv'
added theorem pgame.fuzzy.not_equiv
added theorem pgame.fuzzy.swap
added theorem pgame.fuzzy.swap_iff
added def pgame.fuzzy
added theorem pgame.fuzzy_congr
added theorem pgame.fuzzy_congr_imp
added theorem pgame.fuzzy_congr_left
added theorem pgame.fuzzy_irrefl
modified theorem pgame.le_congr
added theorem pgame.le_congr_imp
added theorem pgame.le_congr_left
added theorem pgame.le_congr_right
added theorem pgame.le_def_lf
deleted theorem pgame.le_def_lt
deleted theorem pgame.le_iff_neg_ge
added def pgame.le_lf
deleted def pgame.le_lt
modified theorem pgame.le_of_equiv_of_le
modified theorem pgame.le_of_le_of_equiv
added theorem pgame.le_or_gf
deleted theorem pgame.le_trans
deleted theorem pgame.le_trans_aux
modified theorem pgame.le_zero
added theorem pgame.le_zero_lf
added def pgame.lf
added theorem pgame.lf_congr
added theorem pgame.lf_congr_imp
added theorem pgame.lf_congr_left
added theorem pgame.lf_congr_right
added theorem pgame.lf_def
added theorem pgame.lf_def_le
added theorem pgame.lf_irrefl
added theorem pgame.lf_mk
added theorem pgame.lf_mk_of_le
added theorem pgame.lf_move_right
added theorem pgame.lf_of_fuzzy
added theorem pgame.lf_of_le_mk
added theorem pgame.lf_of_le_of_lf
added theorem pgame.lf_of_lf_of_le
added theorem pgame.lf_of_lf_of_lt
added theorem pgame.lf_of_lt
added theorem pgame.lf_of_lt_of_lf
added theorem pgame.lf_of_mk_le
added theorem pgame.lf_zero
added theorem pgame.lf_zero_le
added theorem pgame.lt_congr_imp
added theorem pgame.lt_congr_left
added theorem pgame.lt_congr_right
deleted theorem pgame.lt_def
deleted theorem pgame.lt_def_le
added theorem pgame.lt_iff_le_and_lf
deleted theorem pgame.lt_iff_neg_gt
deleted theorem pgame.lt_mk
deleted theorem pgame.lt_mk_of_le
deleted theorem pgame.lt_move_right
deleted theorem pgame.lt_move_right_of_le
modified theorem pgame.lt_of_equiv_of_lt
deleted theorem pgame.lt_of_le_mk
deleted theorem pgame.lt_of_le_move_left
added theorem pgame.lt_of_le_of_lf
deleted theorem pgame.lt_of_le_of_lt
modified theorem pgame.lt_of_lt_of_equiv
deleted theorem pgame.lt_of_lt_of_le
deleted theorem pgame.lt_of_mk_le
deleted theorem pgame.lt_of_move_right_le
deleted theorem pgame.lt_or_equiv_of_le
deleted theorem pgame.lt_or_equiv_or_gt
deleted theorem pgame.lt_zero
added theorem pgame.mk_lf
added theorem pgame.mk_lf_mk
added theorem pgame.mk_lf_of_le
deleted theorem pgame.mk_lt
deleted theorem pgame.mk_lt_mk
deleted theorem pgame.mk_lt_of_le
added theorem pgame.move_left_lf
deleted theorem pgame.move_left_lt
deleted theorem pgame.move_left_lt_of_le
added theorem pgame.neg_le_iff
added theorem pgame.neg_le_zero_iff
added theorem pgame.neg_lf_iff
added theorem pgame.neg_lf_zero_iff
added theorem pgame.neg_lt_iff
added theorem pgame.neg_lt_zero_iff
added theorem pgame.not_fuzzy_of_ge
added theorem pgame.not_fuzzy_of_le
deleted theorem pgame.not_le
added theorem pgame.not_lf
deleted theorem pgame.not_lt
added theorem pgame.star_fuzzy_zero
deleted theorem pgame.star_lt_zero
modified theorem pgame.zero_le
added theorem pgame.zero_le_lf
added theorem pgame.zero_le_neg_iff
modified theorem pgame.zero_le_one
added theorem pgame.zero_lf
added theorem pgame.zero_lf_le
added theorem pgame.zero_lf_neg_iff
added theorem pgame.zero_lf_one
deleted theorem pgame.zero_lt
added theorem pgame.zero_lt_neg_iff
deleted theorem pgame.zero_lt_star
modified def pgame.first_loses
modified def pgame.first_wins
modified def pgame.left_wins
modified theorem pgame.one_left_wins
modified def pgame.right_wins
modified theorem pgame.star_first_wins
modified theorem pgame.winner_cases
modified theorem pgame.zero_first_loses
added theorem pgame.add_lf_add
deleted theorem pgame.add_lt_add
added theorem pgame.le_of_lf
deleted theorem pgame.le_of_lt
added theorem pgame.lf_asymm
added theorem pgame.lf_iff_lt
deleted theorem pgame.lt_asymm
deleted theorem pgame.lt_iff_le_not_le
added theorem pgame.lt_of_lf
deleted theorem pgame.lt_trans'
deleted theorem pgame.lt_trans
added theorem pgame.not_fuzzy
modified theorem pgame.numeric.le_move_right
modified theorem pgame.numeric.move_left_le