Impartial

📁 Source: Mathlib/SetTheory/Game/Impartial.lean

Statistics

Metric	Count
Definitions `Impartial`	1
Theorems `add_self`, `equiv_iff_add_equiv_zero`, `equiv_iff_add_equiv_zero'`, `equiv_or_fuzzy_zero`, `equiv_zero_iff_ge`, `equiv_zero_iff_le`, `exists_left_move_equiv_iff_fuzzy_zero`, `exists_right_move_equiv_iff_fuzzy_zero`, `forall_leftMoves_fuzzy_iff_equiv_zero`, `forall_rightMoves_fuzzy_iff_equiv_zero`, `fuzzy_zero_iff_gf`, `fuzzy_zero_iff_lf`, `impartial_add`, `impartial_congr`, `impartial_neg`, `impartial_star`, `impartial_zero`, `le_zero_iff`, `lf_zero_iff`, `mk'_add_self`, `mk'_neg_equiv_self`, `moveLeft_impartial`, `moveRight_impartial`, `neg_equiv_self`, `nonneg`, `nonpos`, `not_equiv_zero_iff`, `not_fuzzy_zero_iff`, `out`, `impartial_def`	30
Total	31

SetTheory.PGame

Definitions

Name	Category	Theorems
`Impartial` 📖	CompData	9 math math: `impartial_nim`, `Impartial.impartial_star`, `Impartial.moveRight_impartial`, `Impartial.moveLeft_impartial`, `impartial_def`, `Impartial.impartial_neg`, `Impartial.impartial_congr`, `Impartial.impartial_add`, `Impartial.impartial_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`impartial_def` 📖	mathematical	—	`Impartial` `SetTheory.PGame` `setoid` `instNeg` `moveLeft` `moveRight`	—	—

SetTheory.PGame.Impartial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_self` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instAdd` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.Equiv.trans` `SetTheory.PGame.add_congr_left` `neg_equiv_self` `SetTheory.PGame.neg_add_cancel_equiv`
`equiv_iff_add_equiv_zero` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instAdd` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.equiv_iff_game_eq` `add_right_cancel_iff` `AddRightCancelSemigroup.toIsRightCancelAdd` `mk'_add_self` `SetTheory.PGame.quot_add` `SetTheory.PGame.quot_zero`
`equiv_iff_add_equiv_zero'` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instAdd` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.equiv_iff_game_eq` `add_left_cancel_iff` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `mk'_add_self` `SetTheory.PGame.quot_add` `SetTheory.PGame.quot_zero`
`equiv_or_fuzzy_zero` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instZero` `SetTheory.PGame.Fuzzy`	—	`SetTheory.PGame.lt_or_equiv_or_gt_or_fuzzy` `nonneg` `nonpos`
`equiv_zero_iff_ge` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instZero` `SetTheory.PGame.le`	—	`le_zero_iff`
`equiv_zero_iff_le` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instZero` `SetTheory.PGame.le`	—	`le_zero_iff`
`exists_left_move_equiv_iff_fuzzy_zero` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.moveLeft` `SetTheory.PGame.instZero` `SetTheory.PGame.Fuzzy`	—	`fuzzy_zero_iff_gf` `SetTheory.PGame.lf_of_le_moveLeft` `SetTheory.PGame.zero_lf_le` `equiv_zero_iff_ge` `moveLeft_impartial`
`exists_right_move_equiv_iff_fuzzy_zero` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.moveRight` `SetTheory.PGame.instZero` `SetTheory.PGame.Fuzzy`	—	`fuzzy_zero_iff_lf` `SetTheory.PGame.lf_of_moveRight_le` `SetTheory.PGame.lf_zero_le` `equiv_zero_iff_le` `moveRight_impartial`
`forall_leftMoves_fuzzy_iff_equiv_zero` 📖	mathematical	—	`SetTheory.PGame.Fuzzy` `SetTheory.PGame.moveLeft` `SetTheory.PGame` `SetTheory.PGame.instZero` `SetTheory.PGame.setoid`	—	`equiv_zero_iff_le` `SetTheory.PGame.le_zero_lf` `fuzzy_zero_iff_lf` `moveLeft_impartial` `LE.le.moveLeft_lf`
`forall_rightMoves_fuzzy_iff_equiv_zero` 📖	mathematical	—	`SetTheory.PGame.Fuzzy` `SetTheory.PGame.moveRight` `SetTheory.PGame` `SetTheory.PGame.instZero` `SetTheory.PGame.setoid`	—	`equiv_zero_iff_ge` `SetTheory.PGame.zero_le_lf` `fuzzy_zero_iff_gf` `moveRight_impartial` `LE.le.lf_moveRight`
`fuzzy_zero_iff_gf` 📖	mathematical	—	`SetTheory.PGame.Fuzzy` `SetTheory.PGame` `SetTheory.PGame.instZero` `SetTheory.PGame.LF`	—	`lf_zero_iff`
`fuzzy_zero_iff_lf` 📖	mathematical	—	`SetTheory.PGame.Fuzzy` `SetTheory.PGame` `SetTheory.PGame.instZero` `SetTheory.PGame.LF`	—	`lf_zero_iff`
`impartial_add` 📖	mathematical	—	`SetTheory.PGame.Impartial` `SetTheory.PGame` `SetTheory.PGame.instAdd`	—	—
`impartial_congr` 📖	mathematical	—	`SetTheory.PGame.Impartial`	—	—
`impartial_neg` 📖	mathematical	—	`SetTheory.PGame.Impartial` `SetTheory.PGame` `SetTheory.PGame.instNeg`	—	—
`impartial_star` 📖	mathematical	—	`SetTheory.PGame.Impartial` `SetTheory.PGame.star`	—	`SetTheory.PGame.impartial_def` `SetTheory.PGame.neg_star` `impartial_zero`
`impartial_zero` 📖	mathematical	—	`SetTheory.PGame.Impartial` `SetTheory.PGame` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.impartial_def` `neg_zero` `PEmpty.instIsEmpty`
`le_zero_iff` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.le` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.zero_le_neg_iff` `SetTheory.PGame.le_congr_right` `neg_equiv_self`
`lf_zero_iff` 📖	mathematical	—	`SetTheory.PGame.LF` `SetTheory.PGame` `SetTheory.PGame.instZero`	—	`SetTheory.PGame.zero_lf_neg_iff` `SetTheory.PGame.lf_congr_right` `neg_equiv_self`
`mk'_add_self` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.Game.instAdd` `SetTheory.Game.instZero`	—	`SetTheory.PGame.game_eq` `add_self`
`mk'_neg_equiv_self` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.Game.instNeg`	—	`SetTheory.PGame.game_eq` `SetTheory.PGame.Equiv.symm` `neg_equiv_self`
`moveLeft_impartial` 📖	mathematical	—	`SetTheory.PGame.Impartial` `SetTheory.PGame.moveLeft`	—	`SetTheory.PGame.impartial_def`
`moveRight_impartial` 📖	mathematical	—	`SetTheory.PGame.Impartial` `SetTheory.PGame.moveRight`	—	`SetTheory.PGame.impartial_def`
`neg_equiv_self` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instNeg`	—	`SetTheory.PGame.impartial_def`
`nonneg` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.instZero`	—	`nonpos` `impartial_neg`
`nonpos` 📖	mathematical	—	`SetTheory.PGame` `Preorder.toLT` `SetTheory.PGame.instPreorder` `SetTheory.PGame.instZero`	—	`lt_asymm` `SetTheory.PGame.neg_lt_neg_iff` `neg_zero` `SetTheory.PGame.lt_congr_right` `neg_equiv_self`
`not_equiv_zero_iff` 📖	mathematical	—	`SetTheory.PGame` `SetTheory.PGame.setoid` `SetTheory.PGame.instZero` `SetTheory.PGame.Fuzzy`	—	`equiv_or_fuzzy_zero` `SetTheory.PGame.Fuzzy.not_equiv`
`not_fuzzy_zero_iff` 📖	mathematical	—	`SetTheory.PGame.Fuzzy` `SetTheory.PGame` `SetTheory.PGame.instZero` `SetTheory.PGame.setoid`	—	`equiv_or_fuzzy_zero` `SetTheory.PGame.Equiv.not_fuzzy`
`out` 📖	—	—	—	—	—

---

← Back to Index