Root aliases for dotted declarations

These aliases preserve names that Lean Pool's deterministic quality audit derives from dotted declarations inside namespaces.

theorem AllWinning.residual {A : Type u_1} {p : GaleStewartGame.Player} {G : GaleStewartGame.Game A} (hW : G.AllWinning p) (x : List A) : (G.residual x).AllWinning (GaleStewartGame.Player.residual x p)

Alias of GaleStewartGame.Game.AllWinning.residual.

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

Alias of GaleStewartGame.BorelDet.One.Lift.Con.take.

theorem ExtensionsAt.cast_valT' {A : Type u_1} {T : ↥(Descriptive.tree A)} {x y : ↥T} (h : x = y) (a : Descriptive.Tree.ExtensionsAt x) : (cast ⋯ a).valT' = a.valT'

Alias of Descriptive.Tree.ExtensionsAt.cast_valT'.

theorem Fixing.bijective {S T : Descriptive.Tree.Trees} {k : ℕ} {f : S ⟶ T} (h : Descriptive.Tree.Fixing k f) : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom ((Descriptive.Tree.res k).map f))

Alias of Descriptive.Tree.Fixing.bijective.

theorem Fixing.inj {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (x y : ↑↑S.snd) (ht : Descriptive.Tree.Fixing (↑x).length f := by as_aux_lemma => synthFixing) (he : (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) y) : x = y

Alias of Descriptive.Tree.Fixing.inj.

theorem Fixing.mon {S T : Descriptive.Tree.Trees} {k n : ℕ} {f : S ⟶ T} (h : Descriptive.Tree.Fixing k f) (hn : n ≤ k) : Descriptive.Tree.Fixing n f

Alias of Descriptive.Tree.Fixing.mon.

theorem Game.exists_undetermined : ∃ (G : GaleStewartGame.Game (Fin 2)), Descriptive.Tree.IsPruned G.tree ∧ [] ∈ G.tree ∧ ¬G.IsDetermined

Alias of GaleStewartGame.Game.exists_undetermined.

def Games.Covering (G' G : GaleStewartGame.Covering.Games) : Type

Alias of GaleStewartGame.Covering.Games.Covering.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Games.Covering = GaleStewartGame.Covering.Games.Covering

def Games.IsUnravelable (G : GaleStewartGame.Covering.Games) : Prop

Alias of GaleStewartGame.Covering.Games.IsUnravelable.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Games.IsUnravelable = GaleStewartGame.Covering.Games.IsUnravelable

theorem Games.borel_determinacy (G : GaleStewartGame.Covering.Games) (h : MeasurableSet G.snd.fst.payoff) : G.snd.fst.IsDetermined

Alias of GaleStewartGame.Games.borel_determinacy.

---

Borel games are determined

def Games.tree (G : GaleStewartGame.Covering.Games) : GaleStewartGame.Covering.PTrees

Alias of GaleStewartGame.Covering.Games.tree.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Games.tree = GaleStewartGame.Covering.Games.tree

theorem Games.IsUnravelable.isDetermined {G : GaleStewartGame.Covering.Games} (h : G.IsUnravelable) : G.snd.fst.IsDetermined

Alias of GaleStewartGame.Covering.Games.IsUnravelable.isDetermined.

theorem IsPosition.iff_lenHom (p : GaleStewartGame.Player) {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (x : (fun (S : Descriptive.Tree.Trees) => ↑↑S.snd) S) : GaleStewartGame.IsPosition (↑((CategoryTheory.ConcreteCategory.hom f) x)) p ↔ GaleStewartGame.IsPosition (↑x) p

Alias of GaleStewartGame.IsPosition.iff_lenHom.

theorem IsPrefix.zipInitsMap {α : Type u_1} {β : Type u_2} (x y : List α) (f : α → List α → β) (h : x <+: y) : x.zipInitsMap f <+: y.zipInitsMap f

Alias of List.IsPrefix.zipInitsMap.

theorem IsPruned.body_ne_iff_ne {A : Type u_1} {T : ↥(Descriptive.tree A)} (h : Descriptive.Tree.IsPruned T) : (Descriptive.Tree.body T).Nonempty ↔ [] ∈ T

Alias of Descriptive.Tree.IsPruned.body_ne_iff_ne.

theorem IsPruned.pullSub {A : Type u_1} {T : ↥(Descriptive.tree A)} (hP : Descriptive.Tree.IsPruned T) (x : List A) : Descriptive.Tree.IsPruned (Descriptive.Tree.pullSub T x)

Alias of Descriptive.Tree.IsPruned.pullSub.

theorem IsPruned.sub {A : Type u_1} {T : ↥(Descriptive.tree A)} (h : Descriptive.Tree.IsPruned T) (x : List A) : Descriptive.Tree.IsPruned (Descriptive.Tree.subAt T x)

Alias of Descriptive.Tree.IsPruned.sub.

theorem LenHom.bodyMap_continuous {S T : Descriptive.Tree.Trees} (f : S ⟶ T) : Continuous ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map f))

Alias of Descriptive.Tree.LenHom.bodyMap_continuous.

theorem LenHom.bodyMap_spec {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (a : ↑(Descriptive.Tree.body S.snd)) (x : List S.fst) (hx : ↑a ∈ Stream'.Discrete.principalOpen x) (n : ℕ) (hlx : n < x.length) : (↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyPre.map f)) a)).get n = (↑((CategoryTheory.ConcreteCategory.hom f) ⟨x, ⋯⟩))[n]

Alias of Descriptive.Tree.LenHom.bodyMap_spec.

theorem LenHom.bodyMap_spec_res {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (a : ↑(Descriptive.Tree.body S.snd)) (n : ℕ) : (↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyPre.map f)) a)).get n = (↑((CategoryTheory.ConcreteCategory.hom f) (Descriptive.Tree.body.take (n + 1) a)))[n]

Alias of Descriptive.Tree.LenHom.bodyMap_spec_res.

theorem LenHom.bodyMap_spec_res_lt {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (a : ↑(Descriptive.Tree.body S.snd)) {m n : ℕ} (h : m < n) : (↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyPre.map f)) a)).get m = (↑((CategoryTheory.ConcreteCategory.hom f) (Descriptive.Tree.body.take n a)))[m]

