LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.Lift #

Auxiliary declarations for the Borel determinacy formalization.

noncomputable def GaleStewartGame.BorelDet.One.Lift'.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

Descriptive.Tree.ExtensionsAt H.lift

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extension hp R = R H.lift ⋯ ⋯

Instances For

source

noncomputable def GaleStewartGame.BorelDet.One.Lift'.extensionMap {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

Descriptive.Tree.ExtensionsAt H.x

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extensionMap hp R = Descriptive.Tree.ExtensionsAt.map (GaleStewartGame.BorelDet.treeHom hyp) ⋯ (H.extension hp R)

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extension_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

List.take (↑H.x).length (H.extension hp R).val' = H.liftVal

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionMap_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) (h : n ≤ (↑H.x).length) :

List.take n (H.extensionMap hp R).val' = List.take n ↑H.x

source

noncomputable def GaleStewartGame.BorelDet.One.Lift'.extensionLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extensionLift hp R = { x := (H.extensionMap hp R).valT', hlvl := ⋯, R := H.R, liftTree := H.liftTree, htree := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift_liftTree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

(H.extensionLift hp R).liftTree = H.liftTree

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

(H.extensionLift hp R).x = (H.extensionMap hp R).valT'

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

(H.extensionLift hp R).R = H.R

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

(H.extensionLift hp R).take (↑H.x).length ⋯ = H.toLift

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift_liftShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

(H.extensionLift hp R).liftShort = H.liftShort

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift_wonPos {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

(H.extensionLift hp R).WonPos = H.WonPos

source

noncomputable def GaleStewartGame.BorelDet.One.Lift'.extensionLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) (hR : ResStrategy.res ⋯ R = H.R) :

Lift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extensionLift' hp R hR = { toLift := H.extensionLift hp R, con := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift'_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) (hR : ResStrategy.res ⋯ R = H.R) :

