equivTree — Mathlib

English

There is a natural bijection between Dyck words and rooted binary trees.

Русский

Существует естественная биекция между DyckWord и корневыми двоичными деревьями.

LaTeX

$$$ \text{DyckWord} \simeq \text{Tree Unit} $ (bijection between Dyck words and rooted binary trees)$$

Lean4

/-- Equivalence between Dyck words and rooted binary trees. -/
def equivTree : DyckWord ≃ Tree Unit where
  toFun := equivTreeToFun
  invFun := equivTreeInvFun
  left_inv := equivTree_left_inv
  right_inv := equivTree_right_inv

Похожие утверждения