Nuprl - Proof: graph-isomorphic transitivity 1

(4steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

1. G: Graph
2. H: Graph
3. K: Graph
4. v1: Vertices(G)Vertices(H)
5. e1: Edges(G)Edges(H)
6. Bij(Vertices(G); Vertices(H); v1)
7. Bij(Edges(G); Edges(H); e1)
8. (v1,v1) o Incidence(G) = Incidence(H) o e1
9. vmap: Vertices(H)Vertices(K)
10. emap: Edges(H)Edges(K)
11. Bij(Vertices(H); Vertices(K); vmap)
12. Bij(Edges(H); Edges(K); emap)
13. (vmap,vmap) o Incidence(H) = Incidence(K) o emap

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

By: InstConcl [vmap o v1;emap o e1]

Generated subgoal:

1 Bij(Vertices(G); Vertices(K); vmap o v1) & Bij(Edges(G); Edges(K); emap o e1) & (vmap o v1,vmap o v1) o Incidence(G) = Incidence(K) o emap o e1 2 steps

About:

(4steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc