The Bell numbers

src/elementary-number-theory.lagda.md

@@ -24,6 +24,7 @@ open import elementary-number-theory.archimedean-property-rational-numbers publi
 open import elementary-number-theory.arithmetic-functions public
 open import elementary-number-theory.based-induction-natural-numbers public
 open import elementary-number-theory.based-strong-induction-natural-numbers public
+open import elementary-number-theory.bell-numbers public
 open import elementary-number-theory.bezouts-lemma-integers public
 open import elementary-number-theory.bezouts-lemma-natural-numbers public
 open import elementary-number-theory.binomial-coefficients public

src/elementary-number-theory/bell-numbers.lagda.md

@@ -0,0 +1,50 @@
+# The Bell numbers
+
+```agda
+module elementary-number-theory.bell-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## Idea
+
+The {{#concept "Bell numbers" Agda=bell-number-ℕ WDID=Q816063 WD="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 H →
+          binomial-coefficient-ℕ n k *ℕ B k (leq-le-succ-ℕ k n H)))
+```
+
+## References
+
+{{#bibliography}}

src/literature/oeis.lagda.md

@@ -105,6 +105,13 @@ open import elementary-number-theory.catalan-numbers using
   ( catalan-numbers)
 ```
 
+### [A000110](https://oeis.org/A000110) The Bell numbers
+
+```agda
+open import elementary-number-theory.bell-numbers using
+  ( bell-number-ℕ)
+```
+
 ### [A000142](https://oeis.org/A000142) Factorials
 
 ```agda