LeanPool.AFormalizationOfBorelDeterminacyInLean.Proof.CoveringLim #

Auxiliary declarations for the Borel determinacy formalization.

theorem GaleStewartGame.Covering.transition_fixing_full {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {m n : ℕ} (h : m ≤ n) :

Fixing (K + m) (F.map (CategoryTheory.homOfLE h).op)

source

theorem GaleStewartGame.Covering.transition_fixing {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {m n : ℕ} (h : m ≤ n) :

Fixing m (F.map (CategoryTheory.homOfLE h).op)

source

@[reducible, inline]

abbrev GaleStewartGame.Covering.limConePt {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) :

PTrees

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.Covering.limConePt hF = ⟨(Descriptive.Tree.limCone (F.comp GaleStewartGame.Covering.PTreeForget)).pt, ⋯⟩

Instances For

source

@[reducible, inline]

abbrev GaleStewartGame.Covering.limConeπMap {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (n : ℕ) :

(limConePt hF).fst ⟶ (F.obj (Opposite.op n)).fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.Covering.limConeπMap hF n = (Descriptive.Tree.limCone (F.comp GaleStewartGame.Covering.PTreeForget)).π.app (Opposite.op n)

Instances For

source

theorem GaleStewartGame.Covering.limConeπMap_nat {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {n m : ℕ} (h : n ≤ m) :

CategoryTheory.CategoryStruct.comp (limConeπMap hF m) (F.map (CategoryTheory.homOfLE h).op).toHom = limConeπMap hF n

source

instance GaleStewartGame.Covering.limConeπ_fixing_full {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (k : ℕ) :

Descriptive.Tree.Fixing (K + k) (limConeπMap hF k)

source

theorem GaleStewartGame.Covering.fromMap_comp' {p : Player} (k : ℕ) {S T U : Descriptive.Tree.Trees} (f : S ⟶ T) (g : T ⟶ U) (hf : Descriptive.Tree.Fixing k f) (hg : Descriptive.Tree.Fixing k g) (S' : ResStrategy S p k) :

ResStrategy.fromMap (CategoryTheory.CategoryStruct.comp f g) ⋯ S' = ResStrategy.fromMap g hg (ResStrategy.fromMap f hf S')

source

noncomputable def GaleStewartGame.Covering.limConeStr {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (n : ℕ) :

{ tree := limConePt hF } ⟶ { tree := F.obj (Opposite.op n) }

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

theorem GaleStewartGame.Covering.limConeStr_nat {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {n m : ℕ} (h : n ≤ m) :

CategoryTheory.CategoryStruct.comp (limConeStr hF m) (F.map (CategoryTheory.homOfLE h).op).str = limConeStr hF n

source

theorem GaleStewartGame.Covering.cast_limConeStr {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K k : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {m m' : ℕ} (h : m' = m) (hi : Descriptive.Tree.Fixing k (limConeπMap hF m) := by as_aux_lemma => synthFixing) {S : ResStrategy (limConePt hF).fst p k} :

(F.map (CategoryTheory.homOfLE ⋯).op).str.toFun p k (ResStrategy.fromMap (limConeπMap hF m) ⋯ S) = ResStrategy.fromMap (limConeπMap hF m') ⋯ S

source

theorem GaleStewartGame.Covering.limConeStr_large {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K k : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : ResStrategy { tree := limConePt hF }.tree.fst p k) (n : ℕ) (x : (fun (S : Descriptive.Tree.Trees) => ↑↑S.snd) (limConePt hF).fst) (hx : IsPosition (↑x) p) (hl : (↑x).length ≤ k) (h : k ≤ n) :

((limConeStr hF n).toFun p k S ((CategoryTheory.ConcreteCategory.hom (limConeπMap hF n)) x) ⋯ ⋯).valT' = (CategoryTheory.ConcreteCategory.hom (limConeπMap hF n)) (S x hx hl).valT'

source

noncomputable def GaleStewartGame.Covering.coveringLiftBodySystem {p : Player} {T U : PTrees} (f : T ⟶ U) (y : bodySystem.obj U.fst) (S : StrategySystem T.fst p) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map f.str)) S)) :

bodySystem.obj T.fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.Covering.coveringLiftBodySystem f y S yc = ⋯.choose

Instances For

source

theorem GaleStewartGame.Covering.coveringLiftBodySystem_spec1 {p : Player} {T U : PTrees} (f : T ⟶ U) (y : bodySystem.obj U.fst) (S : StrategySystem T.fst p) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map f.str)) S)) :

