LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.BodyFunctor

Auxiliary declarations for the Borel determinacy formalization.

def Descriptive.Tree.bodyDom {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) : Set (Stream' A)

The set of points in body S where the body map of f is defined

Equations

• Descriptive.Tree.bodyDom f = {a : Stream' A | a ∈ Descriptive.Tree.body S ∧ Set.Unbounded Nat.le ((fun (x : ↥S) => (↑(f x)).length) '' {x : ↥S | a ∈ Stream'.Discrete.principalOpen ↑x})}

theorem Descriptive.Tree.bodyMap_uniq {A : Type u_1} {A' : Type u_2} {n : ℕ} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) {a : Stream' A} {x y : List A} {ha : a ∈ body S} (hx : a ∈ Stream'.Discrete.principalOpen x) (hy : a ∈ Stream'.Discrete.principalOpen y) (hlx : n < (↑(f ⟨x, ⋯⟩)).length) (hly : n < (↑(f ⟨y, ⋯⟩)).length) : (↑(f ⟨x, ⋯⟩))[n] = (↑(f ⟨y, ⋯⟩))[n]

theorem Descriptive.Tree.bodyMap_exists {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) (a : ↑(bodyDom f)) (n : ℕ) : ∃ (x : ↥S), ↑a ∈ Stream'.Discrete.principalOpen ↑x ∧ n < (↑(f x)).length

noncomputable def Descriptive.Tree.bodyMapChooseSpec {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) (a : ↑(bodyDom f)) (n : ℕ) : ↥T

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.bodyMapChooseSpec f a n = f ⟨↑⋯.choose, ⋯⟩

noncomputable def Descriptive.Tree.bodyMapVal {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) (a : ↑(bodyDom f)) : Stream' A'

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.bodyMapVal f a n = (↑(f ⋯.choose))[n]

theorem Descriptive.Tree.bodyMap_pspec {A : Type u_1} {A' : Type u_2} {n : ℕ} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) (a : ↑(bodyDom f)) {x : List A} (hx : ↑a ∈ Stream'.Discrete.principalOpen x) (hlx : n < (↑(f ⟨x, ⋯⟩)).length) : (bodyMapVal f a).get n = (↑(f ⟨x, ⋯⟩))[n]

noncomputable def Descriptive.Tree.bodyMap {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) (a : ↑(bodyDom f)) : ↑(body T)

The induced map on branches

Equations

• Descriptive.Tree.bodyMap f a = ⟨Descriptive.Tree.bodyMapVal f a, ⋯⟩

theorem Descriptive.Tree.bodyMap_spec {A : Type u_1} {A' : Type u_2} {n : ℕ} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) (a : ↑(bodyDom f)) {x : List A} (hx : ↑a ∈ Stream'.Discrete.principalOpen x) (hlx : n < (↑(f ⟨x, ⋯⟩)).length) : (↑(bodyMap f a)).get n = (↑(f ⟨x, ⋯⟩))[n]

theorem Descriptive.Tree.bodyMap_continuous {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) : Continuous (bodyMap f)

@[simp]

theorem Descriptive.Tree.bodyDom_univ {S T : Trees} (f : S ⟶ T) : bodyDom f.toOrderHom = body S.snd

if f is length-preserving, then its body map is defined everywhere

noncomputable def Descriptive.Tree.bodyPre : Trees ⥤q Type u_3

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

@[simp]

theorem Descriptive.Tree.bodyPre_obj (S : Trees) : bodyPre.obj S = ↑(body S.snd)

theorem Descriptive.Tree.bodyPre_obj_ext {S : Trees} {x y : bodyPre.obj S} (h : ↑x = ↑y) : x = y

theorem Descriptive.Tree.bodyPre_obj_ext_iff {S : Trees} {x y : bodyPre.obj S} : x = y ↔ ↑x = ↑y

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

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

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

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

noncomputable def Descriptive.Tree.bodyFunctor : CategoryTheory.Functor Trees (Type u_3)

the body of a tree is functorial

Equations

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

@[simp]

theorem Descriptive.Tree.bodyFunctor_obj (S : Trees) : bodyFunctor.obj S = ↑(body S.snd)

@[implicit_reducible]

instance Descriptive.Tree.bodySpace {S : Trees} : TopologicalSpace (bodyFunctor.obj S)

Equations

• Descriptive.Tree.bodySpace = { IsOpen := Descriptive.Tree.bodySpace._aux_1, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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

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

theorem Descriptive.Tree.bodyMap_spec_res' {S T : Trees} (f : S ⟶ T) (a : ↑(body S.snd)) (n : ℕ) : (↑((CategoryTheory.ConcreteCategory.hom (bodyFunctor.map f)) a)).get n = (↑((CategoryTheory.ConcreteCategory.hom f) ⟨Stream'.take (n + 1) ↑a, ⋯⟩))[n]

theorem Descriptive.Tree.bodyMap_restrict {S T : Trees} (f : S ⟶ T) (a : (fun (X : Type u_3) => X) (bodyFunctor.obj S)) (n : ℕ) : Stream'.take n ↑((CategoryTheory.ConcreteCategory.hom (bodyFunctor.map f)) a) = ↑((CategoryTheory.ConcreteCategory.hom f) (body.take n a))

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