(H.extensionLift' hp R hR).toLift = H.extensionLift hp R

source

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift'_game {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) (hR : ResStrategy.res ⋯ R = H.R) :

(H.extensionLift' hp R hR).game = H.game

source

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.extensionLift'_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) (hR : ResStrategy.res ⋯ R = H.R) :

(H.extensionLift' hp R hR).take (↑H.x).length ⋯ = H

source

theorem GaleStewartGame.BorelDet.One.PreLift.Losable'.losable'_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : PreLift hyp} (hL : H'.Losable') (h : H ≤ H') :

H.Losable'

source

structure GaleStewartGame.BorelDet.One.PreLift.LLift {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.One.PreLift hyp :

Type u_1

Auxiliary declaration for the Borel determinacy formalization.

x : ↥G.tree
hlvl : 2 * k < (↑self.x).length
R : ResStrategy (gameAsTrees hyp) Player.one (2 * k + 1)
los : self.Losable'

Instances For

source

def GaleStewartGame.BorelDet.One.PreLift.LLift.S {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

QuasiStrategy H.game.tree Player.one

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.S = H.game.defensiveQuasi GaleStewartGame.Player.one ⋯

Instances For

source

theorem GaleStewartGame.BorelDet.One.PreLift.LLift.S_winning {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

H.S.fst.IsWinning

source

def GaleStewartGame.BorelDet.One.PreLift.LLift.toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.toLift = H.extend H.S

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.LLift.toLift_liftTree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

H.toLift.liftTree = H.S.fst.subtree

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.LLift.toLift_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

H.toLift.toPreLift = H.toPreLift

source

theorem GaleStewartGame.BorelDet.One.PreLift.LLift.toLift_mono {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : LLift hyp} (h : H.toPreLift ≤ H'.toPreLift) :

H.toLift.liftTree = H'.toLift.liftTree

source

theorem GaleStewartGame.BorelDet.One.PreLift.LLift.winning_condition {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) :

WinningCondition ↑H.toLift.liftShort ⋯

source

theorem GaleStewartGame.BorelDet.One.PreLift.LLift.concat_mem_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : LLift hyp) {y : List A} {a : A} (hp : IsPosition y Player.zero) (ha : List.take (2 * k + 1) ↑H.x ++ (↑H.toLift.liftShort)[2 * k + 1].1 :: (y ++ [a]) ∈ G.tree) (hy : y ∈ getTree' hyp ↑H.toLift.liftShort) (hw : ¬H.game.WinningPosition ((↑H.toLift.liftShort)[2 * k + 1].1 :: y ++ [a])) :

y ++ [a] ∈ getTree' hyp ↑H.toLift.liftShort

source

def GaleStewartGame.BorelDet.One.PreLift.Losable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) :

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.Losable = ∃ (h : H.Losable'), { toPreLift := H, los := h }.toLift.Con

Instances For

source

theorem GaleStewartGame.BorelDet.One.PreLift.Losable.losable_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : PreLift hyp} (hL : H'.Losable) (h : H ≤ H') :

H.Losable

source

def GaleStewartGame.BorelDet.One.PreLift.Losable.lift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Losable) :

Lift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.lift' = { toLift := { toPreLift := H, los := ⋯ }.toLift, con := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.Losable.lift'_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Losable) :

h.lift'.toLift = { toPreLift := H, los := ⋯ }.toLift

source

theorem GaleStewartGame.BorelDet.One.PreLift.Won.won_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : PreLift hyp} (hW : H.Won) (h : H ≤ H') :

H'.Won

source

structure GaleStewartGame.BorelDet.One.PreLift.WLift {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.One.PreLift hyp :

Type u_1

Auxiliary declaration for the Borel determinacy formalization.

x : ↥G.tree
hlvl : 2 * k < (↑self.x).length
R : ResStrategy (gameAsTrees hyp) Player.one (2 * k + 1)
won : self.Won

Instances For

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.Winnable

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.exists_prefix {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

∃ (n : ℕ) (h : 2 * k < n), (H.take n h).Won

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.WLift.minLength {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

ℕ

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.minLength = Nat.find ⋯

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.minLength_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.minLength ≤ (↑H.x).length

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.le_minLength {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

2 * k + 1 ≤ H.minLength

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.le_minLength' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

2 * k ≤ H.minLength

Auxiliary declaration for the Borel determinacy formalization.

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.lt_minLength {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

2 * k < H.minLength

Auxiliary declaration for the Borel determinacy formalization.

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.WLift.takeMin {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

PreLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.takeMin = H.take H.minLength ⋯

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.takeMin_x_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑H.takeMin.x = List.take H.minLength ↑H.x

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.takeMin_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.takeMin.R = H.R

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.takeMin_wonPos {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.takeMin.WonPos = H.WonPos

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.min_prefix {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.takeMin.Won

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.WLift.u {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑H.WonPos

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.u = ⟨Exists.choose ⋯, ⋯⟩

Instances For

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.WLift.S {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x)) Player.one

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.S = Exists.choose ⋯

Instances For

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.u_spec {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑H.u <+: List.drop (2 * k + 1) ↑H.takeMin.x

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.u_spec' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑H.u <+: List.drop (2 * k + 1) ↑H.x

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.u_nil {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑H.u ≠ []

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.getTree_liftShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

getTree' hyp ↑(H.extend H.S).liftShort = Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x ++ ↑H.u)) (↑H.u).tail

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.WLift.toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.toLift = H.extend H.S

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.toLift_liftTree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.toLift.liftTree = H.S.fst.subtree

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.toLift_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.toLift.toPreLift = H.toPreLift

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.u_zero {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

(↑H.u)[0] = (↑H.toLift.liftShort)[2 * k + 1].1

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.WLift.toLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

Lift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.toLift' = { toLift := H.toLift, con := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.toLift'_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.toLift'.toLift = H.toLift

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.hEq_fst {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} (x : PSigma β) (y : PSigma β') (h : α = α') (h' : β ≍ β') (h'' : x ≍ y) :

x.fst ≍ y.fst

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.minLength_eq_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : WLift hyp} (h : H.toPreLift ≤ H'.toPreLift) :

H.minLength = H'.minLength

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.takeMin_eq_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : WLift hyp} (h : H.toPreLift ≤ H'.toPreLift) :

H.takeMin = H'.takeMin

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.u_eq_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : WLift hyp} (h : H.toPreLift ≤ H'.toPreLift) :

H.u ≍ H'.u

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.u_min_prefix {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑{ toPreLift := H.takeMin, won := ⋯ }.u = ↑H.u

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.uprop' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

↑{ toPreLift := H.takeMin, won := ⋯ }.u ∈ H.takeMin.WonPos

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.uprop'_choose {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

Exists.choose ⋯ ≍ Exists.choose ⋯

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.toLift_liftTree' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLift hyp) :

H.toLift.liftTree = (Exists.choose ⋯).fst.subtree

source

theorem GaleStewartGame.BorelDet.One.PreLift.WLift.toLift_mono {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : WLift hyp} (h : H.toPreLift ≤ H'.toPreLift) :

H.toLift.liftTree = H'.toLift.liftTree

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.Won.lift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Won) :

Lift' hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.lift' = { toPreLift := H, won := h }.toLift'

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.Won.lift'_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Won) :

h.lift'.toLift = { toPreLift := H, won := h }.toLift

source

theorem GaleStewartGame.BorelDet.One.PreLift.Winnable.winnable_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : PreLift hyp} (hW : H.Winnable) (h : H ≤ H') :

H'.Winnable

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.Winnable.takeMin {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) :

PreLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.takeMin = H.take (2 * k + 1 + GaleStewartGame.PreStrategy.WinningPrefix.num h) ⋯

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.Winnable.takeMin_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) :

h.takeMin.R = H.R

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.Winnable.takeMin_x_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) :

↑h.takeMin.x = List.take (2 * k + 1 + PreStrategy.WinningPrefix.num h) ↑H.x

source

theorem GaleStewartGame.BorelDet.One.PreLift.Winnable.takeMin_winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) :

h.takeMin.Winnable

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.Winnable.x' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) :

↥(H.game.residual (List.take (PreStrategy.WinningPrefix.num h) (List.drop (2 * k + 1) ↑H.x))).tree

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.x' = ⟨List.drop (2 * k + 1 + GaleStewartGame.PreStrategy.WinningPrefix.num h) ↑H.x, ⋯⟩

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.Winnable.x'_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) :

↑h.x' = List.drop (2 * k + 1 + PreStrategy.WinningPrefix.num h) ↑H.x

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.Winnable.a {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) (hp : IsPosition (↑H.x) Player.one) :

Descriptive.Tree.ExtensionsAt h.x'

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.a hp = GaleStewartGame.PreStrategy.WinningPrefix.strat h h.x' ⋯

Instances For

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.Winnable.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Winnable) (hp : IsPosition (↑H.x) Player.one) :

Descriptive.Tree.ExtensionsAt H.x

Auxiliary declaration for the Borel determinacy formalization.

Equations

h.extension hp = ⟨↑(h.a hp), ⋯⟩

Instances For

source

noncomputable def GaleStewartGame.BorelDet.One.PreLift.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

Descriptive.Tree.ExtensionsAt H.x

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extension hp R = if h : H.Won then h.lift'.extensionMap hp R else if h : H.Winnable then h.extension hp else if h : H.Losable then h.lift'.extensionMap hp R else Classical.choice ⋯

Instances For

source

theorem GaleStewartGame.BorelDet.One.PreLift.extension_losable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H : PreLift hyp} (h : H.Losable) (hp : IsPosition (↑H.x) Player.one) (R : ResStrategy (gameAsTrees hyp) Player.one (↑H.x).length) :

H.extension hp R = h.lift'.extensionMap hp R