LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.Zero.PreLift #

Auxiliary declarations for the Borel determinacy formalization.

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

Auxiliary declaration for the Borel determinacy formalization.

x : ↥G.tree
Auxiliary declaration for the Borel determinacy formalization.
hlvl : 2 * k < (↑self.x).length
R : ResStrategy (gameAsTrees hyp) Player.zero (2 * k)
Auxiliary declaration for the Borel determinacy formalization.

Instances For

theorem GaleStewartGame.BorelDet.Zero.PreLift.ext {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : PreLift hyp} :

x.x = y.x → ∀ (R : x.R = y.R), x = y

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.ext_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : PreLift hyp} :

x = y ↔ x.x = y.x ∧ x.R = y.R

source

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

2 * k + 1 ≤ (↑H.x).length

Auxiliary declaration for the Borel determinacy formalization.

source

@[simp]

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

2 * k ≤ (↑H.x).length

source

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

(↑(Descriptive.Tree.pInv (treeHom hyp) (Descriptive.Tree.take (2 * k) H.x) ⋯)).length = 2 * k

source

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

IsPosition (↑(Descriptive.Tree.pInv (treeHom hyp) (Descriptive.Tree.take (2 * k) H.x) ⋯)) Player.zero

source

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

(↑(Descriptive.Tree.pInv (treeHom hyp) (Descriptive.Tree.take (2 * k) H.x) ⋯)).length ≤ 2 * k

source

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

