Nuprl - graph_1_2 LEMMAs for trivial_DASH

Rank	Theorem	Name
5	Thm* k:, L: List. k-1- > L^k (i:\|\|L\|\|. L[i] < k)	[trivial-arrows]
cites
0	Thm* k:. increasing(i.i;k)	[id_increasing]
4	Thm* n,m:, f:(nm). Inj(n; m; f) nm	[pigeon-hole]
1	Thm* k,m:, f:(km). increasing(f;k) Inj(k; m; f)	[increasing_inj]
0	Thm* k:, f:(k). increasing(f;k) (x,y:k. x < y f(x) < f(y))	[increasing_implies]
1	Thm* f:(AB), as:A List, n:\|\|as\|\|. map(f;as)[n] = f(as[n])	[map_select]
0	Thm* f:(AB), as:A List. \|\|map(f;as)\|\| = \|\|as\|\|	[map_length]