Main results

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

@[reducible, inline]

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

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

Equations

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

@[irreducible]

def BinaryTree.treesOfNumNodesEq : ℕ → Finset (BinaryTree 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.
• BinaryTree.treesOfNumNodesEq 0 = {BinaryTree.nil}

@[reducible, inline, deprecated BinaryTree.treesOfNumNodesEq (since := "2026-06-07")]

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

Alias of BinaryTree.treesOfNumNodesEq.

Equations

• Tree.treesOfNumNodesEq = BinaryTree.treesOfNumNodesEq

@[simp]

theorem BinaryTree.treesOfNumNodesEq_zero : treesOfNumNodesEq 0 = {nil}

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

@[simp]

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

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

@[simp]

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

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