Definition 1.8.1.43.  Let m, n ∈ . We define:
min(m, n) := min({m, n}) = {m if m ≤ nn if m > n = {0 if n = 0({0 if m = 0min(x, y) + 1 if m = x + 1 (x ∈ )) if n = y + 1 (y ∈ )
Equality.  No proof.
References.