Documentation Verification Report

Domineering

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

Statistics

Metric	Count
Definitions `Board`, `left`, `moveLeft`, `moveRight`, `right`, `shiftRight`, `shiftUp`, `state`, `domineering`, `L`, `one`, `shortDomineering`, `shortL`, `shortOne`	14
Theorems `card_of_mem_left`, `card_of_mem_right`, `fst_pred_mem_erase_of_mem_right`, `mem_left`, `mem_right`, `moveLeft_card`, `moveLeft_smaller`, `moveRight_card`, `moveRight_smaller`, `shiftRight_apply`, `shiftRight_symm_apply`, `shiftUp_apply`, `shiftUp_symm_apply`, `snd_pred_mem_erase_of_mem_left`	14
Total	28

SetTheory.PGame

Definitions

Name	Category	Theorems
`domineering` 📖	CompOp	—
`shortDomineering` 📖	CompOp	—
`shortL` 📖	CompOp	—
`shortOne` 📖	CompOp	—

SetTheory.PGame.Domineering

Definitions

Name	Category	Theorems
`Board` 📖	CompOp	2 math math: `mem_right`, `mem_left`
`left` 📖	CompOp	1 math math: `mem_left`
`moveLeft` 📖	CompOp	2 math math: `moveLeft_smaller`, `moveLeft_card`
`moveRight` 📖	CompOp	2 math math: `moveRight_smaller`, `moveRight_card`
`right` 📖	CompOp	1 math math: `mem_right`
`shiftRight` 📖	CompOp	2 math math: `shiftRight_apply`, `shiftRight_symm_apply`
`shiftUp` 📖	CompOp	2 math math: `shiftUp_apply`, `shiftUp_symm_apply`
`state` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_of_mem_left` 📖	mathematical	`Finset` `Finset.instMembership` `left`	`Finset.card`	—	`Finset.mem_inter` `snd_pred_mem_erase_of_mem_left` `Finset.card_erase_lt_of_mem`
`card_of_mem_right` 📖	mathematical	`Finset` `Finset.instMembership` `right`	`Finset.card`	—	`Finset.mem_inter` `fst_pred_mem_erase_of_mem_right` `Finset.card_erase_lt_of_mem`
`fst_pred_mem_erase_of_mem_right` 📖	mathematical	`Finset` `Finset.instMembership` `right`	`Finset.erase`	—	`Finset.mem_erase_of_ne_of_mem` `pred_ne_self` `Int.instNontrivial` `mem_right`
`mem_left` 📖	mathematical	—	`Finset` `Finset.instMembership` `left` `Board`	—	`Finset.mem_inter` `Finset.mem_map_equiv`
`mem_right` 📖	mathematical	—	`Finset` `Finset.instMembership` `right` `Board`	—	`Finset.mem_inter` `Finset.mem_map_equiv`
`moveLeft_card` 📖	mathematical	`Finset` `Finset.instMembership` `left`	`Finset.card` `moveLeft`	—	`Finset.card_erase_of_mem` `snd_pred_mem_erase_of_mem_left` `Finset.mem_of_mem_inter_left` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `card_of_mem_left`
`moveLeft_smaller` 📖	mathematical	`Finset` `Finset.instMembership` `left`	`Finset.card` `moveLeft`	—	`moveLeft_card` `Nat.instAtLeastTwoHAddOfNat` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`moveRight_card` 📖	mathematical	`Finset` `Finset.instMembership` `right`	`Finset.card` `moveRight`	—	`Finset.card_erase_of_mem` `fst_pred_mem_erase_of_mem_right` `Finset.mem_of_mem_inter_left` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `card_of_mem_right`
`moveRight_smaller` 📖	mathematical	`Finset` `Finset.instMembership` `right`	`Finset.card` `moveRight`	—	`moveRight_card` `Nat.instAtLeastTwoHAddOfNat` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`shiftRight_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `shiftRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Int.instAddGroup`	—	—
`shiftRight_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shiftRight` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Int.instAddGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`shiftUp_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `shiftUp` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Int.instAddGroup`	—	—
`shiftUp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `shiftUp` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Int.instAddGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	—
`snd_pred_mem_erase_of_mem_left` 📖	mathematical	`Finset` `Finset.instMembership` `left`	`Finset.erase`	—	`Finset.mem_erase_of_ne_of_mem` `pred_ne_self` `Int.instNontrivial` `mem_left`

SetTheory.PGame.domineering

Definitions

Name	Category	Theorems
`L` 📖	CompOp	—
`one` 📖	CompOp	—

---

← Back to Index