LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.One.PreLift

Auxiliary declarations for the Borel determinacy formalization.

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

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.one (2 * k + 1)

  Auxiliary declaration for the Borel determinacy formalization.

theorem GaleStewartGame.BorelDet.One.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

theorem GaleStewartGame.BorelDet.One.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

theorem GaleStewartGame.BorelDet.One.PreLift.hlvl_le {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : 2 * k + 1 ≤ (↑H.x).length

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.hlvl' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : 2 * k ≤ (↑H.x).length

theorem GaleStewartGame.BorelDet.One.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

theorem GaleStewartGame.BorelDet.One.PreLift.gameTree_eq {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : Descriptive.Tree.subAt (getTree' hyp ↑(Descriptive.Tree.pInv (treeHom hyp) (Descriptive.Tree.take (2 * k) H.x) ⋯)) [(↑H.x)[2 * k]] = Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x)

def GaleStewartGame.BorelDet.One.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 }

@[simp]

theorem GaleStewartGame.BorelDet.One.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

@[simp]

theorem GaleStewartGame.BorelDet.One.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

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

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.take_rfl {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : H.take (↑H.x).length ⋯ = H

@[simp]

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

@[implicit_reducible]

instance GaleStewartGame.BorelDet.One.PreLift.instLE {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} : LE (PreLift hyp)

Equations

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

@[simp]

theorem GaleStewartGame.BorelDet.One.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)

theorem GaleStewartGame.BorelDet.One.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

@[implicit_reducible]

instance GaleStewartGame.BorelDet.One.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.

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

theorem GaleStewartGame.BorelDet.One.PreLift.take_le_take {A : Type u_1} {G : Game A} {k m n : ℕ} {hyp : Hyp G k} (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

structure GaleStewartGame.BorelDet.One.Lift {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)
• liftTree : ↥(Descriptive.tree A)

  Auxiliary declaration for the Borel determinacy formalization.

• htree : ∃ (S : QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑self.x)) Player.one), self.liftTree = S.fst.subtree

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

theorem GaleStewartGame.BorelDet.One.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 ∧ x.liftTree = y.liftTree

@[implicit_reducible]

instance GaleStewartGame.BorelDet.One.instPreorderLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} : Preorder (Lift hyp)

Equations

