Documentation
LeanPool
.
AFormalizationOfBorelDeterminacyInLean
.
Proof
Search
return to top
source
Imports
Init
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BorelDeterminacy
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.BuildLevelwise
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Covering
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringClosedGame
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringLim
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.WinAsap
LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero
Imported by
Proof index
#
Import-only index for the covering and unravelling proof of Borel determinacy.