Cardinality of the leaf carrier

PlaneTree.leafCount is the recursive paper-facing number of leaves, while PlaneTree.Leaves is the finite subtype used by the Lean implementation. This file proves that the two notions agree for every plane tree, including invalid trees with unary vertices.

theorem Anderson4D.PlaneTree.card_Leaves_eq_leafCount (t : PlaneTree) : t.Leaves.card = t.leafCount

The finite leaf carrier has exactly the recursive paper-facing leaf count. No Hepp-validity assumption is needed.

theorem Anderson4D.PlaneTree.card_leaves_eq_leafCount (t : PlaneTree) : t.Leaves.card = t.leafCount

Lower-case compatibility spelling used by the Hepp-tree cardinality lemmas.

The root-subtree bridge

@[simp]

theorem Anderson4D.PlaneTree.leavesUnder_root_eq_univ (t : PlaneTree) : leavesUnder t.rootV = Finset.univ

Every leaf lies under the root.

@[simp]

theorem Anderson4D.PlaneTree.card_leavesUnder_root (t : PlaneTree) : (leavesUnder t.rootV).card = t.leafCount

The leaves below the root are all paper leaves.