Alias of Descriptive.Tree.LenHom.bodyMap_spec_res_lt.

theorem LenHom.bodyPre_map_restrict {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (a : ↑(Descriptive.Tree.body S.snd)) (n : ℕ) : Stream'.take n ↑((CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyPre.map f)) a) = ↑((CategoryTheory.ConcreteCategory.hom f) (Descriptive.Tree.body.take n a))

Alias of Descriptive.Tree.LenHom.bodyPre_map_restrict.

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

Alias of GaleStewartGame.BorelDet.One.PreLift.Losable.lift'.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @Losable.lift' = @GaleStewartGame.BorelDet.One.PreLift.Losable.lift'

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

Alias of GaleStewartGame.BorelDet.One.PreLift.Losable.losable_of_le.

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

Alias of GaleStewartGame.BorelDet.One.PreLift.Losable'.losable'_of_le.

theorem LosingCondition.concat {A : Type u_1} {G : GaleStewartGame.Game A} {k : ℕ} {hyp : GaleStewartGame.BorelDet.Hyp G k} {x : List (GaleStewartGame.BorelDet.upA hyp)} {a : GaleStewartGame.BorelDet.upA hyp} {h : (x ++ [a]).length = 2 * k + 2} : GaleStewartGame.BorelDet.LosingCondition (x ++ [a]) h ↔ Descriptive.Tree.body (Descriptive.Tree.pullSub a.2 (List.map Prod.fst x ++ [a.1])) ∩ Subtype.val '' G.payoff = ∅ ∧ ∃ (y : ↥(Descriptive.Tree.subAt (GaleStewartGame.BorelDet.getTree' hyp x) [a.1])), a.2 = Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree (List.map Prod.fst x ++ a.1 :: ↑y)) ↑y

Alias of GaleStewartGame.BorelDet.LosingCondition.concat.

theorem LosingCondition.not_lost_short {A : Type u_1} {G : GaleStewartGame.Game A} {k : ℕ} {hyp : GaleStewartGame.BorelDet.Hyp G k} {x : ↥(GaleStewartGame.BorelDet.game hyp).tree} (hxl : 2 * k + 2 ≤ (↑x).length) (H : GaleStewartGame.BorelDet.LosingCondition ↑(Descriptive.Tree.take (2 * k + 2) x) ⋯) (hnL : ¬G.WonPosition (List.map Prod.fst ↑x) (GaleStewartGame.Player.residual (↑x) GaleStewartGame.Player.one)) : (↑x).length + 1 ≤ 2 * k + 2 + (↑H.y).length

Alias of GaleStewartGame.BorelDet.LosingCondition.not_lost_short.

theorem LosingCondition.of_concat {A : Type u_1} {G : GaleStewartGame.Game A} {k : ℕ} {hyp : GaleStewartGame.BorelDet.Hyp G k} {x : List (GaleStewartGame.BorelDet.upA hyp)} {a : GaleStewartGame.BorelDet.upA hyp} {h : (x ++ [a]).length = 2 * k + 2} (H : GaleStewartGame.BorelDet.LosingCondition (x ++ [a]) h) : ∃ (y : ↥(Descriptive.Tree.subAt (GaleStewartGame.BorelDet.getTree' hyp x) [a.1])), a.2 = Descriptive.Tree.pullSub (Descriptive.Tree.subAt G.tree (List.map Prod.fst x ++ a.1 :: ↑y)) ↑y

Alias of GaleStewartGame.BorelDet.LosingCondition.of_concat.

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

Alias of GaleStewartGame.BorelDet.Zero.Lift.Lost'.mk.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @Lost'.mk = @GaleStewartGame.BorelDet.Zero.Lift.Lost'.mk

def LvlStratHom.comp {T U V : GaleStewartGame.Covering.PTreesS} (g : GaleStewartGame.Covering.LvlStratHom U V) (f : GaleStewartGame.Covering.LvlStratHom T U) : GaleStewartGame.Covering.LvlStratHom T V

Alias of GaleStewartGame.Covering.LvlStratHom.comp.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @LvlStratHom.comp = @GaleStewartGame.Covering.LvlStratHom.comp

theorem LvlStratHom.comp_toFun {k : ℕ} {p : GaleStewartGame.Player} {T U V : GaleStewartGame.Covering.PTreesS} (f : T ⟶ U) (g : U ⟶ V) : (CategoryTheory.CategoryStruct.comp f g).toFun p k = g.toFun p k ∘ f.toFun p k

Alias of GaleStewartGame.Covering.LvlStratHom.comp_toFun.

theorem LvlStratHom.ext' {T U : GaleStewartGame.Covering.PTreesS} {f g : T ⟶ U} (h : f.toFun = g.toFun) : f = g

Alias of GaleStewartGame.Covering.LvlStratHom.ext'.

def LvlStratHom.global (p : GaleStewartGame.Player) : CategoryTheory.Functor GaleStewartGame.Covering.PTreesS Type

Alias of GaleStewartGame.Covering.LvlStratHom.global.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• LvlStratHom.global = GaleStewartGame.Covering.LvlStratHom.global

def LvlStratHom.globalOfObj {p : GaleStewartGame.Player} {T : GaleStewartGame.Covering.PTreesS} (S : (GaleStewartGame.Covering.LvlStratHom.global p).obj T) : GaleStewartGame.Strategy T.tree.fst.snd p

Alias of GaleStewartGame.Covering.LvlStratHom.globalOfObj.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @LvlStratHom.globalOfObj = @GaleStewartGame.Covering.LvlStratHom.globalOfObj

def LvlStratHom.globalToObj {p : GaleStewartGame.Player} {T : GaleStewartGame.Covering.PTreesS} (S : GaleStewartGame.Strategy T.tree.fst.snd p) : (GaleStewartGame.Covering.LvlStratHom.global p).obj T

Alias of GaleStewartGame.Covering.LvlStratHom.globalToObj.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @LvlStratHom.globalToObj = @GaleStewartGame.Covering.LvlStratHom.globalToObj

def LvlStratHom.id (T : GaleStewartGame.Covering.PTreesS) : GaleStewartGame.Covering.LvlStratHom T T

Alias of GaleStewartGame.Covering.LvlStratHom.id.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• LvlStratHom.id = GaleStewartGame.Covering.LvlStratHom.id

theorem LvlStratHom.id_toFun {k : ℕ} {p : GaleStewartGame.Player} (T : GaleStewartGame.Covering.PTreesS) : (CategoryTheory.CategoryStruct.id T).toFun p k = _root_.id

Alias of GaleStewartGame.Covering.LvlStratHom.id_toFun.

def LvlStratHom.system (p : GaleStewartGame.Player) : CategoryTheory.Functor GaleStewartGame.Covering.PTreesS Type

Alias of GaleStewartGame.Covering.LvlStratHom.system.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• LvlStratHom.system = GaleStewartGame.Covering.LvlStratHom.system

def LvlStratHom.systemOfObj {p : GaleStewartGame.Player} {T : GaleStewartGame.Covering.PTreesS} (S : (GaleStewartGame.Covering.LvlStratHom.system p).obj T) : GaleStewartGame.StrategySystem T.tree.fst p

Alias of GaleStewartGame.Covering.LvlStratHom.systemOfObj.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @LvlStratHom.systemOfObj = @GaleStewartGame.Covering.LvlStratHom.systemOfObj

def LvlStratHom.systemToObj {p : GaleStewartGame.Player} {T : GaleStewartGame.Covering.PTreesS} (S : GaleStewartGame.StrategySystem T.tree.fst p) : (GaleStewartGame.Covering.LvlStratHom.system p).obj T

Alias of GaleStewartGame.Covering.LvlStratHom.systemToObj.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @LvlStratHom.systemToObj = @GaleStewartGame.Covering.LvlStratHom.systemToObj

def PartiallyUnravelled.continue {n : ℕ} (G : GaleStewartGame.BorelDet'.PartiallyUnravelled n) (k : ℕ) : (G' : GaleStewartGame.BorelDet'.PartiallyUnravelled (n + 1)) ×' (f : G'.carrier ⟶ G.carrier) ×' GaleStewartGame.Covering.Fixing (k + n) f ∧ ∀ (n_1 : ℕ), (G'.sets n_1).fst = ⇑(CategoryTheory.ConcreteCategory.hom (Descriptive.Tree.bodyFunctor.map f.toHom)) ⁻¹' (G.sets n_1).fst

Alias of GaleStewartGame.BorelDet'.PartiallyUnravelled.continue.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @PartiallyUnravelled.continue = @GaleStewartGame.BorelDet'.PartiallyUnravelled.continue

def Player.ownTree {A : Type u_1} (p : GaleStewartGame.Player) (a : Stream' A) : GaleStewartGame.Strategy ⊤ p

Alias of GaleStewartGame.Player.ownTree.

---

the strategy which plays the infinite sequence a independent of the opponents' moves

Equations

• @Player.ownTree = @GaleStewartGame.Player.ownTree

theorem Player.ownTree.disjoint {A : Type u_1} {p : GaleStewartGame.Player} {a b : Stream' A} (h : a ≠ b) : Descriptive.Tree.body (p.ownTree a).pre.subtree ∩ Descriptive.Tree.body (p.ownTree b).pre.subtree = ∅

Alias of GaleStewartGame.Player.ownTree.disjoint.

theorem Player.ownTree.mem_body {A : Type u_1} {p : GaleStewartGame.Player} {a x : Stream' A} : x ∈ Descriptive.Tree.body (p.ownTree a).pre.subtree ↔ ∀ (n : ℕ), x.get (2 * n + p.toNat) = a.get n

Alias of GaleStewartGame.Player.ownTree.mem_body.

def PreStrategy.IsWinning {A : Type u_1} {p : GaleStewartGame.Player} {G : GaleStewartGame.Game A} (s : GaleStewartGame.PreStrategy G.tree p) : Prop

Alias of GaleStewartGame.PreStrategy.IsWinning.

---

a PreStrategy is winning if all compatible plays are won

Equations

• @PreStrategy.IsWinning = @GaleStewartGame.PreStrategy.IsWinning

theorem PreStrategy.cast_quasi {A : Type u_1} {T T' : ↥(Descriptive.tree A)} {p p' : GaleStewartGame.Player} (hT : T = T') (hP : p = p') (S : GaleStewartGame.PreStrategy T p) : (cast ⋯ S).IsQuasi ↔ S.IsQuasi

Alias of GaleStewartGame.PreStrategy.cast_quasi.

theorem PreStrategy.cast_winning {A : Type u_1} {p : GaleStewartGame.Player} {G G' : GaleStewartGame.Game A} (h : G = G') (S : GaleStewartGame.PreStrategy G.tree p) : (cast ⋯ S).IsWinning ↔ S.IsWinning

Alias of GaleStewartGame.PreStrategy.cast_winning.

theorem PreStrategy.choose_sub {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} {S : GaleStewartGame.PreStrategy T p} (h : S.IsQuasi) : h.choose.pre ≤ S

Alias of GaleStewartGame.PreStrategy.choose_sub.

theorem PreStrategy.eval_mem_congr {A : Type u_1} {p : GaleStewartGame.Player} {U : ↥(Descriptive.tree A)} (S : GaleStewartGame.PreStrategy U p) {x x' : ↥U} (hx : x = x') (hp : GaleStewartGame.IsPosition (↑x) p) (hp' : GaleStewartGame.IsPosition (↑x') p) {a : Descriptive.Tree.ExtensionsAt x} {a' : Descriptive.Tree.ExtensionsAt x'} (ha : ↑a = ↑a') : a ∈ S x hp ↔ a' ∈ S x' hp'

Alias of GaleStewartGame.PreStrategy.eval_mem_congr.

theorem PreStrategy.eval_val_congr {A : Type u_1} {p : GaleStewartGame.Player} {U : ↥(Descriptive.tree A)} (S S' : GaleStewartGame.PreStrategy U p) (h : S = S') (x x' : ↥U) (h' : x = x') (hp : GaleStewartGame.IsPosition (↑x) p) : Subtype.val '' S x hp = Subtype.val '' S' x' ⋯

Alias of GaleStewartGame.PreStrategy.eval_val_congr.

theorem PreStrategy.sub_winning {A : Type u_1} {p : GaleStewartGame.Player} {G : GaleStewartGame.Game A} {s t : GaleStewartGame.PreStrategy G.tree p} (h : s ≤ t) (h' : t.IsWinning) : s.IsWinning

Alias of GaleStewartGame.PreStrategy.sub_winning.

def PreStrategy.subgame {A : Type u_1} {p : GaleStewartGame.Player} {G : GaleStewartGame.Game A} (S : GaleStewartGame.PreStrategy G.tree p) : GaleStewartGame.Game A

Alias of GaleStewartGame.PreStrategy.subgame.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @PreStrategy.subgame = @GaleStewartGame.PreStrategy.subgame

def PreStrategy.IsQuasi.choose {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} {S : GaleStewartGame.PreStrategy T p} (h : S.IsQuasi) : GaleStewartGame.Strategy T p

Alias of GaleStewartGame.PreStrategy.IsQuasi.choose.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @PreStrategy.IsQuasi.choose = @GaleStewartGame.PreStrategy.IsQuasi.choose

theorem PreStrategy.IsQuasi.restrictTree_isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} {S : GaleStewartGame.PreStrategy T p} (rto : ↥(Descriptive.tree A)) (h : S.IsQuasi) (hfair : ∀ (x : ↥rto) (a : A), GaleStewartGame.IsPosition (↑x) p → ↑x ++ [a] ∈ T → ↑x ++ [a] ∈ rto) (hr : rto ≤ T) : (S.restrictTree rto hr).IsQuasi

Alias of GaleStewartGame.PreStrategy.IsQuasi.restrictTree_isQuasi.

theorem PreStrategy.IsQuasi.restrict_isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} {S : GaleStewartGame.PreStrategy T p} (rto : GaleStewartGame.PreStrategy T p.swap) (h : S.IsQuasi) : (S.restrict rto).IsQuasi

Alias of GaleStewartGame.PreStrategy.IsQuasi.restrict_isQuasi.

theorem PreStrategy.IsWinning.choose {A : Type u_1} {p : GaleStewartGame.Player} {G : GaleStewartGame.Game A} (s : GaleStewartGame.QuasiStrategy G.tree p) (h : s.fst.IsWinning) : ⋯.choose.pre.IsWinning

Alias of GaleStewartGame.PreStrategy.IsWinning.choose.

theorem PreStrategy.IsWinning.residual {A : Type u_1} {p : GaleStewartGame.Player} {G : GaleStewartGame.Game A} {s : GaleStewartGame.PreStrategy G.tree p} (h : s.IsWinning) (x : ↥s.subtree) : (s.residual ↑x).IsWinning

Alias of GaleStewartGame.PreStrategy.IsWinning.residual.

theorem QuasiStrategy.ext {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} {f g : GaleStewartGame.QuasiStrategy T p} (h : f.fst = g.fst) : f = g

Alias of GaleStewartGame.QuasiStrategy.ext.

def QuasiStrategy.residual {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} (S : GaleStewartGame.QuasiStrategy T p) (x : List A) : GaleStewartGame.QuasiStrategy (Descriptive.Tree.subAt T x) (GaleStewartGame.Player.residual x p)

Alias of GaleStewartGame.QuasiStrategy.residual.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @QuasiStrategy.residual = @GaleStewartGame.QuasiStrategy.residual

def QuasiStrategy.restrict {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} (S : GaleStewartGame.QuasiStrategy T p) (rto : GaleStewartGame.PreStrategy T p.swap) : GaleStewartGame.QuasiStrategy rto.subtree p

Alias of GaleStewartGame.QuasiStrategy.restrict.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @QuasiStrategy.restrict = @GaleStewartGame.QuasiStrategy.restrict

theorem QuasiStrategy.subtree_isPruned {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} (S : GaleStewartGame.QuasiStrategy T p) (hT : Descriptive.Tree.IsPruned T) : Descriptive.Tree.IsPruned S.fst.subtree

Alias of GaleStewartGame.QuasiStrategy.subtree_isPruned.

theorem QuasiStrategy.subtree_top_large {A : Type u_1} {p : GaleStewartGame.Player} (h : 2 ≤ Cardinal.mk A) (S : GaleStewartGame.QuasiStrategy ⊤ p) : Cardinal.continuum ≤ Cardinal.mk ↑(Descriptive.Tree.body S.fst.subtree)

Alias of GaleStewartGame.QuasiStrategy.subtree_top_large.

theorem Strategy.eval_val_congr {A : Type u_1} {p : GaleStewartGame.Player} {U : ↥(Descriptive.tree A)} (S S' : GaleStewartGame.Strategy U p) (h : S = S') (x x' : ↥U) (h' : x = x') (hp : GaleStewartGame.IsPosition (↑x) p) : ↑(S x hp) = ↑(S' x' ⋯)

Alias of GaleStewartGame.Strategy.eval_val_congr.

theorem Strategy.ext {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} {f g : GaleStewartGame.Strategy T p} (h : ∀ (x : ↥T) (hp : GaleStewartGame.IsPosition (↑x) p), f x hp = g x hp) : f = g

Alias of GaleStewartGame.Strategy.ext.

theorem Strategy.isQuasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} (S : GaleStewartGame.Strategy T p) : S.pre.IsQuasi

Alias of GaleStewartGame.Strategy.isQuasi.

def Strategy.pre {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} (S : GaleStewartGame.Strategy T p) : GaleStewartGame.PreStrategy T p

Alias of GaleStewartGame.Strategy.pre.

---

regard a Strategy as PreStrategy

Equations

• @Strategy.pre = @GaleStewartGame.Strategy.pre

def Strategy.quasi {A : Type u_1} {T : ↥(Descriptive.tree A)} {p : GaleStewartGame.Player} (S : GaleStewartGame.Strategy T p) : GaleStewartGame.QuasiStrategy T p

Alias of GaleStewartGame.Strategy.quasi.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @Strategy.quasi = @GaleStewartGame.Strategy.quasi

theorem StrategySystem.con' {k m : ℕ} {T : Descriptive.Tree.Trees} {p : GaleStewartGame.Player} (S : GaleStewartGame.StrategySystem T p) (h : k ≤ m) : GaleStewartGame.ResStrategy.res h (S.str m) = S.str k

Alias of GaleStewartGame.StrategySystem.con'.

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

Alias of GaleStewartGame.BorelDet.Zero.Lift.Winnable.conLong.

theorem WinningCondition.concat {A : Type u_1} {G : GaleStewartGame.Game A} {k : ℕ} {hyp : GaleStewartGame.BorelDet.Hyp G k} {x : List (GaleStewartGame.BorelDet.upA hyp)} {a : GaleStewartGame.BorelDet.upA hyp} {h : (x ++ [a]).length = 2 * k + 2} : GaleStewartGame.BorelDet.WinningCondition (x ++ [a]) h ↔ Descriptive.Tree.body (Descriptive.Tree.pullSub a.2 (List.map Prod.fst x ++ [a.1])) ⊆ Subtype.val '' G.payoff ∧ ∃ (S' : GaleStewartGame.QuasiStrategy (Descriptive.Tree.subAt (GaleStewartGame.BorelDet.getTree' hyp x) [a.1]) GaleStewartGame.Player.one), a.2 = S'.fst.subtree

Alias of GaleStewartGame.BorelDet.WinningCondition.concat.

theorem WinningCondition.of_concat {A : Type u_1} {G : GaleStewartGame.Game A} {k : ℕ} {hyp : GaleStewartGame.BorelDet.Hyp G k} {x : List (GaleStewartGame.BorelDet.upA hyp)} {a : GaleStewartGame.BorelDet.upA hyp} {h : (x ++ [a]).length = 2 * k + 2} (H : GaleStewartGame.BorelDet.WinningCondition (x ++ [a]) h) : ∃ (S' : GaleStewartGame.QuasiStrategy (Descriptive.Tree.subAt (GaleStewartGame.BorelDet.getTree' hyp x) [a.1]) GaleStewartGame.Player.one), a.2 = S'.fst.subtree

Alias of GaleStewartGame.BorelDet.WinningCondition.of_concat.

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

Alias of GaleStewartGame.BorelDet.One.PreLift.Won.lift'.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @Won.lift' = @GaleStewartGame.BorelDet.One.PreLift.Won.lift'

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

Alias of GaleStewartGame.BorelDet.One.PreLift.Won.won_of_le.

theorem WonPosition.extend {A : Type u_1} {G : GaleStewartGame.Game A} {p : GaleStewartGame.Player} {x : List A} (y : List A) (hW : G.WonPosition x p) : G.WonPosition (x ++ y) (GaleStewartGame.Player.residual y p)

Alias of GaleStewartGame.Game.WonPosition.extend.

def body.append {A : Type u_1} {T : ↥(Descriptive.tree A)} (x : List A) (y : ↑(Descriptive.Tree.body (Descriptive.Tree.subAt T x))) : ↑(Descriptive.Tree.body T)

Alias of Descriptive.Tree.body.append.

---

Appending lists to the front of a branch lifts as an operation on bodies

Equations

• @body.append = @Descriptive.Tree.body.append

theorem body.append_con {A : Type u_1} {T : ↥(Descriptive.tree A)} (x : List A) : Continuous (Descriptive.Tree.body.append x)

Alias of Descriptive.Tree.body.append_con.

def body.drop {A : Type u_1} {T : ↥(Descriptive.tree A)} (n : ℕ) (x : ↑(Descriptive.Tree.body T)) : ↑(Descriptive.Tree.body (Descriptive.Tree.subAt T (Stream'.take n ↑x)))

Alias of Descriptive.Tree.body.drop.

---

Dropping the first elements of a branch lifts as an operation on bodies

Equations

• @body.drop = @Descriptive.Tree.body.drop

def body.take {A : Type u_1} {T : ↥(Descriptive.tree A)} (n : ℕ) (x : ↑(Descriptive.Tree.body T)) : ↥T

Alias of Descriptive.Tree.body.take.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @body.take = @Descriptive.Tree.body.take

def chainTree.concat {X : Type u_1} (V : Set (Set X)) (x : ↥(Choquet.chainTree V)) (A : ↑V) (h : ∀ (hx : ↑x ≠ []), A ≤ (↑x).getLast hx) : ↥(Choquet.chainTree V)

Alias of Choquet.chainTree.concat.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @chainTree.concat = @Choquet.chainTree.concat

theorem containsTree.map {S T : Descriptive.Tree.Trees} {x : GaleStewartGame.BodySystemObj S} {y : ↑↑S.snd} (h : x.containsTree y) (f : S ⟶ T) : (GaleStewartGame.BodySystemObj.ofObj ((CategoryTheory.ConcreteCategory.hom (GaleStewartGame.bodySystem.map f)) x.toObj)).containsTree ((CategoryTheory.ConcreteCategory.hom f) y)

Alias of GaleStewartGame.BodySystemObj.containsTree.map.

def extensions.val' {T : Descriptive.Tree.PointedTrees} (a : Descriptive.Tree.extensions.obj T) : List T.fst.fst

Alias of Descriptive.Tree.extensions.val'.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @extensions.val' = @Descriptive.Tree.extensions.val'

def extensions.valT' {T : Descriptive.Tree.PointedTrees} (a : Descriptive.Tree.extensions.obj T) : ↑↑T.fst.snd

Alias of Descriptive.Tree.extensions.valT'.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @extensions.valT' = @Descriptive.Tree.extensions.valT'

theorem res.ext_val' {S : Descriptive.Tree.Trees} {k : ℕ} {x y : ↑↑((Descriptive.Tree.res k).obj S).snd} (h : Descriptive.Tree.res.val' x = Descriptive.Tree.res.val' y) : x = y

Alias of Descriptive.Tree.res.ext_val'.

def res.val' {S : Descriptive.Tree.Trees} {k : ℕ} (x : ↑↑((Descriptive.Tree.res k).obj S).snd) : ↑↑S.snd

Alias of Descriptive.Tree.res.val'.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @res.val' = @Descriptive.Tree.res.val'

theorem resEq.ext_val' {S : Descriptive.Tree.Trees} {k : ℕ} {x y : (Descriptive.Tree.resEq k).obj S} (h : Descriptive.Tree.resEq.val' x = Descriptive.Tree.resEq.val' y) : x = y

Alias of Descriptive.Tree.resEq.ext_val'.

def resEq.val' {S : Descriptive.Tree.Trees} {k : ℕ} (x : (Descriptive.Tree.resEq k).obj S) : ↑↑S.snd

Alias of Descriptive.Tree.resEq.val'.

---

Auxiliary declaration for the Borel determinacy formalization.

Equations

• @resEq.val' = @Descriptive.Tree.resEq.val'