Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-19 12:42
b9638579
View on Github →
feat: port SetTheory.Game.PGame (
#1512
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/SetTheory/Game/PGame.lean
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
theorem
PGame.IsOption.mk_right
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
def
PGame.Relabelling.addCongr
added
theorem
PGame.Relabelling.equiv
added
theorem
PGame.Relabelling.ge
added
def
PGame.Relabelling.isEmpty
added
theorem
PGame.Relabelling.le
added
def
PGame.Relabelling.leftMovesEquiv
added
def
PGame.Relabelling.mk'
added
theorem
PGame.Relabelling.mk'_leftMovesEquiv
added
theorem
PGame.Relabelling.mk'_rightMovesEquiv
added
theorem
PGame.Relabelling.mk_leftMovesEquiv
added
theorem
PGame.Relabelling.mk_rightMovesEquiv
added
def
PGame.Relabelling.moveLeft
added
def
PGame.Relabelling.moveLeftSymm
added
def
PGame.Relabelling.moveRight
added
def
PGame.Relabelling.moveRightSymm
added
def
PGame.Relabelling.negCongr
added
def
PGame.Relabelling.refl
added
def
PGame.Relabelling.rightMovesEquiv
added
def
PGame.Relabelling.subCongr
added
def
PGame.Relabelling.symm
added
def
PGame.Relabelling.trans
added
inductive
PGame.Relabelling
added
def
PGame.RightMoves
added
theorem
PGame.Subsequent.mk_left
added
theorem
PGame.Subsequent.mk_right'
added
theorem
PGame.Subsequent.mk_right
added
theorem
PGame.Subsequent.moveLeft
added
theorem
PGame.Subsequent.moveLeft_mk_left
added
theorem
PGame.Subsequent.moveLeft_mk_right
added
theorem
PGame.Subsequent.moveRight
added
theorem
PGame.Subsequent.moveRight_mk_left
added
theorem
PGame.Subsequent.moveRight_mk_right
added
theorem
PGame.Subsequent.trans
added
def
PGame.Subsequent
added
def
PGame.addAssocRelabelling
added
def
PGame.addCommRelabelling
added
def
PGame.addZeroRelabelling
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_left_neg_equiv
added
theorem
PGame.add_left_neg_le_zero
added
theorem
PGame.add_lf_add_left
added
theorem
PGame.add_lf_add_of_le_of_lf
added
theorem
PGame.add_lf_add_of_lf_of_le
added
theorem
PGame.add_lf_add_right
added
theorem
PGame.add_moveLeft_inl
added
theorem
PGame.add_moveLeft_inr
added
theorem
PGame.add_moveRight_inl
added
theorem
PGame.add_moveRight_inr
added
theorem
PGame.add_right_neg_equiv
added
theorem
PGame.add_right_neg_le_zero
added
theorem
PGame.add_zero_equiv
added
theorem
PGame.equiv_congr_left
added
theorem
PGame.equiv_congr_right
added
theorem
PGame.equiv_of_eq
added
theorem
PGame.equiv_of_mk_equiv
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_congr_right
added
theorem
PGame.fuzzy_irrefl
added
theorem
PGame.fuzzy_of_equiv_of_fuzzy
added
theorem
PGame.fuzzy_of_fuzzy_of_equiv
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_iff_sub_nonneg
added
theorem
PGame.le_neg_iff
added
theorem
PGame.le_of_equiv_of_le
added
theorem
PGame.le_of_forall_lf
added
theorem
PGame.le_of_forall_lt
added
theorem
PGame.le_of_le_of_equiv
added
theorem
PGame.le_or_gf
added
theorem
PGame.le_zero
added
theorem
PGame.le_zero_lf
added
theorem
PGame.le_zero_of_isEmpty_leftMoves
added
theorem
PGame.leftMoves_add
added
theorem
PGame.leftMoves_add_cases
added
theorem
PGame.leftMoves_mk
added
theorem
PGame.leftMoves_neg
added
theorem
PGame.leftMoves_ofLists
added
theorem
PGame.leftResponse_spec
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_iff_lt_or_fuzzy
added
theorem
PGame.lf_iff_sub_zero_lf
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_moveRight_of_le
added
theorem
PGame.lf_neg_iff
added
theorem
PGame.lf_of_equiv_of_lf
added
theorem
PGame.lf_of_fuzzy
added
theorem
PGame.lf_of_le_mk
added
theorem
PGame.lf_of_le_moveLeft
added
theorem
PGame.lf_of_le_of_lf
added
theorem
PGame.lf_of_lf_of_equiv
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_of_moveRight_le
added
theorem
PGame.lf_or_equiv_or_gf
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_equiv_of_lt
added
theorem
PGame.lt_of_le_of_lf
added
theorem
PGame.lt_of_lt_of_equiv
added
theorem
PGame.lt_or_equiv_of_le
added
theorem
PGame.lt_or_equiv_or_gf
added
theorem
PGame.lt_or_equiv_or_gt_or_fuzzy
added
theorem
PGame.lt_or_fuzzy_of_lf
added
theorem
PGame.mk_add_moveLeft_inl
added
theorem
PGame.mk_add_moveLeft_inr
added
theorem
PGame.mk_add_moveRight_inl
added
theorem
PGame.mk_add_moveRight_inr
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_lf_of_le
added
theorem
PGame.moveLeft_mk
added
theorem
PGame.moveLeft_neg'
added
theorem
PGame.moveLeft_neg
added
theorem
PGame.moveLeft_neg_symm'
added
theorem
PGame.moveLeft_neg_symm
added
def
PGame.moveRecOn
added
def
PGame.moveRight
added
theorem
PGame.moveRight_mk
added
theorem
PGame.moveRight_neg'
added
theorem
PGame.moveRight_neg
added
theorem
PGame.moveRight_neg_symm'
added
theorem
PGame.moveRight_neg_symm
added
def
PGame.neg
added
def
PGame.negAddRelabelling
added
theorem
PGame.neg_add_le
added
theorem
PGame.neg_def
added
theorem
PGame.neg_equiv_iff
added
theorem
PGame.neg_equiv_neg_iff
added
theorem
PGame.neg_equiv_zero_iff
added
theorem
PGame.neg_fuzzy_iff
added
theorem
PGame.neg_fuzzy_neg_iff
added
theorem
PGame.neg_fuzzy_zero_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.ofLists_moveLeft
added
theorem
PGame.ofLists_moveRight'
added
theorem
PGame.ofLists_moveRight
added
theorem
PGame.one_leftMoves
added
theorem
PGame.one_moveLeft
added
theorem
PGame.one_rightMoves
added
def
PGame.relabel
added
def
PGame.relabelRelabelling
added
theorem
PGame.relabel_moveLeft'
added
theorem
PGame.relabel_moveLeft
added
theorem
PGame.relabel_moveRight'
added
theorem
PGame.relabel_moveRight
added
theorem
PGame.rightMoves_add
added
theorem
PGame.rightMoves_add_cases
added
theorem
PGame.rightMoves_mk
added
theorem
PGame.rightMoves_neg
added
theorem
PGame.rightMoves_ofLists
added
theorem
PGame.rightResponse_spec
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
def
PGame.toLeftMovesAdd
added
def
PGame.toLeftMovesNeg
added
def
PGame.toOfListsLeftMoves
added
def
PGame.toOfListsRightMoves
added
def
PGame.toRightMovesAdd
added
def
PGame.toRightMovesNeg
added
theorem
PGame.wf_isOption
added
theorem
PGame.wf_subsequent
added
def
PGame.zeroAddRelabelling
added
theorem
PGame.zero_add_equiv
added
theorem
PGame.zero_equiv_neg_iff
added
theorem
PGame.zero_fuzzy_neg_iff
added
theorem
PGame.zero_le
added
theorem
PGame.zero_le_add_left_neg
added
theorem
PGame.zero_le_add_right_neg
added
theorem
PGame.zero_le_lf
added
theorem
PGame.zero_le_neg_iff
added
theorem
PGame.zero_le_of_isEmpty_rightMoves
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