DyckWord

📁 Source: Mathlib/Combinatorics/Enumerative/DyckWord.lean

Statistics

Metric	Count
Definitions `DyckStep`, `DyckWord`, `IsNested`, `denest`, `drop`, `equivTree`, `equivTreesOfNumNodesEq`, `firstReturn`, `insidePart`, `instFintypeSubtypeEqNatSemilength`, `instPartialOrder`, `instPreorder`, `instUniqueAddUnits`, `nest`, `ofTree`, `outsidePart`, `semilength`, `take`, `toList`, `toTree`, `evalDyckWordFirstReturn`, `instAddCancelMonoidDyckWord`, `instAddDyckWord`, `instCoeDyckWordListDyckStep`, `instDecidableEqDyckStep`, `instDecidableEqDyckWord`, `decEq`, `instInhabitedDyckStep`, `default`, `instZeroDyckWord`	30
Theorems `dichotomy`, `nest`, `card_dyckWord_semilength_eq_catalan`, `cons_tail_dropLast_concat`, `count_D_le_count_U`, `count_D_lt_count_U_of_lt_firstReturn`, `count_U_eq_count_D`, `count_take_firstReturn_add_one`, `denest_nest`, `equivTree_apply`, `equivTree_symm_apply`, `equivTreesOfNumNodesEq_apply_coe`, `equivTreesOfNumNodesEq_symm_apply_coe`, `ext`, `ext_iff`, `firstReturn_add`, `firstReturn_lt_length`, `firstReturn_nest`, `firstReturn_pos`, `firstReturn_zero`, `getLast_eq_D`, `head_eq_U`, `infix_of_le`, `insidePart_add`, `insidePart_nest`, `insidePart_zero`, `le_add_self`, `le_of_suffix`, `monotone_semilength`, `nest_denest`, `nest_insidePart_add_outsidePart`, `nest_ne_zero`, `numNodes_toTree`, `ofTree_toTree`, `outsidePart_add`, `outsidePart_nest`, `outsidePart_zero`, `pos_iff_ne_zero`, `semilength_add`, `semilength_eq_count_D`, `semilength_eq_numNodes_equivTree`, `semilength_insidePart_add_semilength_outsidePart_add_one`, `semilength_insidePart_lt`, `semilength_nest`, `semilength_outsidePart_lt`, `semilength_zero`, `strictMono_semilength`, `toList_eq_nil`, `toList_ne_nil`, `toTree_ofTree`, `two_mul_semilength_eq_length`, `zero_le`	52
Total	82

