graph
1
2
Sections
Graphs
Doc
Def
Inj(A; B; f) ==
a1,a2:A. f(a1) = f(a2)
B
a1 = a2
is mentioned by
Thm*
n,m:
, f:(
n
m). Inj(
n;
m; f)
n
m
[pigeon-hole]
Thm*
n,m:
, f:(
(n-1)
(m-1)). Inj(
(n-1);
(m-1); f)
Inj(
n;
m; f[n-1:=m-1])
[fappend-inject]
In prior sections:
mb
nat
graph
1
1
fun
1
Try larger context:
Graphs
graph
1
2
Sections
Graphs
Doc