consistent (coveringLiftBodySystem f y S yc) S

source

theorem GaleStewartGame.Covering.coveringLiftBodySystem_spec2 {p : Player} {T U : PTrees} (f : T ⟶ U) (y : bodySystem.obj U.fst) (S : StrategySystem T.fst p) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map f.str)) S)) :

(CategoryTheory.ConcreteCategory.hom (bodySystem.map f.toHom)) (coveringLiftBodySystem f y S yc) = y

source

theorem GaleStewartGame.Covering.ineq_rec (n k : ℕ) :

max n k ≤ max n (k + 1)

source

def GaleStewartGame.Covering.mapIneqRec {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} (n k : ℕ) :

F.obj (Opposite.op (max n (k + 1))) ⟶ F.obj (Opposite.op (max n k))

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.Covering.mapIneqRec n k = F.map (CategoryTheory.homOfLE ⋯).op

Instances For

source

def GaleStewartGame.Covering.limConeBodyLifts {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) (k : ℕ) :

(y : bodySystem.obj (F.obj (Opposite.op (max n k))).fst) ×' consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n k)))) S)

Auxiliary declaration for the Borel determinacy formalization.

Equations

One or more equations did not get rendered due to their size.
GaleStewartGame.Covering.limConeBodyLifts hF S y yc 0 = ⟨y, yc⟩

Instances For

source

theorem GaleStewartGame.Covering.limCone_body_is_lift {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) (k m : ℕ) :

(CategoryTheory.ConcreteCategory.hom ((Descriptive.Tree.resEq m).map (mapIneqRec n k).toHom)) ((limConeBodyLifts hF S y yc (k + 1)).fst.res m) = (limConeBodyLifts hF S y yc k).fst.res m

source

noncomputable def GaleStewartGame.Covering.limConeBodySystem {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) :

bodySystem.obj (limConePt hF).fst

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

theorem GaleStewartGame.Covering.consistent_cast {p : Player} {S T : Descriptive.Tree.Trees} (h : S = T) {S' : StrategySystem S p} {S'' : StrategySystem T p} (h' : S' ≍ S'') (y : bodySystem.obj S) (hc : consistent y S') :

consistent (cast ⋯ y) S''

source

theorem GaleStewartGame.Covering.cancel_resEq_inv_cast {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K k : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {m n : ℕ} (h : n = m) (h' : k ≤ m) (x : (Descriptive.Tree.resEq k).obj (F.obj (Opposite.op n)).fst) :

have this := ⋯; (CategoryTheory.ConcreteCategory.hom ((Descriptive.Tree.resEq k).map (limConeπMap hF m))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv ((Descriptive.Tree.resEq k).map (limConeπMap hF n)))) x) = cast ⋯ x

source

