LeanPool.AFormalizationOfBorelDeterminacyInLean.Tree.TreeBody

Auxiliary declarations for the Borel determinacy formalization.

def Descriptive.Tree.body {A : Type u_1} (T : ↥(tree A)) : Set (Stream' A)

The body of a tree T, also written [T] in the literature, is the set of infinite branches, implemented as Stream

Equations

• Descriptive.Tree.body T = {y : Stream' A | ∀ (x : List A), y ∈ Stream'.Discrete.principalOpen x → x ∈ T}

theorem Descriptive.Tree.body_mono {A : Type u_1} {S T : ↥(tree A)} (h : S ≤ T) : body S ⊆ body T

@[simp]

theorem Descriptive.Tree.take_mem_body {A : Type u_1} {T : ↥(tree A)} {x : Stream' A} (h : x ∈ body T) (n : ℕ) : Stream'.take n x ∈ T

Auxiliary declaration for the Borel determinacy formalization.

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

Auxiliary declaration for the Borel determinacy formalization.

Equations

• Descriptive.Tree.body.take n x = ⟨Stream'.take n ↑x, ⋯⟩

@[simp]

theorem Descriptive.Tree.body.take_coe {A : Type u_1} {T : ↥(tree A)} (n : ℕ) (x : ↑(body T)) : ↑(take n x) = Stream'.take n ↑x

theorem Descriptive.Tree.mem_body_of_take {A : Type u_1} (m : ℕ) (T : ↥(tree A)) (x : Stream' A) (h : ∀ n ≥ m, Stream'.take n x ∈ T) : x ∈ body T

def Descriptive.Tree.bodyInfHom {A : Type u_1} : sInfHom (↥(tree A)) (Set (Stream' A))

Taking bodies preserves arbitrary intersections

Equations

• Descriptive.Tree.bodyInfHom = { toFun := Descriptive.Tree.body, map_sInf' := ⋯ }

@[simp]

theorem Descriptive.Tree.body_inter {A : Type u_1} {S T : ↥(tree A)} : body (S ⊓ T) = body S ∩ body T

@[simp]

theorem Descriptive.Tree.body_bot {A : Type u_1} : body ⊥ = ∅

@[simp]

theorem Descriptive.Tree.body_isClosed {A : Type u_1} (T : ↥(tree A)) : IsClosed (body T)

@[simp]

theorem Descriptive.Tree.subAt_body {A : Type u_1} (T : ↥(tree A)) (x : List A) : body (subAt T x) = (fun (x_1 : Stream' A) => x ++ₛ x_1) ⁻¹' body T

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

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

Equations

• Descriptive.Tree.body.append x y = ⟨x ++ₛ ↑y, ⋯⟩

@[simp]

theorem Descriptive.Tree.body.append_coe {A : Type u_1} {T : ↥(tree A)} (x : List A) (y : ↑(body (subAt T x))) : ↑(append x y) = x ++ₛ ↑y

@[simp]

theorem Descriptive.Tree.body_append_nil {A : Type u_1} (T : ↥(tree A)) (y : ↑(body T)) : body.append [] y = y

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

theorem Descriptive.Tree.range_body_append {A : Type u_1} (T : ↥(tree A)) (x y : List A) (h : x = y) : Set.range (body.append x) = Set.range (body.append y)

@[simp]

theorem Descriptive.Tree.subtype_body_append {A : Type u_1} (T : ↥(tree A)) (x : List A) : Subtype.val '' Set.range (body.append x) = Stream'.Discrete.principalOpen x ∩ body T

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

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

Equations

• Descriptive.Tree.body.drop n x = ⟨Stream'.drop n ↑x, ⋯⟩

@[simp]

theorem Descriptive.Tree.body.drop_coe {A : Type u_1} {T : ↥(tree A)} (n : ℕ) (x : ↑(body T)) : ↑(drop n x) = Stream'.drop n ↑x

@[simp]

theorem Descriptive.Tree.subAt_body_image {A : Type u_1} {T : ↥(tree A)} (X : Set ↑(body T)) (x : List A) : Subtype.val '' body.append x ⁻¹' X = (fun (x_1 : Stream' A) => x ++ₛ x_1) ⁻¹' Subtype.val '' X

theorem Descriptive.Tree.subAt_body_image_compl {A : Type u_1} {T : ↥(tree A)} (X : Set ↑(body T)) (x : List A) : Subtype.val '' (body.append x ⁻¹' X)ᶜ = (fun (x_1 : Stream' A) => x ++ₛ x_1) ⁻¹' body T \ (fun (x_1 : Stream' A) => x ++ₛ x_1) ⁻¹' Subtype.val '' X

theorem Descriptive.Tree.subAt_body_image_compl_preimage {A : Type u_1} {T : ↥(tree A)} (X : Set ↑(body T)) (x y : List A) : (fun (a : Stream' A) => y ++ₛ a) ⁻¹' Subtype.val '' (body.append x ⁻¹' X)ᶜ = (fun (a : Stream' A) => x ++ₛ (y ++ₛ a)) ⁻¹' body T \ (fun (a : Stream' A) => x ++ₛ (y ++ₛ a)) ⁻¹' Subtype.val '' X

theorem Descriptive.Tree.subAt_body_image_compl_compl_preimage {A : Type u_1} {T : ↥(tree A)} (X : Set ↑(body T)) (x y : List A) : (fun (a : Stream' A) => y ++ₛ a) ⁻¹' Subtype.val '' (body.append x ⁻¹' X)ᶜᶜ = (fun (a : Stream' A) => x ++ₛ (y ++ₛ a)) ⁻¹' Subtype.val '' X

theorem Descriptive.Tree.mem_subAt_body {A : Type u_1} {T : ↥(tree A)} (X : Set ↑(body T)) (x : List A) (y : ↑(body (subAt T x))) : y ∈ body.append x ⁻¹' X ↔ x ++ₛ ↑y ∈ Subtype.val '' X

@[simp]

theorem Descriptive.Tree.pullSub_body {A : Type u_1} (T : ↥(tree A)) (x : List A) : body (pullSub T x) = (fun (x_1 : Stream' A) => x ++ₛ x_1) '' body T

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

theorem Descriptive.Tree.isPruned_iff_principalOpen_ne {A : Type u_1} {T : ↥(tree A)} : IsPruned T ↔ ∀ (x : ↥T), (Stream'.Discrete.principalOpen ↑x ∩ body T).Nonempty