English
Let T be a tree on A, i.e., a complete sublattice of Set(List A) closed under prefixes. Then if x ++ y ∈ T, necessarily x ∈ T.
Русский
Пусть T — дерево над A; то есть множество конечных последовательностей из List(A), замкнутое по префиксам. Тогда если x ++ y ∈ T, то обязательно x ∈ T.
LaTeX
$$$ x,y \\in \\mathrm{List}(A) \\quad (x \\!+\\!+\\; y) \\in T \\Rightarrow x \\in T $$$
Lean4
/-- 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`. -/
def tree (A : Type*) : CompleteSublattice (Set (List A)) :=
CompleteSublattice.mk' {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
(by rintro S hS x a ⟨t, ht, hx⟩; use t, ht, hS ht hx) (by rintro S hS x a h T hT; exact hS hT <| h T hT)
