English
pullSub(T,x) consists of y such that y.take(length(x)) is a prefix of x and y.drop(length(x)) ∈ T; i.e., a re-rooted tree by inserting x before the root.
Русский
pullSub(T,x) состоит из таких y, что y.take(|x|) является префиксом x и y.drop(|x|) ∈ T; то есть дерево заново корневое, полученное вставкой x перед корнем.
LaTeX
$$$ \\mathrm{pullSub}(T, x) = \\{ y \\mid y.take(|x|) \\text{ является префиксом } x \\land y.drop(|x|) \\in T \\}$$$
Lean4
/-- 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 -/
def pullSub : tree A where
val := {y | y.take x.length <+: x ∧ y.drop x.length ∈ T}
property := fun y a ⟨h1, h2⟩ ↦
⟨((y.prefix_append [a]).take x.length).trans h1, mem_of_prefix ((y.prefix_append [a]).drop x.length) h2⟩
