Nuprl - graph_1_2 Citations of rel-graph

Def Graph(x,y:T. R(x;y)) == < vertices = T, edges = {p:(T

T)| R(1of(p);2of(p)) }, incidence = Id >

is mentioned by

Thm* f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) | b:B) Graph(a,a':A. b:B. a' = f(a,b)) [fun-graph-rel-graph]

Thm* R1,R2:(TTProp). (x,y:T. R1(x,y) R2(x,y)) Graph(x,y:T. R1(x,y)) Graph(x,y:T. R2(x,y)) [rel-graph_functionality]

Def DivGraph_1 == Graph(i,j:. i | j) [divides-graph1]

Try larger context: Graphs

graph 1 2 Sections Graphs Doc

`Thm* f:(ABA). (a:A, b1,b2:B. f(a,b1) = f(a,b2) b1 = b2) (a,a':A. Dec(b:B. a' = f(a,b))) Graph(a:A -- > f(a,b) \| b:B) Graph(a,a':A. b:B. a' = f(a,b))`	[fun-graph-rel-graph]
`Thm* R1,R2:(TTProp). (x,y:T. R1(x,y) R2(x,y)) Graph(x,y:T. R1(x,y)) Graph(x,y:T. R2(x,y))`	[rel-graph_functionality]
`Def DivGraph_1 == Graph(i,j:. i \| j)`	[divides-graph1]