DyckStep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dichotomy` 📖	mathematical	—	`U` `D`	—	—

DyckWord

Definitions

Name	Category	Theorems
`IsNested` 📖	MathDef	1 math math: `IsNested.nest`
`denest` 📖	CompOp	2 math math: `nest_denest`, `denest_nest`
`drop` 📖	CompOp	—
`equivTree` 📖	CompOp	2 math math: `equivTree_symm_apply`, `equivTree_apply`
`equivTreesOfNumNodesEq` 📖	CompOp	2 math math: `equivTreesOfNumNodesEq_symm_apply_coe`, `equivTreesOfNumNodesEq_apply_coe`
`firstReturn` 📖	CompOp	6 math math: `firstReturn_pos`, `firstReturn_lt_length`, `firstReturn_nest`, `count_take_firstReturn_add_one`, `firstReturn_add`, `firstReturn_zero`
`insidePart` 📖	CompOp	6 math math: `insidePart_zero`, `nest_insidePart_add_outsidePart`, `insidePart_nest`, `semilength_insidePart_add_semilength_outsidePart_add_one`, `insidePart_add`, `semilength_insidePart_lt`
`instFintypeSubtypeEqNatSemilength` 📖	CompOp	1 math math: `card_dyckWord_semilength_eq_catalan`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	6 math math: `pos_iff_ne_zero`, `monotone_semilength`, `strictMono_semilength`, `le_of_suffix`, `zero_le`, `le_add_self`
`instUniqueAddUnits` 📖	CompOp	—
`nest` 📖	CompOp	8 math math: `nest_denest`, `nest_insidePart_add_outsidePart`, `firstReturn_nest`, `IsNested.nest`, `insidePart_nest`, `semilength_nest`, `outsidePart_nest`, `denest_nest`
`ofTree` 📖	CompOp	4 math math: `ofTree_toTree`, `equivTreesOfNumNodesEq_symm_apply_coe`, `equivTree_symm_apply`, `toTree_ofTree`
`outsidePart` 📖	CompOp	6 math math: `semilength_outsidePart_lt`, `nest_insidePart_add_outsidePart`, `outsidePart_add`, `semilength_insidePart_add_semilength_outsidePart_add_one`, `outsidePart_zero`, `outsidePart_nest`
`semilength` 📖	CompOp	15 math math: `semilength_outsidePart_lt`, `semilength_zero`, `semilength_add`, `two_mul_semilength_eq_length`, `equivTreesOfNumNodesEq_symm_apply_coe`, `equivTreesOfNumNodesEq_apply_coe`, `monotone_semilength`, `semilength_insidePart_add_semilength_outsidePart_add_one`, `semilength_nest`, `semilength_eq_count_D`, `strictMono_semilength`, `semilength_eq_numNodes_equivTree`, `card_dyckWord_semilength_eq_catalan`, `numNodes_toTree`, `semilength_insidePart_lt`
`take` 📖	CompOp	—
`toList` 📖	CompOp	14 math math: `count_U_eq_count_D`, `getLast_eq_D`, `two_mul_semilength_eq_length`, `cons_tail_dropLast_concat`, `head_eq_U`, `count_D_lt_count_U_of_lt_firstReturn`, `toList_eq_nil`, `count_D_le_count_U`, `firstReturn_lt_length`, `firstReturn_nest`, `count_take_firstReturn_add_one`, `ext_iff`, `semilength_eq_count_D`, `infix_of_le`
`toTree` 📖	CompOp	6 math math: `ofTree_toTree`, `equivTreesOfNumNodesEq_apply_coe`, `toTree_ofTree`, `semilength_eq_numNodes_equivTree`, `numNodes_toTree`, `equivTree_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_dyckWord_semilength_eq_catalan` 📖	mathematical	—	`Fintype.card` `DyckWord` `semilength` `instFintypeSubtypeEqNatSemilength` `catalan`	—	`Fintype.ofEquiv_card` `Tree.treesOfNumNodesEq_card_eq_catalan` `Fintype.card_congr'` `Fintype.card_coe`
`cons_tail_dropLast_concat` 📖	mathematical	—	`DyckStep` `DyckStep.U` `toList` `DyckStep.D`	—	`toList_ne_nil` `List.count_eq_one_of_mem` `List.dropLast_append_getLast` `getLast_eq_D` `head_eq_U`
`count_D_le_count_U` 📖	mathematical	—	`DyckStep` `instDecidableEqDyckStep` `DyckStep.D` `toList` `DyckStep.U`	—	—
`count_D_lt_count_U_of_lt_firstReturn` 📖	mathematical	`firstReturn`	`DyckStep` `instDecidableEqDyckStep` `DyckStep.D` `toList` `DyckStep.U`	—	`lt_of_le_of_ne` `count_D_le_count_U`
`count_U_eq_count_D` 📖	mathematical	—	`DyckStep` `instDecidableEqDyckStep` `DyckStep.U` `toList` `DyckStep.D`	—	—
`count_take_firstReturn_add_one` 📖	mathematical	—	`DyckStep` `instDecidableEqDyckStep` `DyckStep.U` `firstReturn` `toList` `DyckStep.D`	—	`firstReturn_lt_length`
`denest_nest` 📖	mathematical	—	`denest` `nest` `IsNested.nest`	—	`IsNested.nest`
`equivTree_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DyckWord` `Tree` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivTree` `toTree`	—	—
`equivTree_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Tree` `DyckWord` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivTree` `ofTree`	—	—
`equivTreesOfNumNodesEq_apply_coe` 📖	mathematical	—	`Tree` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Tree.treesOfNumNodesEq` `DFunLike.coe` `Equiv` `DyckWord` `semilength` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivTreesOfNumNodesEq` `toTree`	—	—
`equivTreesOfNumNodesEq_symm_apply_coe` 📖	mathematical	—	`DyckWord` `DFunLike.coe` `Equiv` `Tree` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Tree.treesOfNumNodesEq` `semilength` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivTreesOfNumNodesEq` `ofTree`	—	—
`ext` 📖	—	`toList`	—	—	—
`ext_iff` 📖	mathematical	—	`toList`	—	`ext`
`firstReturn_add` 📖	mathematical	—	`firstReturn` `DyckWord` `instAddDyckWord` `instZeroDyckWord` `instDecidableEqDyckWord`	—	`zero_add` `firstReturn.eq_1` `firstReturn_lt_length` `count_take_firstReturn_add_one` `LT.lt.ne'` `count_D_lt_count_U_of_lt_firstReturn`
`firstReturn_lt_length` 📖	mathematical	—	`firstReturn` `DyckStep` `toList`	—	`List.length_pos_of_ne_nil` `toList_ne_nil` `le_refl` `count_U_eq_count_D`
`firstReturn_nest` 📖	mathematical	—	`firstReturn` `nest` `DyckStep` `toList`	—	`firstReturn.eq_1` `zero_add` `count_U_eq_count_D` `count_D_le_count_U` `add_zero`
`firstReturn_pos` 📖	mathematical	—	`firstReturn`	—	`not_le` `firstReturn.eq_1` `toList_ne_nil` `instIsEmptyFalse` `cons_tail_dropLast_concat` `zero_add` `List.count_eq_one_of_mem`
`firstReturn_zero` 📖	mathematical	—	`firstReturn` `DyckWord` `instZeroDyckWord`	—	—
`getLast_eq_D` 📖	mathematical	—	`DyckStep` `toList` `DyckStep.D`	—	`count_U_eq_count_D` `count_D_le_count_U` `DyckStep.dichotomy` `List.dropLast_append_getLast`
`head_eq_U` 📖	mathematical	—	`DyckStep` `toList` `DyckStep.U`	—	`DyckStep.dichotomy` `List.count_eq_one_of_mem` `Nat.instCanonicallyOrderedAdd`
`infix_of_le` 📖	mathematical	`DyckWord` `Preorder.toLE` `instPreorder`	`DyckStep` `toList`	—	`eq_or_ne` `outsidePart_zero` `insidePart_zero` `ext_iff` `nest_insidePart_add_outsidePart`
`insidePart_add` 📖	mathematical	—	`insidePart` `DyckWord` `instAddDyckWord`	—	`count_take_firstReturn_add_one` `firstReturn_add` `take.congr_simp` `denest.congr_simp` `Unique.instSubsingleton` `firstReturn_lt_length`
`insidePart_nest` 📖	mathematical	—	`insidePart` `nest`	—	`count_take_firstReturn_add_one` `firstReturn_nest` `take.congr_simp` `denest.congr_simp` `IsNested.nest` `ext_iff` `denest_nest`
`insidePart_zero` 📖	mathematical	—	`insidePart` `DyckWord` `instZeroDyckWord`	—	`count_take_firstReturn_add_one`
`le_add_self` 📖	mathematical	—	`DyckWord` `Preorder.toLE` `instPreorder` `instAddDyckWord`	—	—
`le_of_suffix` 📖	mathematical	`DyckStep` `toList`	`DyckWord` `Preorder.toLE` `instPreorder`	—	`count_U_eq_count_D` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `ext` `le_add_self`
`monotone_semilength` 📖	mathematical	—	`Monotone` `DyckWord` `instPreorder` `Nat.instPreorder` `semilength`	—	`le_refl` `eq_or_ne` `outsidePart_zero` `insidePart_zero` `LE.le.trans` `LT.lt.le` `semilength_insidePart_lt` `semilength_outsidePart_lt`
`nest_denest` 📖	mathematical	`IsNested`	`nest` `denest`	—	`cons_tail_dropLast_concat`
`nest_insidePart_add_outsidePart` 📖	mathematical	—	`DyckWord` `instAddDyckWord` `nest` `insidePart` `outsidePart`	—	`count_take_firstReturn_add_one` `nest_denest`
`nest_ne_zero` 📖	—	—	—	—	—
`numNodes_toTree` 📖	mathematical	—	`Tree.numNodes` `toTree` `semilength`	—	`toTree.eq_1` `semilength_insidePart_add_semilength_outsidePart_add_one` `semilength_insidePart_lt` `semilength_outsidePart_lt`
`ofTree_toTree` 📖	mathematical	—	`ofTree` `toTree`	—	`toTree.eq_1` `semilength_insidePart_lt` `semilength_outsidePart_lt` `nest_insidePart_add_outsidePart`
`outsidePart_add` 📖	mathematical	—	`outsidePart` `DyckWord` `instAddDyckWord`	—	`count_take_firstReturn_add_one` `firstReturn_add` `drop.congr_simp` `Unique.instSubsingleton` `firstReturn_lt_length`
`outsidePart_nest` 📖	mathematical	—	`outsidePart` `nest` `DyckWord` `instZeroDyckWord`	—	`count_take_firstReturn_add_one` `firstReturn_nest` `drop.congr_simp` `ext_iff`
`outsidePart_zero` 📖	mathematical	—	`outsidePart` `DyckWord` `instZeroDyckWord`	—	`count_take_firstReturn_add_one`
`pos_iff_ne_zero` 📖	mathematical	—	`DyckWord` `Preorder.toLT` `instPreorder` `instZeroDyckWord`	—	`ne_iff_lt_iff_le` `zero_le`
`semilength_add` 📖	mathematical	—	`semilength` `DyckWord` `instAddDyckWord`	—	—
`semilength_eq_count_D` 📖	mathematical	—	`semilength` `DyckStep` `instDecidableEqDyckStep` `DyckStep.D` `toList`	—	`count_U_eq_count_D`
`semilength_eq_numNodes_equivTree` 📖	mathematical	—	`Tree.numNodes` `toTree` `semilength`	—	`numNodes_toTree`
`semilength_insidePart_add_semilength_outsidePart_add_one` 📖	mathematical	—	`semilength` `insidePart` `outsidePart`	—	`nest_insidePart_add_outsidePart` `semilength_add` `semilength_nest` `add_right_comm`
`semilength_insidePart_lt` 📖	mathematical	—	`semilength` `insidePart`	—	`semilength_insidePart_add_semilength_outsidePart_add_one`
`semilength_nest` 📖	mathematical	—	`semilength` `nest`	—	`add_zero`
`semilength_outsidePart_lt` 📖	mathematical	—	`semilength` `outsidePart`	—	`semilength_insidePart_add_semilength_outsidePart_add_one`
`semilength_zero` 📖	mathematical	—	`semilength` `DyckWord` `instZeroDyckWord`	—	—
`strictMono_semilength` 📖	mathematical	—	`StrictMono` `DyckWord` `instPreorder` `Nat.instPreorder` `semilength`	—	`lt_iff_le_and_ne` `lt_of_le_of_ne` `monotone_semilength` `Mathlib.Tactic.Contrapose.contrapose₄` `ext` `infix_of_le` `two_mul_semilength_eq_length`
`toList_eq_nil` 📖	mathematical	—	`toList` `DyckStep` `DyckWord` `instZeroDyckWord`	—	`ext_iff`
`toList_ne_nil` 📖	—	—	—	—	`Iff.ne` `toList_eq_nil`
`toTree_ofTree` 📖	mathematical	—	`toTree` `ofTree`	—	`toTree.eq_1` `Unique.instSubsingleton` `insidePart_add` `insidePart_nest` `outsidePart_add` `outsidePart_nest` `zero_add`
`two_mul_semilength_eq_length` 📖	mathematical	—	`semilength` `DyckStep` `toList`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `semilength.eq_1` `count_U_eq_count_D`
`zero_le` 📖	mathematical	—	`DyckWord` `Preorder.toLE` `instPreorder` `instZeroDyckWord`	—	`le_add_self` `add_zero`

