m,k:
, f:(m
k). k<m 
(
x,y:m. x 
y & f(x) = f(y))m:, f:(m
). 
Inj(m; ; f) (x:m, y:x. f(x) = f(y))f:(mk). Inj(m; k; f)) m
k| Rank | Theorem | Name |
| 3 | m,k:, f:(mk). k<m (x,y:m. x y & f(x) = f(y)) | [pigeon_hole] |
| cites the following: | ||
| 0 | m:, f:(m). Inj(m; ; f) (x:m, y:x. f(x) = f(y)) | [finite_inj_counter_example] |
| 2 | f:(mk). Inj(m; k; f)) mk | [inj_imp_le] |