subAt — Mathlib

English

The residual tree obtained by re-rooting at x is the preimage of the original tree under the function y → x ++ y.

Русский

Остаточное дерево, полученное при повторной корневой перестройке на x, является предпобразом исходного дерева по функции y → x ++ y.

LaTeX

$$$ \\mathrm{subAt}(T, x) = \\{ y : \\mathrm{List}(A) \\mid x ++ y \\in T \\} $$$

Lean4

/-- The residual tree obtained by regarding the node x as new root -/
def subAt : tree A :=
  ⟨(x ++ ·) ⁻¹' T, fun _ _ _ ↦ mem_of_append (by rwa [List.append_assoc])⟩

Похожие утверждения