e:Type(e
vv)Top
Type{i'}
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| Some definitions of interest. | |
| graph | Def Graph == v:Typee:Type(evv)Top |
| Thm* Graph Type{i'} | |
| graph-isomorphic | 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 |
About:
 |  |  |  |  |  |  |  |  |  |