Subtrees of nonplanar trees

UnorderedTree.subtrees t is the multiset of all subtrees of t, the root included, one per vertex, so its cardinality is t.numNodes. It is defined on planar representatives and descends to the quotient because a permutation of children permutes the subtree multiset.

Main definitions

• UnorderedTree.subtrees

Main results

• UnorderedTree.card_subtrees: one subtree per vertex.
• UnorderedTree.mem_subtrees_node_pair: membership at a binary node.

def RoseTree.unorderedSubtrees {α : Type u_1} : RoseTree α → Multiset (UnorderedTree α)

The nonplanar subtrees of a planar tree, root included.

Equations

• (RoseTree.node a cs).unorderedSubtrees = UnorderedTree.mk (RoseTree.node a cs) ::ₘ RoseTree.unorderedSubtreesList cs

def RoseTree.unorderedSubtreesList {α : Type u_1} : List (RoseTree α) → Multiset (UnorderedTree α)

The nonplanar subtrees of a list of trees.

Equations

• RoseTree.unorderedSubtreesList [] = 0
• RoseTree.unorderedSubtreesList (c :: cs) = c.unorderedSubtrees + RoseTree.unorderedSubtreesList cs

theorem RoseTree.unorderedSubtrees_perm {α : Type u_1} {t s : RoseTree α} : t.Perm s → t.unorderedSubtrees = s.unorderedSubtrees

theorem RoseTree.unorderedSubtreesList_permList {α : Type u_1} {cs ds : List (RoseTree α)} : PermList cs ds → unorderedSubtreesList cs = unorderedSubtreesList ds

theorem RoseTree.card_unorderedSubtrees {α : Type u_1} (p : RoseTree α) : p.unorderedSubtrees.card = p.numNodes

theorem RoseTree.card_unorderedSubtreesList {α : Type u_1} (cs : List (RoseTree α)) : (unorderedSubtreesList cs).card = (List.map numNodes cs).sum

def UnorderedTree.subtrees {α : Type u_1} : UnorderedTree α → Multiset (UnorderedTree α)

All subtrees of a nonplanar tree, root included.

Equations

• UnorderedTree.subtrees = UnorderedTree.lift RoseTree.unorderedSubtrees ⋯

@[simp]

theorem UnorderedTree.subtrees_mk {α : Type u_1} (t : RoseTree α) : (mk t).subtrees = t.unorderedSubtrees

theorem UnorderedTree.subtrees_leaf {α : Type u_1} (a : α) : (leaf a).subtrees = {leaf a}

theorem UnorderedTree.subtrees_node_pair {α : Type u_1} (a : α) (l r : UnorderedTree α) : (node a {l, r}).subtrees = node a {l, r} ::ₘ (l.subtrees + r.subtrees)

@[simp]

theorem UnorderedTree.mem_subtrees_leaf {α : Type u_1} {m : UnorderedTree α} {a : α} : m ∈ (leaf a).subtrees ↔ m = leaf a

@[simp]

theorem UnorderedTree.mem_subtrees_node_pair {α : Type u_1} {m : UnorderedTree α} {a : α} {l r : UnorderedTree α} : m ∈ (node a {l, r}).subtrees ↔ m = node a {l, r} ∨ m ∈ l.subtrees ∨ m ∈ r.subtrees

theorem UnorderedTree.self_mem_subtrees {α : Type u_1} (t : UnorderedTree α) : t ∈ t.subtrees

theorem UnorderedTree.card_subtrees {α : Type u_1} (t : UnorderedTree α) : t.subtrees.card = t.numNodes

One subtree per vertex.