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

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

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

@[simp]

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