Theorems · Definition · combinatorics
DyckWord.toTree
DyckWord → BinaryTree Unit
Convert a Dyck word to a binary rooted tree.
f(0) = nil. For a nonzero word find the D that matches the initial U,
which has index p.firstReturn, then let x be everything strictly between said U and D,
and y be everything strictly after said D. p = x.nest + y with x, y (possibly empty)
Dyck words. f(p) = f(x) △ f(y), where △ (defined in Mathlib/Data/Tree/Basic.lean) joins two
subtrees to a new root node.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DyckWordstatement and proof · cited by 59
- BinaryTreestatement and proof · cited by 41
- DyckWord.semilengthproof · cited by 17
- DyckWord.outsidePartproof · cited by 12
- DyckWord.insidePartproof · cited by 12
Cited by8
Results whose statement or proof uses this declaration.
- DyckWord.equivTreeproof · cited by 2
- DyckWord.numNodes_toTreestatement and proof · cited by 1
- DyckWord.toTree_ofTreestatement · cited by 0
- DyckWord.equivTree_applystatement · cited by 0
- DyckWord.equivTreesOfNumNodesEq_apply_coestatement · cited by 0
- DyckWord.ofTree_toTreestatement and proof · cited by 0
- DyckWord.toTree.eq_defstatement and proof · cited by 0
- DyckWord.semilength_eq_numNodes_equivTreestatement · cited by 0