Documentation Verification Report

State

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

Statistics

Metric	Count
Definitions `State`, `State`, `State`, `State`, `State`, `ofState`, `State`, `l`, `r`, `turnBound`, `fintypeLeftMovesOfStateAux`, `fintypeRightMovesOfStateAux`, `leftMovesOfState`, `leftMovesOfStateAux`, `ofState`, `ofStateAux`, `ofStateAuxRelabelling`, `relabellingMoveLeft`, `relabellingMoveLeftAux`, `relabellingMoveRight`, `relabellingMoveRightAux`, `rightMovesOfState`, `rightMovesOfStateAux`, `shortOfState`, `shortOfStateAux`	25
Theorems `left_bound`, `right_bound`, `turnBound_ne_zero_of_left_move`, `turnBound_ne_zero_of_right_move`, `turnBound_of_left`, `turnBound_of_right`	6
Total	31

Lean.Export

Definitions

Name	Category	Theorems
`State` 📖	CompData	—

Mathlib.Meta.FunProp

Definitions

Name	Category	Theorems
`State` 📖	CompData	—

Mathlib.PrintSorries

Definitions

Name	Category	Theorems
`State` 📖	CompData	—

Mathlib.Tactic.AtomM

Definitions

Name	Category	Theorems
`State` 📖	CompData	—

Mathlib.Tactic.BicategoryLike

Definitions

Name	Category	Theorems
`State` 📖	CompData	—

SetTheory.Game

Definitions

Name	Category	Theorems
`ofState` 📖	CompOp	—

SetTheory.PGame

Definitions

Name	Category	Theorems
`State` 📖	CompData	—
`fintypeLeftMovesOfStateAux` 📖	CompOp	—
`fintypeRightMovesOfStateAux` 📖	CompOp	—
`leftMovesOfState` 📖	CompOp	—
`leftMovesOfStateAux` 📖	CompOp	—
`ofState` 📖	CompOp	—
`ofStateAux` 📖	CompOp	—
`ofStateAuxRelabelling` 📖	CompOp	—
`relabellingMoveLeft` 📖	CompOp	—
`relabellingMoveLeftAux` 📖	CompOp	—
`relabellingMoveRight` 📖	CompOp	—
`relabellingMoveRightAux` 📖	CompOp	—
`rightMovesOfState` 📖	CompOp	—
`rightMovesOfStateAux` 📖	CompOp	—
`shortOfState` 📖	CompOp	—
`shortOfStateAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`turnBound_ne_zero_of_left_move` 📖	—	`Finset` `Finset.instMembership` `State.l`	—	—	`State.left_bound`
`turnBound_ne_zero_of_right_move` 📖	—	`Finset` `Finset.instMembership` `State.r`	—	—	`State.right_bound`
`turnBound_of_left` 📖	—	`Finset` `Finset.instMembership` `State.l` `State.turnBound`	—	—	`State.left_bound`
`turnBound_of_right` 📖	—	`Finset` `Finset.instMembership` `State.r` `State.turnBound`	—	—	`State.right_bound`

SetTheory.PGame.State

Definitions

Name	Category	Theorems
`l` 📖	CompOp	—
`r` 📖	CompOp	—
`turnBound` 📖	CompOp	2 math math: `left_bound`, `right_bound`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_bound` 📖	mathematical	`Finset` `Finset.instMembership` `l`	`turnBound`	—	—
`right_bound` 📖	mathematical	`Finset` `Finset.instMembership` `r`	`turnBound`	—	—

---

← Back to Index