↥(gameTree hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.liftShort = (H.R (Descriptive.Tree.pInv (GaleStewartGame.BorelDet.treeHom hyp) (Descriptive.Tree.take (2 * k) H.x) ⋯) ⋯ ⋯).valT'

Instances For

source

@[simp]

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

(↑H.liftShort).length = 2 * k + 1

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.getTree_fair {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) {y : List A} {a : A} (hy : y ∈ getTree' hyp ↑H.liftShort) (hp : IsPosition y Player.zero) (ha : List.map Prod.fst ↑H.liftShort ++ (y ++ [a]) ∈ G.tree) :

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

source

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

Game A

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.game = { tree := GaleStewartGame.BorelDet.getTree' hyp ↑H.liftShort, payoff := Subtype.val ⁻¹' Subtype.val '' (G.residual (List.take (2 * k + 1) ↑H.x)).payoffᶜ }

Instances For

source

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

H.game.payoff = Subtype.val ⁻¹' Subtype.val '' (G.residual (List.take (2 * k + 1) ↑H.x)).payoffᶜ

source

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

H.game.tree = getTree' hyp ↑H.liftShort

source

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

H.game.tree ≤ Descriptive.Tree.subAt G.tree (List.map Prod.fst ↑H.liftShort)

source

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

Descriptive.Tree.IsPruned H.game.tree

source

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

IsClosed H.game.payoff

source

def GaleStewartGame.BorelDet.Zero.PreLift.take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (n : ℕ) (h : 2 * k < n) :

PreLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.take n h = { x := Descriptive.Tree.take n H.x, hlvl := ⋯, R := H.R }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.take_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (n : ℕ) (h : 2 * k < n) :

(H.take n h).x = Descriptive.Tree.take n H.x

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.take_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (n : ℕ) (h : 2 * k < n) :

(H.take n h).R = H.R

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.take_of_length_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : PreLift hyp) {h : 2 * k < n} (h' : (↑H.x).length ≤ n) :

H.take n h = H

source

@[simp]

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

H.take (↑H.x).length ⋯ = H

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.take_trans {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {m n : ℕ} (H : PreLift hyp) (hm : 2 * k < m) (hn : 2 * k < n) :

(H.take m hm).take n hn = H.take (min m n) ⋯

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.liftShort_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : PreLift hyp) (h : 2 * k < n) :

(H.take n h).liftShort = H.liftShort

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.game_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : PreLift hyp) (h : 2 * k < n) :

(H.take n h).game = H.game

source

@[implicit_reducible]

instance GaleStewartGame.BorelDet.Zero.PreLift.instLE {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

LE (PreLift hyp)

Equations

GaleStewartGame.BorelDet.Zero.PreLift.instLE = { le := fun (p q : GaleStewartGame.BorelDet.Zero.PreLift hyp) => q.take (↑p.x).length ⋯ = p }

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.le_def {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (p q : PreLift hyp) :

(p ≤ q) = (q.take (↑p.x).length ⋯ = p)

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.length_mono {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {p q : PreLift hyp} (h : p ≤ q) :

(↑p.x).length ≤ (↑q.x).length

source

@[implicit_reducible]

instance GaleStewartGame.BorelDet.Zero.PreLift.instPartialOrder {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

PartialOrder (PreLift hyp)

Equations

One or more equations did not get rendered due to their size.

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.take_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : PreLift hyp) {h : 2 * k < n} :

H.take n h ≤ H

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.take_le_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {m n : ℕ} (H : PreLift hyp) (hm : 2 * k < m) (hn : 2 * k < n) :

H.take m hm ≤ H.take n hn ↔ m ≤ n ∨ (↑H.x).length ≤ n

source

def GaleStewartGame.BorelDet.Zero.PreLift.ConShort {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.ConShort = ((↑H.x)[2 * k] = (↑H.liftShort)[2 * k].1)

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.PreLift.conShort_iff_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : PreLift hyp) (h : 2 * k < n) :

(H.take n h).ConShort ↔ H.ConShort

Auxiliary declaration for the Borel determinacy formalization.

source

def GaleStewartGame.BorelDet.Zero.PreLift.ConLong {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.ConLong = (List.drop (2 * k + 1) ↑H.x ∈ H.game.tree)

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.PreLift.conLong_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : PreLift hyp) {h : 2 * k < n} (h' : H.ConLong) :

(H.take n h).ConLong

source

structure GaleStewartGame.BorelDet.Zero.Lift {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.Zero.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.zero (2 * k)
h'lvl : 2 * k + 1 < (↑self.x).length
conShort : self.ConShort

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.Lift.ext_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : Lift hyp} :

x = y ↔ x.toPreLift = y.toPreLift

source

theorem GaleStewartGame.BorelDet.Zero.Lift.ext {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : Lift hyp} (toPreLift : x.toPreLift = y.toPreLift) :

x = y

source

@[implicit_reducible]

instance GaleStewartGame.BorelDet.Zero.instPartialOrderLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

PartialOrder (Lift hyp)

Equations

One or more equations did not get rendered due to their size.

source

def GaleStewartGame.BorelDet.Zero.Lift.Lost' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.Lost' = G.WonPosition (↑H.x) (GaleStewartGame.Player.residual (↑H.x) GaleStewartGame.Player.one)

Instances For

source

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

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.Losable = (H.ConLong ∧ GaleStewartGame.PreStrategy.WinningPrefix H.game GaleStewartGame.Player.one (List.drop (2 * k + 1) ↑H.x))

Instances For

source

def GaleStewartGame.BorelDet.Zero.Lift.Winnable {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.Winnable = ¬GaleStewartGame.PreStrategy.WinningPrefix H.game GaleStewartGame.Player.one (List.drop (2 * k + 1) ↑H.x)

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.Lift.Winnable.conLong {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : H.Winnable) :

H.ConLong

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.h'lvl_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

2 * k + 2 ≤ (↑H.x).length

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.liftShort_val_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

List.map Prod.fst ↑H.liftShort = List.take (2 * k + 1) ↑H.x

source

theorem GaleStewartGame.BorelDet.Zero.Lift.liftShort_lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

(CategoryTheory.ConcreteCategory.hom (treeHom hyp)) H.liftShort = Descriptive.Tree.take (2 * k + 1) H.x

source

def GaleStewartGame.BorelDet.Zero.Lift.liftNode {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.liftNode = (↑H.x)[2 * k + 1]

Instances For

source

def GaleStewartGame.BorelDet.Zero.Lift.take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (n : ℕ) (h : 2 * k + 2 ≤ n) :

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.take n h = { toPreLift := H.take n ⋯, h'lvl := ⋯, conShort := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.take_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (n : ℕ) (h : 2 * k + 2 ≤ n) :

(H.take n h).toPreLift = H.take n ⋯

source

theorem GaleStewartGame.BorelDet.Zero.Lift.take_of_length_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : Lift hyp) {h : 2 * k + 2 ≤ n} (h' : (↑H.x).length ≤ n) :

H.take n h = H

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.take_rfl {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) :

H.take (↑H.x).length ⋯ = H

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.take_trans {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {m n : ℕ} (H : Lift hyp) (hm : 2 * k + 2 ≤ m) (hn : 2 * k + 2 ≤ n) :

(H.take m hm).take n hn = H.take (min m n) ⋯

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.Lift.liftNode_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : Lift hyp) (h : 2 * k + 2 ≤ n) :

(H.take n h).liftNode = H.liftNode

source

theorem GaleStewartGame.BorelDet.Zero.Lift.eq_take_of_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {p q : Lift hyp} (h : p ≤ q) :

q.take (↑p.x).length ⋯ = p

source

theorem GaleStewartGame.BorelDet.Zero.Lift.take_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : Lift hyp) {h : 2 * k + 2 ≤ n} :

H.take n h ≤ H

source

theorem GaleStewartGame.BorelDet.Zero.Lift.take_le_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {m n : ℕ} (H : Lift hyp) (hm : 2 * k + 2 ≤ m) (hn : 2 * k + 2 ≤ n) :

H.take m hm ≤ H.take n hn ↔ m ≤ n ∨ (↑H.x).length ≤ n

source

structure GaleStewartGame.BorelDet.Zero.WLLift {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.Zero.Lift 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.zero (2 * k)
h'lvl : 2 * k + 1 < (↑self.x).length
conShort : self.ConShort
liftTree : ↥(Descriptive.tree A)
Auxiliary declaration for the Borel determinacy formalization.

Instances For

source

theorem GaleStewartGame.BorelDet.Zero.WLLift.ext {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : WLLift hyp} (toLift : x.toLift = y.toLift) (liftTree : x.liftTree = y.liftTree) :

x = y

source

theorem GaleStewartGame.BorelDet.Zero.WLLift.ext_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : WLLift hyp} :

x = y ↔ x.toLift = y.toLift ∧ x.liftTree = y.liftTree

source

@[implicit_reducible]

instance GaleStewartGame.BorelDet.Zero.instPreorderWLLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} :

Preorder (WLLift hyp)

Equations

GaleStewartGame.BorelDet.Zero.instPreorderWLLift = { le := fun (p q : GaleStewartGame.BorelDet.Zero.WLLift hyp) => p.toLift ≤ q.toLift, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

source

noncomputable def GaleStewartGame.BorelDet.Zero.WLLift.liftMediumVal {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

List (upA hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.liftMediumVal = ↑H.liftShort ++ [(H.liftNode, H.liftTree)]

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftMediumVal_length {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

H.liftMediumVal.length = 2 * k + 2

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.getTree_liftMediumVal {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

getTree' hyp H.liftMediumVal = H.liftTree

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftMediumVal_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

List.map Prod.fst H.liftMediumVal = List.take (2 * k + 2) ↑H.x

source

noncomputable def GaleStewartGame.BorelDet.Zero.WLLift.liftVal {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

List (upA hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.liftVal = H.liftMediumVal ++ (List.drop (2 * k + 2) ↑H.x).zipInitsMap fun (a : A) (y : List A) => (a, Descriptive.Tree.subAt H.liftTree y)

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftVal_take_medium {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

List.take (2 * k + 2) H.liftVal = H.liftMediumVal

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftVal_take_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

List.take (2 * k + 1) H.liftVal = ↑H.liftShort

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftVal_lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

List.map Prod.fst H.liftVal = ↑H.x

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftVal_length {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift hyp) :

H.liftVal.length = (↑H.x).length

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftVal_lift_get {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {n : ℕ} (H : WLLift hyp) (h : n < H.liftVal.length) :

H.liftVal[n].1 = (↑H.x)[n]

source

theorem GaleStewartGame.BorelDet.Zero.WLLift.liftVal_take_eq_of_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : WLLift hyp} (h : H ≤ H') (ht : H.liftTree = H'.liftTree) :

H.liftVal = List.take (↑H.x).length H'.liftVal

source

structure GaleStewartGame.BorelDet.Zero.WLLift' {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.Zero.WLLift 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.zero (2 * k)
h'lvl : 2 * k + 1 < (↑self.x).length
conShort : self.ConShort
liftTree : ↥(Descriptive.tree A)
hlift : self.liftVal ∈ gameTree hyp

Instances For

source

noncomputable def GaleStewartGame.BorelDet.Zero.WLLift'.lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) :

↥(gameTree hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.lift = ⟨H.liftVal, ⋯⟩

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.lift_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) :

↑H.lift = H.liftVal

source

theorem GaleStewartGame.BorelDet.Zero.WLLift'.lift_lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) :

(CategoryTheory.ConcreteCategory.hom (treeHom hyp)) H.lift = H.x

source

noncomputable def GaleStewartGame.BorelDet.Zero.WLLift'.extension {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑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.Zero.WLLift'.extensionMap {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑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.Zero.WLLift'.extension_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

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

source

@[simp]

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

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

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extension_take_medium {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

List.take (2 * k + 2) (H.extension hp R).val' = H.liftMediumVal

source

noncomputable def GaleStewartGame.BorelDet.Zero.WLLift'.extensionPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

PreLift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extensionPreLift_x {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

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

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extensionPreLift_R {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

(H.extensionPreLift hp R).R = H.R

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extensionPreLift_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

(H.extensionPreLift hp R).take (↑H.x).length ⋯ = H.toPreLift

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extensionPreLift_liftShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

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

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extensionPreLift_game {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

(H.extensionPreLift hp R).game = H.game

source

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

Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

H.extensionLift hp R = { toPreLift := H.extensionPreLift hp R, h'lvl := ⋯, conShort := ⋯ }

Instances For

source

@[simp]

theorem GaleStewartGame.BorelDet.Zero.WLLift'.extensionLift_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : WLLift' hyp) (hp : IsPosition (↑H.x) Player.zero) (R : ResStrategy (gameAsTrees hyp) Player.zero (↑H.x).length) :

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

source

@[simp]

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

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