Enumerative combinatorics

DefinitionCatalan numbers#

The recursive definition of the sequence of Catalan numbers: catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i)

catalan : ℕ → ℕ

Sources

• Mathlib documentation: catalan
• Source of catalan in Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean
• Mathlib overview: Combinatorics › Enumerative combinatorics

Mathlibcatalan

Uses 2

Statement usesFinite set · Natural number

DefinitionBell numbers#

Number of partitions of a set of cardinality m.sum whose parts have cardinalities given by m

Multiset.bell (m : Multiset ℕ) : ℕ

Sources

• Mathlib documentation: Multiset.bell
• Source of Multiset.bell in Mathlib/Combinatorics/Enumerative/Bell.lean
• Mathlib overview: Combinatorics › Enumerative combinatorics

MathlibMultiset.bell

Uses 2

Statement usesFinite set · Natural number

StructureDyck words#

A Dyck word is a list of DyckSteps with as many Us as Ds and with every prefix having at least as many Us as Ds.

DyckWord : Type

Sources

• Mathlib documentation: DyckWord
• Source of DyckWord in Mathlib/Combinatorics/Enumerative/DyckWord.lean
• Mathlib overview: Combinatorics › Enumerative combinatorics

MathlibDyckWord

Uses 2

Statement usesList · Natural number

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.