theorem GaleStewartGame.Covering.cancel_pInv_cast {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {m n : ℕ} (h : m = n) (x : ↑↑(F.obj (Opposite.op n)).fst.snd) [Descriptive.Tree.Fixing (↑x).length (limConeπMap hF n)] :

(CategoryTheory.ConcreteCategory.hom (limConeπMap hF m)) (Descriptive.Tree.pInv (limConeπMap hF n) x ⋯) = cast ⋯ x

source

theorem GaleStewartGame.Covering.cast_lifts' {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K k : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) {m n : ℕ} (h : m = n) {S : (LvlStratHom.system p).obj { tree := limConePt hF }} {y : bodySystem.obj (F.obj (Opposite.op (max k 0))).fst} (hy : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max k 0)))) S)) :

⟨↑((limConeBodyLifts hF S y hy n).fst.res m), ⋯⟩ = ⟨↑((limConeBodyLifts hF S y hy n).fst.res n), ⋯⟩

source

theorem GaleStewartGame.Covering.take_apply_val_resEq {S T : Descriptive.Tree.Trees} (f : S ⟶ T) (k n : ℕ) (x : (Descriptive.Tree.resEq k).obj S) :

↑((CategoryTheory.ConcreteCategory.hom f) ⟨List.take n ↑x, ⋯⟩) = List.take n ↑((CategoryTheory.ConcreteCategory.hom f) (Descriptive.Tree.resEq.val' x))

source

theorem GaleStewartGame.Covering.limCone_body_is_lift' {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) (k m : ℕ) :

(CategoryTheory.ConcreteCategory.hom (mapIneqRec n k).toHom) (Descriptive.Tree.resEq.val' ((limConeBodyLifts hF S y yc (k + 1)).fst.res m)) = Descriptive.Tree.resEq.val' ((limConeBodyLifts hF S y yc k).fst.res m)

source

theorem GaleStewartGame.Covering.limConeBodySystem_map_contains {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) (x : ↑↑(limConePt hF).fst.snd) (hc : (BodySystemObj.ofObj (limConeBodySystem hF S y yc)).containsTree x) :

(BodySystemObj.ofObj (limConeBodyLifts hF S y yc ((↑x).length + 1)).fst).containsTree ((CategoryTheory.ConcreteCategory.hom (limConeπMap hF (max n ((↑x).length + 1)))) x)

source

theorem GaleStewartGame.Covering.limConeBodySystem_project {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) (k : ℕ) :

(CategoryTheory.ConcreteCategory.hom (limConeπMap hF (max n k))) (Descriptive.Tree.resEq.val' ((limConeBodySystem hF S y yc).res k)) = Descriptive.Tree.resEq.val' ((limConeBodyLifts hF S y yc k).fst.res k)

source

theorem GaleStewartGame.Covering.limCone_body_consistent {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) :

consistent (limConeBodySystem hF S y yc) S

source

theorem GaleStewartGame.Covering.cast_apply_F {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {k m n n' : ℕ} (h : n ≤ m) (hn : n = n') (x : (Descriptive.Tree.resEq k).obj (F.obj (Opposite.op m)).fst) (hpr2 : ↑x ∈ ↑(F.obj (Opposite.op m)).fst.snd) (hpr1 : ↑x ∈ (F.obj (Opposite.op m)).fst.snd) :

↑((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE h).op).toHom) ⟨↑x, hpr1⟩) = cast ⋯ ↑((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op).toHom) ⟨↑x, hpr2⟩)

source

theorem GaleStewartGame.Covering.lifts_cast_lifts {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {m n m' n' : ℕ} (hm : m = m') (hn : n = n') (y : bodySystem.obj (F.obj (Opposite.op m)).fst) :

cast ⋯ ↑((cast ⋯ y).res n) = ↑(y.res n')

source

theorem GaleStewartGame.Covering.limCone_body_is_lift_fin {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op (max n 0))).fst) (yc : consistent y ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) (k m : ℕ) :

↑((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op).toHom) (Descriptive.Tree.resEq.val' ((limConeBodyLifts hF S y yc k).fst.res m))) = ↑(y.res m)

source

theorem GaleStewartGame.Covering.limConeBodySystem_lift {p : Player} {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K n : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (S : (LvlStratHom.system p).obj { tree := limConePt hF }) (y : bodySystem.obj (F.obj (Opposite.op n)).fst) (yc : consistent (cast ⋯ y) ((CategoryTheory.ConcreteCategory.hom ((LvlStratHom.system p).map (limConeStr hF (max n 0)))) S)) :

(CategoryTheory.ConcreteCategory.hom (bodySystem.map (limConeπMap hF n))) (limConeBodySystem hF S (cast ⋯ y) yc) = y

source

noncomputable def GaleStewartGame.Covering.limConeπ {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (n : ℕ) :

limConePt hF ⟶ F.obj (Opposite.op n)

Auxiliary declaration for the Borel determinacy formalization.

Equations

GaleStewartGame.Covering.limConeπ hF n = { toHom := GaleStewartGame.Covering.limConeπMap hF n, str := GaleStewartGame.Covering.limConeStr hF n, h_body := ⋯ }

Instances For

source

noncomputable def GaleStewartGame.Covering.limCone {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) :

CategoryTheory.Limits.Cone F

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

theorem GaleStewartGame.Covering.limCone_fixing {F : CategoryTheory.Functor ℕ ᵒᵖ PTrees} {K : ℕ} (hF : ∀ (k : ℕ), Fixing (K + k) (F.map (CategoryTheory.homOfLE ⋯).op)) (n : ℕ) :

Fixing (K + n) ((limCone hF).π.app (Opposite.op n))