English
There is a finite set T(n) of trees with exactly n nodes, defined recursively by T(0) = { nil } and T(n+1) = ⋃_{(i,j)∈Antidiagonal(n)} pairwiseNode(T(i), T(j)).
Русский
Существует конечное множество T(n) деревьев с ровно n узлами, задаваемое рекуррентно: T(0) = { nil } и T(n+1) = ⋃_{(i,j)∈Antidiagonal(n)} pairwiseNode(T(i), T(j)).
LaTeX
$$$\\mathrm{Trees}(0) = \\{\\mathrm{nil}\\},\\quad \\mathrm{Trees}(n+1) = \\bigcup_{(i,j)\\in \\mathrm{Antidiagonal}(n)} \\mathrm{pairwiseNode}(\\mathrm{Trees}(i), \\mathrm{Trees}(j)).$$$
Lean4
/-- A Finset of all trees with `n` nodes. See `mem_treesOfNodesEq` -/
def treesOfNumNodesEq : ℕ → Finset (Tree Unit)
| 0 => { nil }
| n + 1 =>
(antidiagonal n).attach.biUnion fun ijh => pairwiseNode (treesOfNumNodesEq ijh.1.1) (treesOfNumNodesEq ijh.1.2)
decreasing_by
· simp_wf; have := fst_le ijh.2; cutsat
· simp_wf; have := snd_le ijh.2; cutsat
