Nuprl - graph_1_2 LEMMAs for graph_DASH_isomorphic

Rank	Theorem	Name
3	Thm* G,H:Graph. G H H G	[graph-isomorphic_inversion]
cites
2	Thm* f:(AB). Bij(A; B; f) (g:(BA). Bij(B; A; g) & InvFuns(A; B; f; g))	[inverse-biject]
0	Thm* g:(ABC). (Id,Id) o g = g	[comp2_id_l]
0	Thm* h:(A'A1A2), g1:(A1B), g2:(A2C), f1:(BB'), f2:(CC'). (f1,f2) o (g1,g2) o h = (f1 o g1,f2 o g2) o h	[comp2_comp2_assoc]
0	Thm* f:(AB), g:(BC), h:(CD). h o (g o f) = (h o g) o f AD	[comp_assoc]
1	Thm* f:(AB). f o Id = f	[comp_id_r]