Commit 2024-08-26 13:16 f2763286

View on Github →

feat: bijection between Dyck words and rooted binary trees (#9781)

Estimated changes

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

added def DyckWord.IsNested

added theorem DyckWord.card_dyckWord_semilength_eq_catalan

modified def DyckWord.denest

modified theorem DyckWord.denest_nest

added def DyckWord.equivTree

added def DyckWord.equivTreesOfNumNodesEq

deleted theorem DyckWord.firstReturn_nest_add

added theorem DyckWord.insidePart_add

added theorem DyckWord.insidePart_nest

deleted theorem DyckWord.insidePart_nest_add

added theorem DyckWord.le_add_self

added theorem DyckWord.le_of_suffix

added theorem DyckWord.nest_denest

added theorem DyckWord.outsidePart_add

added theorem DyckWord.outsidePart_nest

deleted theorem DyckWord.outsidePart_nest_add

added theorem DyckWord.semilength_eq_numNodes_equivTree

deleted theorem DyckWord.zero_le