English
There is an equivalence between the subtype { p ∈ DyckWord | p.semilength = n } and treesWithNumNodesEq n.
Русский
Существует эквивалентность между подмножеством слов DyckWord с semilength = n и деревьями с количеством узлов n.
LaTeX
$$$ { p : DyckWord // p.semilength = n } \\simeq treesOfNumNodesEq\,n $$$
Lean4
/-- Equivalence between Dyck words of semilength `n` and rooted binary trees with
`n` internal nodes. -/
def equivTreesOfNumNodesEq (n : ℕ) : { p : DyckWord // p.semilength = n } ≃ treesOfNumNodesEq n
where
toFun := fun ⟨p, _⟩ ↦ ⟨equivTree p, by rwa [mem_treesOfNumNodesEq, ← semilength_eq_numNodes_equivTree]⟩
invFun := fun ⟨tr, _⟩ ↦
⟨equivTree.symm tr, by rwa [semilength_eq_numNodes_equivTree, ← mem_treesOfNumNodesEq, Equiv.apply_symm_apply]⟩
left_inv _ := by simp only [Equiv.symm_apply_apply]
right_inv _ := by simp only [Equiv.apply_symm_apply]
