subtrees — Mathlib

English

All immediate subtrees of a rooted tree are exactly those rooted at atoms.

Русский

Все непосредственные поддеревья корневого дерева равны тем, что корень каждого из них является атомом.

LaTeX

$$def subtrees (t) : Set (SubRootedTree t) := {x | IsAtom x.root}$$

Lean4

/-- All of the immediate subtrees of a given rooted tree, that is subtrees which are rooted at a direct
child of the root (or, order-theoretically, at an atom).
-/
def subtrees (t : RootedTree) : Set (SubRootedTree t) :=
  {x | IsAtom x.root}

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