• GaleStewartGame.BorelDet.One.instPreorderLift = { le := fun (p q : GaleStewartGame.BorelDet.One.Lift hyp) => p.toPreLift ≤ q.toPreLift, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[simp]

theorem GaleStewartGame.BorelDet.One.le_def {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (p q : Lift hyp) : (p ≤ q) = (p.toPreLift ≤ q.toPreLift)

@[simp]

theorem GaleStewartGame.BorelDet.One.lt_def {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (a b : Lift hyp) : (a < b) = ((fun (p q : Lift hyp) => p.toPreLift ≤ q.toPreLift) a b ∧ ¬(fun (p q : Lift hyp) => p.toPreLift ≤ q.toPreLift) b a)

noncomputable def GaleStewartGame.BorelDet.One.Lift.liftVeryShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : ↥(gameTree hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.liftVeryShort = ⟨↑(Descriptive.Tree.pInv (GaleStewartGame.BorelDet.treeHom hyp) (Descriptive.Tree.take (2 * k) H.x) ⋯) ++ [((↑H.x)[2 * k], H.liftTree)], ⋯⟩

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVeryShort_length {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : (↑H.liftVeryShort).length = 2 * k + 1

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVeryShort_val_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : List.map Prod.fst ↑H.liftVeryShort = List.take (2 * k + 1) ↑H.x

noncomputable def GaleStewartGame.BorelDet.One.Lift.liftShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : ↥(gameTree hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.liftShort = (H.R H.liftVeryShort ⋯ ⋯).valT'

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftShort_length {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : (↑H.liftShort).length = 2 * k + 2

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftShort_val_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : List.take (2 * k + 1) ↑H.liftShort = ↑H.liftVeryShort

noncomputable def GaleStewartGame.BorelDet.One.Lift.liftVal {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : List (upA hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_very_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : (↑H.x).length = 2 * k + 1) : H.liftVal = ↑H.liftVeryShort

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_length {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : H.liftVal.length = (↑H.x).length

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_take_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : List.take (2 * k + 2) H.liftVal = ↑H.liftShort

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_take_veryShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : List.take (2 * k + 1) H.liftVal = ↑H.liftVeryShort

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_take_init {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : n ≤ 2 * k) : List.take n H.liftVal = pInvTreeHomMap hyp (List.take n ↑H.x)

def GaleStewartGame.BorelDet.One.Lift.PreWonPos {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (u : List A) : Prop

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.take n h = { toPreLift := H.take n ⋯, liftTree := H.liftTree, htree := ⋯ }

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.take_liftTree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (n : ℕ) (h : 2 * k + 1 ≤ n) : (H.take n h).liftTree = H.liftTree

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.take_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (n : ℕ) (h : 2 * k + 1 ≤ n) : (H.take n h).toPreLift = H.take n ⋯

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

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.take_rfl {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) : H.take (↑H.x).length ⋯ = H

@[simp]

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

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVeryShort_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : 2 * k + 1 ≤ n) : (H.take n h).liftVeryShort = H.liftVeryShort

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftShort_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : 2 * k + 1 ≤ n) : (H.take n h).liftShort = H.liftShort

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (n : ℕ) (h : 2 * k + 1 ≤ n) : (H.take n h).liftVal = List.take n H.liftVal

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift.preWonPos_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : 2 * k + 1 ≤ n) (u : List A) : (H.take n h).PreWonPos u ↔ H.PreWonPos u

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

theorem GaleStewartGame.BorelDet.One.Lift.take_le_take {A : Type u_1} {G : Game A} {k m n : ℕ} {hyp : Hyp G k} (H : Lift hyp) (hm : 2 * k + 1 ≤ m) (hn : 2 * k + 1 ≤ n) : H.take m hm ≤ H.take n hn ↔ m ≤ n ∨ (↑H.x).length ≤ n

theorem GaleStewartGame.BorelDet.One.Lift.eq_take {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H ≤ H') (ht : H.liftTree = H'.liftTree) : H = H'.take (↑H.x).length ⋯

theorem GaleStewartGame.BorelDet.One.Lift.liftVal_mono {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {H H' : Lift hyp} (h : H ≤ H') (ht : H.liftTree = H'.liftTree) : H.liftVal <+: H'.liftVal

def GaleStewartGame.BorelDet.One.Lift.Con {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.Con = (List.drop (2 * k + 1) ↑H.x ∈ Descriptive.Tree.pullSub (GaleStewartGame.BorelDet.getTree' hyp ↑H.liftShort) [(↑H.liftShort)[2 * k + 1].1])

theorem GaleStewartGame.BorelDet.One.Lift.Con.take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : 2 * k + 1 ≤ n) (h' : H.Con) : (H.take n h).Con

theorem GaleStewartGame.BorelDet.One.Lift.con_of_short {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : (↑H.x).length = 2 * k + 1) : H.Con

theorem GaleStewartGame.BorelDet.One.Lift.con_short_long {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : H.Con ↔ (↑H.liftShort)[2 * k + 1].1 = (↑H.x)[2 * k + 1] ∧ List.drop (2 * k + 2) ↑H.x ∈ getTree' hyp ↑H.liftShort

structure GaleStewartGame.BorelDet.One.Lift' {A : Type u_1} {G : Game A} {k : ℕ} (hyp : Hyp G k) extends GaleStewartGame.BorelDet.One.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.one (2 * k + 1)
• liftTree : ↥(Descriptive.tree A)
• htree : ∃ (S : QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑self.x)) Player.one), self.liftTree = S.fst.subtree
• con : self.Con

theorem GaleStewartGame.BorelDet.One.Lift'.ext_iff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} {x y : Lift' hyp} : x = y ↔ x.toLift = y.toLift

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

@[implicit_reducible]

instance GaleStewartGame.BorelDet.One.instPreorderLift' {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} : Preorder (Lift' hyp)

Equations

• GaleStewartGame.BorelDet.One.instPreorderLift' = { le := fun (p q : GaleStewartGame.BorelDet.One.Lift' hyp) => p.toLift ≤ q.toLift, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem GaleStewartGame.BorelDet.One.Lift'.conShort {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : (↑H.liftShort)[2 * k + 1].1 = (↑H.x)[2 * k + 1]

theorem GaleStewartGame.BorelDet.One.Lift'.conLong {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) : List.drop (2 * k + 2) ↑H.x ∈ getTree' hyp ↑H.liftShort

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.liftShort_val_map {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (h : 2 * k + 2 ≤ (↑H.x).length) : List.map Prod.fst ↑H.liftShort = List.take (2 * k + 2) ↑H.x

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.liftVal_lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) : List.map Prod.fst H.liftVal = ↑H.x

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.liftVal_lift_get {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (h : n < (↑H.x).length) : H.liftVal[n].1 = (↑H.x)[n]

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.take n h = { toLift := H.take n h, con := ⋯ }

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.take_toLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (n : ℕ) (h : 2 * k + 1 ≤ n) : (H.take n h).toLift = H.take n h

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

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.take_rfl {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) : H.take (↑H.x).length ⋯ = H

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.take_trans {A : Type u_1} {G : Game A} {k m n : ℕ} {hyp : Hyp G k} (H : Lift' hyp) (hm : 2 * k + 1 ≤ m) (hn : 2 * k + 1 ≤ n) : (H.take m hm).take n hn = H.take (min m n) ⋯

noncomputable def GaleStewartGame.BorelDet.One.Lift'.lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) : ↥(gameTree hyp)

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.lift = ⟨H.liftVal, ⋯⟩

@[simp]

theorem GaleStewartGame.BorelDet.One.Lift'.lift_coe {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) : ↑H.lift = H.liftVal

theorem GaleStewartGame.BorelDet.One.Lift'.lift_lift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : Lift' hyp) : (CategoryTheory.ConcreteCategory.hom (treeHom hyp)) H.lift = H.x

def GaleStewartGame.BorelDet.One.PreLift.extend {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (S : QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x)) Player.one) : Lift hyp

Auxiliary declaration for the Borel determinacy formalization.

Equations

• H.extend S = { toPreLift := H, liftTree := S.fst.subtree, htree := ⋯ }

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.extend_liftTree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (S : QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x)) Player.one) : (H.extend S).liftTree = S.fst.subtree

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.extend_toPreLift {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (S : QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x)) Player.one) : (H.extend S).toPreLift = H

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

def GaleStewartGame.BorelDet.One.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 := Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x), payoff := Subtype.val ⁻¹' ⋃ u ∈ H.WonPos, Stream'.Discrete.principalOpen u }

theorem GaleStewartGame.BorelDet.One.PreLift.game_tree {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : H.game.tree = Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑H.x)

theorem GaleStewartGame.BorelDet.One.PreLift.game_payoff {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : H.game.payoff = Subtype.val ⁻¹' ⋃ u ∈ H.WonPos, Stream'.Discrete.principalOpen u

theorem GaleStewartGame.BorelDet.One.PreLift.game_open {A : Type u_1} {G : Game A} {k : ℕ} {hyp : Hyp G k} (H : PreLift hyp) : IsOpen H.game.payoff

theorem GaleStewartGame.BorelDet.One.PreLift.extend_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (h : 2 * k < n) (S : QuasiStrategy (Descriptive.Tree.subAt G.tree (List.take (2 * k + 1) ↑(H.take n h).x)) Player.one) : (H.take n h).extend S = (H.extend (cast ⋯ S)).take n h

@[simp]

theorem GaleStewartGame.BorelDet.One.PreLift.wonPos_take {A : Type u_1} {G : Game A} {k n : ℕ} {hyp : Hyp G k} (H : PreLift hyp) (h : 2 * k < n) : (H.take n h).WonPos = H.WonPos

@[simp]

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

def GaleStewartGame.BorelDet.One.PreLift.Won {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.Won = ∃ u ∈ H.WonPos, u <+: List.drop (2 * k + 1) ↑H.x

def GaleStewartGame.BorelDet.One.PreLift.Winnable {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.Winnable = GaleStewartGame.PreStrategy.WinningPrefix H.game GaleStewartGame.Player.zero (List.drop (2 * k + 1) ↑H.x)

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' = ¬GaleStewartGame.PreStrategy.WinningPrefix H.game GaleStewartGame.Player.zero (List.drop (2 * k + 1) ↑H.x)