LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.Trees #

Auxiliary declarations for the Borel determinacy formalization.

source

def Descriptive.Tree.ExtensionsAt {A : Type u_1} {T : ↥(tree A)} (x : ↥T) :

Type u_1

Set of children of node x as elements of T

Equations

Descriptive.Tree.ExtensionsAt x = { a : A // ↑x ++ [a] ∈ T }

Instances For

source

def Descriptive.Tree.ExtensionsAt.val' {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

List A

The underlying list of a child

Equations

a.val' = ↑x ++ [↑a]

Instances For

source

def Descriptive.Tree.ExtensionsAt.valT' {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

↥T

Auxiliary declaration for the Borel determinacy formalization.

Equations

a.valT' = ⟨a.val', ⋯⟩

Instances For

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.valT'_coe {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

↑a.valT' = a.val'

source

theorem Descriptive.Tree.ExtensionsAt.ext {A : Type u_1} {T : ↥(tree A)} {x : ↥T} {a b : ExtensionsAt x} (h : ↑a = ↑b) :

a = b

source

theorem Descriptive.Tree.ExtensionsAt.ext_iff {A : Type u_1} {T : ↥(tree A)} {x : ↥T} {a b : ExtensionsAt x} :

a = b ↔ ↑a = ↑b

source

theorem Descriptive.Tree.ExtensionsAt.ext_val' {A : Type u_1} {T : ↥(tree A)} {x : ↥T} {a b : ExtensionsAt x} (h : a.val' = b.val') :

a = b

source

theorem Descriptive.Tree.ExtensionsAt.ext_valT' {A : Type u_1} {T : ↥(tree A)} {x : ↥T} {a b : ExtensionsAt x} (h : a.valT' = b.valT') :

a = b

source

def Descriptive.Tree.ExtensionsAt.drop {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} :

ExtensionsAt x ≃ ExtensionsAt (Tree.drop T n x)

Auxiliary declaration for the Borel determinacy formalization.

Equations

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

Instances For

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.drop_symm_apply_coe {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt (Tree.drop T n x)) :

↑(drop.symm a) = ↑a

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.drop_apply_coe {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt x) :

↑(drop a) = ↑a

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.val'_length {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

a.val'.length = (↑x).length + 1

source

theorem Descriptive.Tree.ExtensionsAt.val'_get_last_of_eq {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt x) (h : n = (↑x).length) :

a.val'[n] = ↑a

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.val'_get_last {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

a.val'[(↑x).length] = ↑a

source

theorem Descriptive.Tree.ExtensionsAt.val'_take_of_le {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt x) (h : n ≤ (↑x).length) :

List.take n a.val' = List.take n ↑x

source

theorem Descriptive.Tree.ExtensionsAt.val'_take_of_eq {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt x) (h : n = (↑x).length) :

List.take n a.val' = ↑x

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.val'_take {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

List.take (↑x).length a.val' = ↑x

source

theorem Descriptive.Tree.ExtensionsAt.valT'_take_of_le {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt x) (h : n ≤ (↑x).length) :

take n a.valT' = take n x

source

theorem Descriptive.Tree.ExtensionsAt.valT'_take_of_eq {A : Type u_1} {T : ↥(tree A)} {n : ℕ} {x : ↥T} (a : ExtensionsAt x) (h : n = (↑x).length) :

take n a.valT' = x

source

@[simp]

theorem Descriptive.Tree.ExtensionsAt.valT'_take {A : Type u_1} {T : ↥(tree A)} {x : ↥T} (a : ExtensionsAt x) :

take (↑x).length a.valT' = x

source

def Descriptive.Tree.IsPruned {A : Type u_1} (T : ↥(tree A)) :

Prop

A tree is pruned if it has no leaves

Equations

Descriptive.Tree.IsPruned T = ∀ (x : ↥T), Nonempty (Descriptive.Tree.ExtensionsAt x)

Instances For

source

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

IsPruned (subAt T x)

source

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

IsPruned (Tree.pullSub T x)

source

@[simp]

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

[] ∈ pullSub T x ↔ [] ∈ T

source

@[simp]

theorem Descriptive.Tree.top_isPruned {A : Type u_1} [h : Nonempty A] :

IsPruned ⊤

source

@[implicit_reducible]

instance Descriptive.Tree.instPartialOrderTree {A : Type u_1} (T : ↥(tree A)) :

PartialOrder ↑↑T

Order elements of a tree by the prefix relation

Equations

Descriptive.Tree.instPartialOrderTree T = { le := fun (x y : ↑↑T) => ↑x <+: ↑y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source

@[simp]

theorem Descriptive.Tree.lt_def {A : Type u_1} (T : ↥(tree A)) (a b : ↑↑T) :

(a < b) = ((fun (x y : ↑↑T) => ↑x <+: ↑y) a b ∧ ¬(fun (x y : ↑↑T) => ↑x <+: ↑y) b a)

source

@[simp]

theorem Descriptive.Tree.le_def {A : Type u_1} (T : ↥(tree A)) (x y : ↑↑T) :

(x ≤ y) = (↑x <+: ↑y)

source

theorem Descriptive.Tree.apply_append {A : Type u_1} {A' : Type u_2} {S : ↥(tree A)} {T : ↥(tree A')} (f : ↑↑S →o ↑↑T) {x y : List A} (h : x ++ y ∈ S) :

∃ (z : List A'), ↑(f ⟨x ++ y, h⟩) = ↑(f ⟨x, ⋯⟩) ++ z