Size measures on unordered trees and their forests

Main definitions

• UnorderedTree.numEdges: the edge count numNodes - 1 of a rooted tree.

Main results

• UnorderedTree.sum_map_numNodes: Euler's relation #V = b₀ + #E for forests, with Multiset.card the component count.
• UnorderedTree.countP_leaves_le_numEdges: counted leaves are among the non-root vertices whenever some vertex is uncounted.

def UnorderedTree.numEdges {α : Type u_1} (t : UnorderedTree α) : ℕ

The number of edges of a rooted tree, numNodes - 1: every vertex except the root has exactly one parent edge.

Equations

• t.numEdges = t.numNodes - 1

@[simp]

theorem UnorderedTree.numEdges_leaf {α : Type u_1} (a : α) : (leaf a).numEdges = 0

theorem UnorderedTree.numEdges_eq_numNodes_sub_one {α : Type u_1} (t : UnorderedTree α) : t.numEdges = t.numNodes - 1

theorem UnorderedTree.numEdges_add_one {α : Type u_1} (t : UnorderedTree α) : t.numEdges + 1 = t.numNodes

Euler's relation for a rooted tree: #V = 1 + #E.

theorem UnorderedTree.numEdges_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).numEdges = (Multiset.map numNodes F).sum

The edges of a node are the root-to-child edges plus each child's own: the total vertex count of the children.

theorem UnorderedTree.numEdges_node_pair {α : Type u_1} (a : α) (l r : UnorderedTree α) : (node a {l, r}).numEdges = l.numEdges + r.numEdges + 2

Adjoining a root above a pair of trees adds two edges.

theorem UnorderedTree.numNodes_node_pair {α : Type u_1} (a : α) (l r : UnorderedTree α) : (node a {l, r}).numNodes = l.numNodes + r.numNodes + 1

Adjoining a root above a pair of trees adds one vertex.

theorem UnorderedTree.countP_leaves_le_numEdges {α : Type u_1} (p : α → Prop) [DecidablePred p] (t : UnorderedTree α) (h : Multiset.countP p t.leaves < t.numNodes) : Multiset.countP p t.leaves ≤ t.numEdges

Counted leaves are among the non-root vertices whenever some vertex is uncounted.

theorem UnorderedTree.sum_map_numNodes {α : Type u_1} (F : Multiset (UnorderedTree α)) : (Multiset.map numNodes F).sum = F.card + (Multiset.map numEdges F).sum

Euler's relation for forests: #V = b₀ + #E, with Multiset.card the number of component trees.