DyckWord.IsNested

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nest` 📖	mathematical	—	`DyckWord.IsNested` `DyckWord.nest`	—	`DyckWord.nest_ne_zero` `DyckWord.count_D_le_count_U`

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalDyckWordFirstReturn` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`DyckStep` 📖	CompData	13 math math: `DyckWord.count_U_eq_count_D`, `DyckWord.getLast_eq_D`, `DyckWord.two_mul_semilength_eq_length`, `DyckWord.cons_tail_dropLast_concat`, `DyckWord.head_eq_U`, `DyckWord.count_D_lt_count_U_of_lt_firstReturn`, `DyckWord.toList_eq_nil`, `DyckWord.count_D_le_count_U`, `DyckWord.firstReturn_lt_length`, `DyckWord.firstReturn_nest`, `DyckWord.count_take_firstReturn_add_one`, `DyckWord.semilength_eq_count_D`, `DyckWord.infix_of_le`
`DyckWord` 📖	CompData	22 math math: `DyckWord.insidePart_zero`, `DyckWord.semilength_zero`, `DyckWord.semilength_add`, `DyckWord.nest_insidePart_add_outsidePart`, `DyckWord.pos_iff_ne_zero`, `DyckWord.outsidePart_add`, `DyckWord.toList_eq_nil`, `DyckWord.equivTreesOfNumNodesEq_symm_apply_coe`, `DyckWord.firstReturn_add`, `DyckWord.equivTreesOfNumNodesEq_apply_coe`, `DyckWord.monotone_semilength`, `DyckWord.equivTree_symm_apply`, `DyckWord.firstReturn_zero`, `DyckWord.insidePart_add`, `DyckWord.strictMono_semilength`, `DyckWord.outsidePart_zero`, `DyckWord.outsidePart_nest`, `DyckWord.le_of_suffix`, `DyckWord.card_dyckWord_semilength_eq_catalan`, `DyckWord.zero_le`, `DyckWord.equivTree_apply`, `DyckWord.le_add_self`
`instAddCancelMonoidDyckWord` 📖	CompOp	—
`instAddDyckWord` 📖	CompOp	6 math math: `DyckWord.semilength_add`, `DyckWord.nest_insidePart_add_outsidePart`, `DyckWord.outsidePart_add`, `DyckWord.firstReturn_add`, `DyckWord.insidePart_add`, `DyckWord.le_add_self`
`instCoeDyckWordListDyckStep` 📖	CompOp	—
`instDecidableEqDyckStep` 📖	CompOp	5 math math: `DyckWord.count_U_eq_count_D`, `DyckWord.count_D_lt_count_U_of_lt_firstReturn`, `DyckWord.count_D_le_count_U`, `DyckWord.count_take_firstReturn_add_one`, `DyckWord.semilength_eq_count_D`
`instDecidableEqDyckWord` 📖	CompOp	1 math math: `DyckWord.firstReturn_add`
`instInhabitedDyckStep` 📖	CompOp	—
`instZeroDyckWord` 📖	CompOp	9 math math: `DyckWord.insidePart_zero`, `DyckWord.semilength_zero`, `DyckWord.pos_iff_ne_zero`, `DyckWord.toList_eq_nil`, `DyckWord.firstReturn_add`, `DyckWord.firstReturn_zero`, `DyckWord.outsidePart_zero`, `DyckWord.outsidePart_nest`, `DyckWord.zero_le`

instDecidableEqDyckWord

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

instInhabitedDyckStep

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index