Finiteness of size classes

There are finitely many plane trees with a bounded number of vertices. The proof uses the list of root-child subtrees: for a tree of size at most n + 1, there are at most n children, each having size at most n.

theorem BGW.PlaneTree.finite_size_le (n : ℕ) : {t : PlaneTree | t.size ≤ n}.Finite

Only finitely many plane trees have at most n vertices.

theorem BGW.PlaneTree.finite_size_eq (n : ℕ) : {t : PlaneTree | t.size = n}.Finite

Only finitely many plane trees have exactly n vertices.