Trees in the sense of descriptive set theory

This file defines trees of depth ω in the sense of descriptive set theory as sets of finite sequences that are stable under taking prefixes.

Main declarations

• tree A: a (possibly infinite) tree of depth at most ω with nodes in A

def Descriptive.tree (A : Type u_1) : CompleteSublattice (Set (List A))

A tree is a set of finite sequences, implemented as List A, that is stable under taking prefixes. For the definition we use the equivalent property x ++ [a] ∈ T → x ∈ T, which is more convenient to check. We define tree A as a complete sublattice of Set (List A), which coerces to the type of trees on A.

Equations

• Descriptive.tree A = CompleteSublattice.mk' {T : Set (List A) | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T} ⋯ ⋯

instance Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree (A : Type u_1) : SetLike (↥(tree A)) (List A)

Equations

• Descriptive.instSetLikeSubtypeSetListMemCompleteSublatticeTree A = SetLike.instSubtypeSet

@[simp]

theorem Descriptive.coe_def (A : Type u_1) (self : ↥(tree A)) : ↑self = ↑self

theorem Descriptive.Tree.mem_of_append {A : Type u_1} {T : ↥(tree A)} {x y : List A} (h : x ++ y ∈ T) : x ∈ T

theorem Descriptive.Tree.mem_of_prefix {A : Type u_1} {T : ↥(tree A)} {x y : List A} (h' : x <+: y) (h : y ∈ T) : x ∈ T

instance Descriptive.Tree.instTransListSubtypeSetMemCompleteSublatticeTreeIsPrefix {A : Type u_1} : Trans List.IsPrefix (fun (x : List A) (T : ↥(tree A)) => x ∈ T) fun (x : List A) (T : ↥(tree A)) => x ∈ T

Equations

• Descriptive.Tree.instTransListSubtypeSetMemCompleteSublatticeTreeIsPrefix = { trans := ⋯ }

theorem Descriptive.Tree.singleton_mem {A : Type u_1} (T : ↥(tree A)) {a : A} {x : List A} (h : a :: x ∈ T) : [a] ∈ T

@[simp]

theorem Descriptive.Tree.tree_eq_bot {A : Type u_1} {T : ↥(tree A)} : T = ⊥ ↔ [] ∉ T

theorem Descriptive.Tree.take_mem {A : Type u_1} {T : ↥(tree A)} {n : ℕ} (x : ↥T) : List.take n ↑x ∈ T

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

A variant of List.take internally to a tree

Equations

• Descriptive.Tree.take n x = ⟨List.take n ↑x, ⋯⟩

@[simp]

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

@[simp]

theorem Descriptive.Tree.take_take {A : Type u_1} {T : ↥(tree A)} (m n : ℕ) (x : ↥T) : take m (take n x) = take (min m n) x

@[simp]

theorem Descriptive.Tree.take_eq_take {A : Type u_1} {T : ↥(tree A)} {x : ↥T} {m n : ℕ} : take m x = take n x ↔ min m (↑x).length = min n (↑x).length

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

The residual tree obtained by regarding the node x as new root

Equations

• Descriptive.Tree.subAt T x = ⟨(fun (x_1 : List A) => x ++ x_1) ⁻¹' ↑T, ⋯⟩

@[simp]

theorem Descriptive.Tree.mem_subAt {A : Type u_1} (T : ↥(tree A)) (x y : List A) : y ∈ subAt T x ↔ x ++ y ∈ T

@[simp]

theorem Descriptive.Tree.subAt_nil {A : Type u_1} (T : ↥(tree A)) : subAt T [] = T

@[simp]

theorem Descriptive.Tree.subAt_append {A : Type u_1} (T : ↥(tree A)) (x y : List A) : subAt (subAt T x) y = subAt T (x ++ y)

theorem Descriptive.Tree.subAt_mono {A : Type u_1} {S : ↥(tree A)} (T : ↥(tree A)) (x : List A) (h : S ≤ T) : subAt S x ≤ subAt T x

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

A variant of List.drop that takes values in subAt

Equations

• Descriptive.Tree.drop T n x = ⟨List.drop n ↑x, ⋯⟩

@[simp]

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

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

Adjoint of subAt, given by pasting x before the root of T. Explicitly, elements are prefixes of x or x with an element of T appended

Equations

• Descriptive.Tree.pullSub T x = ⟨{y : List A | List.take x.length y <+: x ∧ List.drop x.length y ∈ T}, ⋯⟩

theorem Descriptive.Tree.mem_pullSub_short {A : Type u_1} {T : ↥(tree A)} {x y : List A} (hl : y.length ≤ x.length) : y ∈ pullSub T x ↔ y <+: x ∧ [] ∈ T

theorem Descriptive.Tree.mem_pullSub_long {A : Type u_1} {T : ↥(tree A)} {x y : List A} (hl : x.length ≤ y.length) : y ∈ pullSub T x ↔ ∃ z ∈ T, y = x ++ z

@[simp]

theorem Descriptive.Tree.mem_pullSub_append {A : Type u_1} {T : ↥(tree A)} {x y : List A} : x ++ y ∈ pullSub T x ↔ y ∈ T

@[simp]

theorem Descriptive.Tree.mem_pullSub_self {A : Type u_1} {T : ↥(tree A)} {x : List A} : x ∈ pullSub T x ↔ [] ∈ T

theorem Descriptive.Tree.pullSub_subAt {A : Type u_1} (T : ↥(tree A)) (x : List A) : pullSub (subAt T x) x ≤ T

@[simp]

theorem Descriptive.Tree.subAt_pullSub {A : Type u_1} (T : ↥(tree A)) (x : List A) : subAt (pullSub T x) x = T

theorem Descriptive.Tree.pullSub_mono {A : Type u_1} {S : ↥(tree A)} (T : ↥(tree A)) (h : S ≤ T) (x : List A) : pullSub S x ≤ pullSub T x

theorem Descriptive.Tree.pullSub_adjunction {A : Type u_1} (S T : ↥(tree A)) (x : List A) : pullSub S x ≤ T ↔ S ≤ subAt T x

@[simp]

theorem Descriptive.Tree.pullSub_nil {A : Type u_1} (T : ↥(tree A)) : pullSub T [] = T

@[simp]

theorem Descriptive.Tree.pullSub_append {A : Type u_1} (T : ↥(tree A)) (x y : List A) : pullSub (pullSub T y) x = pullSub T (x ++ y)