Commit 2023-05-19 12:42 b9638579

View on Github →

feat: port SetTheory.Game.PGame (#1512)

Estimated changes

added theorem LE.le.not_gf
added theorem PGame.Equiv.ge
added theorem PGame.Equiv.isEmpty
added theorem PGame.Equiv.le
added theorem PGame.Equiv.not_fuzzy'
added theorem PGame.Equiv.not_fuzzy
added def PGame.Equiv
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.IsOption.mk_left
added inductive PGame.IsOption
added def PGame.LeftMoves
added theorem PGame.Lf.not_equiv'
added theorem PGame.Lf.not_equiv
added theorem PGame.Lf.not_ge
added theorem PGame.Lf.not_gt
added def PGame.Lf
added theorem PGame.Relabelling.ge
added theorem PGame.Relabelling.le
added inductive PGame.Relabelling
added def PGame.RightMoves
added theorem PGame.Subsequent.trans
added def PGame.Subsequent
added theorem PGame.add_assoc_equiv
added theorem PGame.add_comm_equiv
added theorem PGame.add_comm_le
added theorem PGame.add_congr
added theorem PGame.add_congr_left
added theorem PGame.add_congr_right
added theorem PGame.add_lf_add_left
added theorem PGame.add_lf_add_right
added theorem PGame.add_moveLeft_inl
added theorem PGame.add_moveLeft_inr
added theorem PGame.add_zero_equiv
added theorem PGame.equiv_congr_left
added theorem PGame.equiv_of_eq
added theorem PGame.equiv_refl
added theorem PGame.equiv_rfl
added theorem PGame.fuzzy_congr
added theorem PGame.fuzzy_congr_imp
added theorem PGame.fuzzy_congr_left
added theorem PGame.fuzzy_irrefl
added theorem PGame.isOption_neg
added theorem PGame.isOption_neg_neg
added 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
added theorem PGame.le_iff_forall_lf
added theorem PGame.le_neg_iff
added theorem PGame.le_of_forall_lf
added theorem PGame.le_of_forall_lt
added theorem PGame.le_or_gf
added theorem PGame.le_zero
added theorem PGame.le_zero_lf
added theorem PGame.leftMoves_add
added theorem PGame.leftMoves_mk
added theorem PGame.leftMoves_neg
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_iff_exists_le
added theorem PGame.lf_irrefl
added theorem PGame.lf_mk
added theorem PGame.lf_mk_of_le
added theorem PGame.lf_moveRight
added theorem PGame.lf_neg_iff
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
added theorem PGame.lt_congr_imp
added theorem PGame.lt_congr_left
added theorem PGame.lt_congr_right
added theorem PGame.lt_iff_le_and_lf
added theorem PGame.lt_iff_sub_pos
added theorem PGame.lt_neg_iff
added theorem PGame.lt_of_le_of_lf
added theorem PGame.mk_le_mk
added theorem PGame.mk_lf
added theorem PGame.mk_lf_mk
added theorem PGame.mk_lf_of_le
added def PGame.moveLeft
added theorem PGame.moveLeft_lf
added theorem PGame.moveLeft_mk
added theorem PGame.moveLeft_neg'
added theorem PGame.moveLeft_neg
added def PGame.moveRecOn
added def PGame.moveRight
added theorem PGame.moveRight_mk
added theorem PGame.moveRight_neg'
added theorem PGame.moveRight_neg
added def PGame.neg
added theorem PGame.neg_add_le
added theorem PGame.neg_def
added theorem PGame.neg_equiv_iff
added theorem PGame.neg_fuzzy_iff
added theorem PGame.neg_le_iff
added theorem PGame.neg_le_neg_iff
added theorem PGame.neg_le_zero_iff
added theorem PGame.neg_lf_iff
added theorem PGame.neg_lf_neg_iff
added theorem PGame.neg_lf_zero_iff
added theorem PGame.neg_lt_iff
added theorem PGame.neg_lt_neg_iff
added theorem PGame.neg_lt_zero_iff
added theorem PGame.neg_ofLists
added theorem PGame.neg_star
added theorem PGame.not_fuzzy_of_ge
added theorem PGame.not_fuzzy_of_le
added theorem PGame.not_lf
added def PGame.ofLists
added theorem PGame.ofLists_moveLeft
added theorem PGame.one_leftMoves
added theorem PGame.one_moveLeft
added theorem PGame.one_rightMoves
added def PGame.relabel
added theorem PGame.relabel_moveLeft
added theorem PGame.rightMoves_add
added theorem PGame.rightMoves_mk
added theorem PGame.rightMoves_neg
added def PGame.star
added theorem PGame.star_fuzzy_zero
added theorem PGame.star_leftMoves
added theorem PGame.star_moveLeft
added theorem PGame.star_moveRight
added theorem PGame.star_rightMoves
added theorem PGame.sub_congr
added theorem PGame.sub_congr_left
added theorem PGame.sub_congr_right
added theorem PGame.sub_self_equiv
added theorem PGame.sub_zero
added theorem PGame.wf_isOption
added theorem PGame.wf_subsequent
added theorem PGame.zero_add_equiv
added theorem PGame.zero_le
added theorem PGame.zero_le_lf
added theorem PGame.zero_le_neg_iff
added theorem PGame.zero_leftMoves
added theorem PGame.zero_lf
added theorem PGame.zero_lf_le
added theorem PGame.zero_lf_neg_iff
added theorem PGame.zero_lf_one
added theorem PGame.zero_lt_neg_iff
added theorem PGame.zero_rightMoves
added inductive PGame