Nuprl - graph_1_3 LEMMAs for adjm_to_adjl

Rank	Theorem	Name
7	Thm* m:AdjMatrix. adjl-graph(adjm_to_adjl(m)) adjm-graph(m)	[adjm_to_adjl_graph]
cites
0	Thm* Bij(T; T; Id)	[identity-biject]
6	Thm* P:(T), l:T List. no_repeats(T;l) no_repeats(T;filter(P;l))	[no_repeats_filter]
3	Thm* i,j:. no_repeats(;upto(i;j))	[no_repeats_upto]
2	Thm* i,j,k:. (k upto(i;j)) ik & k < j	[member_upto]
2	Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x)	[member_filter]