Main results

• treesOfNumNodesEq_card_eq_catalan: The number of binary trees with n internal nodes is catalan n

@[reducible, inline]

abbrev Tree.pairwiseNode (a b : Finset (Tree Unit)) : Finset (Tree Unit)

Given two finsets, find all trees that can be formed with left child in a and right child in b

Equations

• Tree.pairwiseNode a b = Finset.map { toFun := fun (x : Tree Unit × Tree Unit) => Tree.node () x.1 x.2, inj' := Tree.pairwiseNode._proof_1 } (a ×ˢ b)

@[irreducible]

def Tree.treesOfNumNodesEq : ℕ → Finset (Tree Unit)

A Finset of all trees with n nodes. See mem_treesOfNodesEq

Equations

• One or more equations did not get rendered due to their size.
• Tree.treesOfNumNodesEq 0 = {Tree.nil}

@[simp]

theorem Tree.treesOfNumNodesEq_zero : treesOfNumNodesEq 0 = {nil}

theorem Tree.treesOfNumNodesEq_succ (n : ℕ) : treesOfNumNodesEq (n + 1) = (Finset.antidiagonal n).biUnion fun (ij : ℕ × ℕ) => pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

@[simp]

theorem Tree.mem_treesOfNumNodesEq {x : Tree Unit} {n : ℕ} : x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

theorem Tree.mem_treesOfNumNodesEq_numNodes (x : Tree Unit) : x ∈ treesOfNumNodesEq x.numNodes

@[simp]

theorem Tree.coe_treesOfNumNodesEq (n : ℕ) : ↑(treesOfNumNodesEq n) = {x : Tree Unit | x.numNodes = n}

theorem Tree.treesOfNumNodesEq_card_eq_catalan (n : ℕ) : (treesOfNumNodesEq n).card = catalan n