Nuprl - graph_1_2 Citations of graph-isomorphic

graph 1 2 Sections Graphs Doc

Def G

H ==

vmap:(Vertices(G)

Vertices(H)), emap:(Edges(G)

Edges(H)). Bij(Vertices(G); Vertices(H); vmap) & Bij(Edges(G); Edges(H); emap) & (vmap,vmap) o Incidence(G) = Incidence(H) o emap

is mentioned by

Thm* DivGraph_2 DivGraph_1 [div-graph-iso]

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]

Thm* EquivRel G,H:Graph. G H [graph-isomorphic-equiv]

Thm* G,H:Graph. G H H G [graph-isomorphic_inversion]

Thm* G,H,K:Graph. G H H K G K [graph-isomorphic_transitivity]

Thm* G,H:Graph. G = H G H [graph-isomorphic_weakening]

Try larger context: Graphs

graph 1 2 Sections Graphs Doc

`Thm* DivGraph_2 DivGraph_1`	[div-graph-iso]
`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]
`Thm* EquivRel G,H:Graph. G H`	[graph-isomorphic-equiv]
`Thm* G,H:Graph. G H H G`	[graph-isomorphic_inversion]
`Thm* G,H,K:Graph. G H H K G K`	[graph-isomorphic_transitivity]
`Thm* G,H:Graph. G = H G H`	[graph-isomorphic_weakening]