diff --git a/src/elementary-number-theory/bell-numbers.lagda.md b/src/elementary-number-theory/bell-numbers.lagda.md new file mode 100644 index 0000000000..fbe598165f --- /dev/null +++ b/src/elementary-number-theory/bell-numbers.lagda.md @@ -0,0 +1,47 @@ +# The Bell numbers + +```agda +module elementary-number-theory.bell-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.binomial-coefficients +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.strict-inequality-natural-numbers +open import elementary-number-theory.strong-induction-natural-numbers +open import elementary-number-theory.sums-of-natural-numbers +``` + +
+ +## Idea + +The {{#concept "Bell numbers" Agda=bell-number-ℕ}} count the number of ways to partition a set of size $n$. The Bell numbers can be defined recursively by $B_0 := 1$ and + +$$ + B_{n+1} := \sum_{k=0}^{n} \binom{n}{k}B_k. +$$ + +The Bell numbers are listed as sequence A000110 in the [OEIS](literature.oeis.md) {{#cite OEIS}} + +## Definitions + +### The Bell numbers + +```agda +bell-number-ℕ : ℕ → ℕ +bell-number-ℕ = + strong-rec-ℕ 1 + ( λ n B → + bounded-sum-ℕ + ( succ-ℕ n) + ( λ k k