subtreeOf_mem_subtrees — Mathlib

English

Let t be a rooted tree with decidable equality on its vertices. For any vertex v of t with v not equal to the bottom element, the subtree rooted at v is one of the subtrees of t.

Русский

Пусть t — корневое дерево с корректным равенством вершин. Для любой вершины v в t, если v ≠ нижний элемент, поддерево, корневое в v, принадлежит множеству поддеревьев t.

LaTeX

$$$\forall t \ (\text{DecidableEq } t) \;\forall v \in t,\ v \neq \perp \Rightarrow t.\text{subtreeOf}(v) \in t.\text{subtrees}.$$

Lean4

theorem subtreeOf_mem_subtrees [DecidableEq t] {v : t} (hr : v ≠ ⊥) : t.subtreeOf v ∈ t.subtrees := by
  simpa [RootedTree.subtrees, RootedTree.subtreeOf]

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