:: About Graph Mappings
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


definition
let G1, G2 be _Graph;
mode PVertexMapping of G1,G2 -> PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) means :Def1: :: GLIB_011:def 1
for v, w being Vertex of G1 st v in dom it & w in dom it & v,w are_adjacent holds
it /. v,it /. w are_adjacent ;
existence
ex b1 being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) st
for v, w being Vertex of G1 st v in dom b1 & w in dom b1 & v,w are_adjacent holds
b1 /. v,b1 /. w are_adjacent
proof end;
end;

:: deftheorem Def1 defines PVertexMapping GLIB_011:def 1 :
for G1, G2 being _Graph
for b3 being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( b3 is PVertexMapping of G1,G2 iff for v, w being Vertex of G1 st v in dom b3 & w in dom b3 & v,w are_adjacent holds
b3 /. v,b3 /. w are_adjacent );

theorem Th1: :: GLIB_011:1
for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e Joins v,w,G1 holds
ex e9 being object st e9 Joins f . v,f . w,G2 )
proof end;

definition
let G1, G2 be _Graph;
let f be PVertexMapping of G1,G2;
attr f is directed means :Def2: :: GLIB_011:def 2
for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2;
attr f is continuous means :: GLIB_011:def 3
for v, w being Vertex of G1 st v in dom f & w in dom f & f /. v,f /. w are_adjacent holds
v,w are_adjacent ;
attr f is Dcontinuous means :Def4: :: GLIB_011:def 4
for v, w, e9 being object st v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 holds
ex e being object st e DJoins v,w,G1;
end;

:: deftheorem Def2 defines directed GLIB_011:def 2 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is directed iff for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 );

:: deftheorem defines continuous GLIB_011:def 3 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is continuous iff for v, w being Vertex of G1 st v in dom f & w in dom f & f /. v,f /. w are_adjacent holds
v,w are_adjacent );

:: deftheorem Def4 defines Dcontinuous GLIB_011:def 4 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is Dcontinuous iff for v, w, e9 being object st v in dom f & w in dom f & e9 DJoins f . v,f . w,G2 holds
ex e being object st e DJoins v,w,G1 );

theorem Th2: :: GLIB_011:2
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is continuous iff for v, w, e9 being object st v in dom f & w in dom f & e9 Joins f . v,f . w,G2 holds
ex e being object st e Joins v,w,G1 )
proof end;

theorem :: GLIB_011:3
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is continuous iff for v, w being Vertex of G1 st v in dom f & w in dom f holds
( v,w are_adjacent iff f /. v,f /. w are_adjacent ) ) by Def1;

registration
let G1, G2 be _Graph;
cluster Dcontinuous -> continuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is Dcontinuous holds
b1 is continuous
proof end;
cluster empty -> one-to-one directed continuous Dcontinuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is empty holds
( b1 is one-to-one & b1 is Dcontinuous & b1 is directed & b1 is continuous )
;
cluster total -> non empty for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is total holds
not b1 is empty
;
cluster onto -> non empty for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is onto holds
not b1 is empty
proof end;
end;

registration
let G1 be simple _Graph;
let G2 be _Graph;
cluster Dcontinuous -> directed for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is Dcontinuous holds
b1 is directed
proof end;
end;

registration
let G1 be _Graph;
let G2 be simple _Graph;
cluster directed continuous -> Dcontinuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is directed & b1 is continuous holds
b1 is Dcontinuous
proof end;
end;

registration
let G1 be _trivial _Graph;
let G2 be _Graph;
cluster -> directed for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 holds b1 is directed
proof end;
cluster continuous -> Dcontinuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is continuous holds
b1 is Dcontinuous
proof end;
cluster non empty -> total for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st not b1 is empty holds
b1 is total
proof end;
end;

registration
let G1 be _Graph;
let G2 be _trivial _Graph;
cluster non empty -> onto for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st not b1 is empty holds
b1 is onto
proof end;
end;

registration
let G1 be _Graph;
let G2 be loopless _trivial _Graph;
cluster -> continuous Dcontinuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 holds
( b1 is Dcontinuous & b1 is continuous )
proof end;
end;

registration
let G1, G2 be _Graph;
cluster empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like one-to-one directed continuous Dcontinuous for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( b1 is empty & b1 is one-to-one & b1 is directed & b1 is continuous & b1 is Dcontinuous )
proof end;
end;

theorem :: GLIB_011:4
for G1, G2 being _Graph
for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( f is directed PVertexMapping of G1,G2 iff for v, w, e being object st v in dom f & w in dom f & e DJoins v,w,G1 holds
ex e9 being object st e9 DJoins f . v,f . w,G2 )
proof end;

registration
let G1 be loopless _Graph;
let G2 be _Graph;
cluster non empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like one-to-one directed for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( not b1 is empty & b1 is one-to-one & b1 is directed )
proof end;
end;

registration
let G1, G2 be loopless _Graph;
cluster non empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like one-to-one directed continuous Dcontinuous for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( not b1 is empty & b1 is one-to-one & b1 is directed & b1 is continuous & b1 is Dcontinuous )
proof end;
end;

registration
let G1, G2 be non loopless _Graph;
cluster non empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like one-to-one directed continuous Dcontinuous for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( not b1 is empty & b1 is one-to-one & b1 is directed & b1 is continuous & b1 is Dcontinuous )
proof end;
end;

theorem Th5: :: GLIB_011:5
for G being _Graph holds id (the_Vertices_of G) is directed continuous Dcontinuous PVertexMapping of G,G
proof end;

theorem :: GLIB_011:6
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 st f is total holds
( ( G2 is loopless implies G1 is loopless ) & ( G2 is edgeless implies G1 is edgeless ) )
proof end;

theorem :: GLIB_011:7
for G1, G2 being _Graph
for f being continuous PVertexMapping of G1,G2 st f is onto holds
( ( G1 is loopless implies G2 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) )
proof end;

definition
let G1, G2 be _Graph;
let f be PVertexMapping of G1,G2;
attr f is isomorphism means :: GLIB_011:def 5
( f is total & f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ) );
attr f is Disomorphism means :: GLIB_011:def 6
( f is total & f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ) ) );
end;

:: deftheorem defines isomorphism GLIB_011:def 5 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is isomorphism iff ( f is total & f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ) ) );

:: deftheorem defines Disomorphism GLIB_011:def 6 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is Disomorphism iff ( f is total & f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ) ) ) );

registration
let G1, G2 be _Graph;
cluster isomorphism -> one-to-one total onto continuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is isomorphism holds
( b1 is total & b1 is one-to-one & b1 is onto & b1 is continuous )
proof end;
cluster Disomorphism -> one-to-one total onto directed continuous Dcontinuous isomorphism for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is Disomorphism holds
( b1 is total & b1 is one-to-one & b1 is onto & b1 is isomorphism & b1 is continuous & b1 is directed & b1 is Dcontinuous )
proof end;
end;

theorem Th8: :: GLIB_011:8
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is continuous holds
for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
proof end;

definition
let G1, G2 be non-multi _Graph;
let f be PVertexMapping of G1,G2;
redefine attr f is isomorphism means :: GLIB_011:def 7
( f is total & f is one-to-one & f is onto & f is continuous );
compatibility
( f is isomorphism iff ( f is total & f is one-to-one & f is onto & f is continuous ) )
by Th8;
end;

:: deftheorem defines isomorphism GLIB_011:def 7 :
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 holds
( f is isomorphism iff ( f is total & f is one-to-one & f is onto & f is continuous ) );

registration
let G1, G2 be non-multi _Graph;
cluster one-to-one total onto continuous -> isomorphism for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is total & b1 is one-to-one & b1 is onto & b1 is continuous holds
b1 is isomorphism
;
end;

theorem Th9: :: GLIB_011:9
for G1, G2 being non-Dmulti _Graph
for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is directed & f is Dcontinuous holds
for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) )
proof end;

definition
let G1, G2 be non-Dmulti _Graph;
let f be PVertexMapping of G1,G2;
redefine attr f is Disomorphism means :: GLIB_011:def 8
( f is total & f is one-to-one & f is onto & f is directed & f is Dcontinuous );
compatibility
( f is Disomorphism iff ( f is total & f is one-to-one & f is onto & f is directed & f is Dcontinuous ) )
by Th9;
end;

:: deftheorem defines Disomorphism GLIB_011:def 8 :
for G1, G2 being non-Dmulti _Graph
for f being PVertexMapping of G1,G2 holds
( f is Disomorphism iff ( f is total & f is one-to-one & f is onto & f is directed & f is Dcontinuous ) );

registration
let G1, G2 be non-Dmulti _Graph;
cluster one-to-one total onto directed Dcontinuous -> Disomorphism for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is total & b1 is one-to-one & b1 is onto & b1 is directed & b1 is Dcontinuous holds
b1 is Disomorphism
;
end;

registration
let G be _Graph;
cluster Relation-like the_Vertices_of G -defined the_Vertices_of G -valued Function-like isomorphism Disomorphism for PVertexMapping of G,G;
existence
ex b1 being PVertexMapping of G,G st
( b1 is Disomorphism & b1 is isomorphism )
proof end;
end;

theorem :: GLIB_011:10
for G being _Graph holds id (the_Vertices_of G) is isomorphism Disomorphism PVertexMapping of G,G
proof end;

definition
let G1, G2 be _Graph;
let f be PVertexMapping of G1,G2;
attr f is invertible means :: GLIB_011:def 9
( f is one-to-one & f is continuous );
end;

:: deftheorem defines invertible GLIB_011:def 9 :
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2 holds
( f is invertible iff ( f is one-to-one & f is continuous ) );

registration
let G1, G2 be _Graph;
cluster invertible -> one-to-one continuous for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is invertible holds
( b1 is one-to-one & b1 is continuous )
;
cluster one-to-one continuous -> invertible for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is one-to-one & b1 is continuous holds
b1 is invertible
;
cluster isomorphism -> invertible for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is isomorphism holds
b1 is invertible
;
cluster Disomorphism -> invertible for PVertexMapping of G1,G2;
coherence
for b1 being PVertexMapping of G1,G2 st b1 is Disomorphism holds
b1 is invertible
;
cluster empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like invertible for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( b1 is empty & b1 is invertible )
proof end;
end;

registration
let G1, G2 be loopless _Graph;
cluster non empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like directed invertible for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( not b1 is empty & b1 is directed & b1 is invertible )
proof end;
end;

registration
let G1, G2 be non loopless _Graph;
cluster non empty Relation-like the_Vertices_of G1 -defined the_Vertices_of G2 -valued Function-like directed invertible for PVertexMapping of G1,G2;
existence
ex b1 being PVertexMapping of G1,G2 st
( not b1 is empty & b1 is directed & b1 is invertible )
proof end;
end;

definition
let G1, G2 be _Graph;
let f be invertible PVertexMapping of G1,G2;
:: original: "
redefine func f " -> PVertexMapping of G2,G1;
coherence
f " is PVertexMapping of G2,G1
proof end;
end;

registration
let G1, G2 be _Graph;
let f be invertible PVertexMapping of G1,G2;
cluster f " -> one-to-one continuous invertible for PVertexMapping of G2,G1;
coherence
for b1 being PVertexMapping of G2,G1 st b1 = f " holds
( b1 is one-to-one & b1 is continuous & b1 is invertible )
proof end;
end;

definition
let G1, G2, G3 be _Graph;
let f be PVertexMapping of G1,G2;
let g be PVertexMapping of G2,G3;
:: original: *
redefine func g * f -> PVertexMapping of G1,G3;
coherence
f * g is PVertexMapping of G1,G3
proof end;
end;

theorem :: GLIB_011:11
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is continuous & g is continuous holds
g * f is continuous
proof end;

theorem :: GLIB_011:12
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is directed & g is directed holds
g * f is directed
proof end;

theorem :: GLIB_011:13
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is Dcontinuous & g is Dcontinuous holds
g * f is Dcontinuous
proof end;

theorem :: GLIB_011:14
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is isomorphism & g is isomorphism holds
g * f is isomorphism
proof end;

theorem :: GLIB_011:15
for G1, G2, G3 being _Graph
for f being PVertexMapping of G1,G2
for g being PVertexMapping of G2,G3 st f is Disomorphism & g is Disomorphism holds
g * f is Disomorphism
proof end;

theorem Th16: :: GLIB_011:16
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st ( for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & v,w are_adjacent holds
ex e being object st
( e in dom (F _E) & e Joins v,w,G1 ) ) holds
F _V is PVertexMapping of G1,G2
proof end;

theorem Th17: :: GLIB_011:17
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st dom (F _E) = the_Edges_of G1 holds
F _V is PVertexMapping of G1,G2
proof end;

theorem Th18: :: GLIB_011:18
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total holds
F _V is PVertexMapping of G1,G2
proof end;

theorem Th19: :: GLIB_011:19
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2 st ( for v, w being object st v in dom (F _V) & w in dom (F _V) & ex e being object st e DJoins v,w,G1 holds
ex e being object st
( e in dom (F _E) & e DJoins v,w,G1 ) ) holds
F _V is directed PVertexMapping of G1,G2
proof end;

theorem Th20: :: GLIB_011:20
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2 st dom (F _E) = the_Edges_of G1 holds
F _V is directed PVertexMapping of G1,G2
proof end;

theorem Th21: :: GLIB_011:21
for G1, G2 being _Graph
for F being directed PGraphMapping of G1,G2 st F is total holds
F _V is directed PVertexMapping of G1,G2
proof end;

theorem Th22: :: GLIB_011:22
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st F _V is PVertexMapping of G1,G2 & ( for v, w being Vertex of G1 st v in dom (F _V) & w in dom (F _V) & (F _V) /. v,(F _V) /. w are_adjacent holds
ex e9 being object st
( e9 in rng (F _E) & e9 Joins (F _V) . v,(F _V) . w,G2 ) ) holds
F _V is continuous PVertexMapping of G1,G2
proof end;

theorem Th23: :: GLIB_011:23
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st dom (F _E) = the_Edges_of G1 & rng (F _E) = the_Edges_of G2 holds
F _V is continuous PVertexMapping of G1,G2
proof end;

theorem :: GLIB_011:24
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1,G2 st F is total & F is onto holds
F _V is continuous PVertexMapping of G1,G2
proof end;

Lm1: for x being object
for f being Function st x in dom f holds
f .: {x} = {(f . x)}

proof end;

theorem Th25: :: GLIB_011:25
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
ex f being PVertexMapping of G1,G2 st
( F _V = f & f is isomorphism )
proof end;

theorem Th26: :: GLIB_011:26
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism holds
ex f being directed PVertexMapping of G1,G2 st
( F _V = f & f is Disomorphism )
proof end;

:: Maybe add that f is continuous implies rng F_E = E2 /\ ... ?
:: An example why this isn't always the case is the embedding of P_3 into K_3
theorem Th27: :: GLIB_011:27
for G1, G2 being _Graph
for f being PVertexMapping of G1,G2
for E1 being RepEdgeSelection of G1
for E2 being RepEdgeSelection of G2 ex F being PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
proof end;

definition
let G1, G2 be non-multi _Graph;
let f be PVertexMapping of G1,G2;
func PVM2PGM f -> PGraphMapping of G1,G2 means :Def10: :: GLIB_011:def 10
( it _V = f & dom (it _E) = G1 .edgesBetween (dom f) & rng (it _E) c= G2 .edgesBetween (rng f) );
existence
ex b1 being PGraphMapping of G1,G2 st
( b1 _V = f & dom (b1 _E) = G1 .edgesBetween (dom f) & rng (b1 _E) c= G2 .edgesBetween (rng f) )
proof end;
uniqueness
for b1, b2 being PGraphMapping of G1,G2 st b1 _V = f & dom (b1 _E) = G1 .edgesBetween (dom f) & rng (b1 _E) c= G2 .edgesBetween (rng f) & b2 _V = f & dom (b2 _E) = G1 .edgesBetween (dom f) & rng (b2 _E) c= G2 .edgesBetween (rng f) holds
b1 = b2
by GLIB_010:40;
end;

:: deftheorem Def10 defines PVM2PGM GLIB_011:def 10 :
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2
for b4 being PGraphMapping of G1,G2 holds
( b4 = PVM2PGM f iff ( b4 _V = f & dom (b4 _E) = G1 .edgesBetween (dom f) & rng (b4 _E) c= G2 .edgesBetween (rng f) ) );

theorem Th28: :: GLIB_011:28
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 holds (PVM2PGM f) _V = f by Def10;

registration
let G1, G2 be non-multi _Graph;
let f be PVertexMapping of G1,G2;
reduce (PVM2PGM f) _V to f;
reducibility
(PVM2PGM f) _V = f
by Th28;
end;

:: as above
theorem Th29: :: GLIB_011:29
for G1, G2 being _Graph
for f being directed PVertexMapping of G1,G2
for E1 being RepDEdgeSelection of G1
for E2 being RepDEdgeSelection of G2 ex F being directed PGraphMapping of G1,G2 st
( F _V = f & dom (F _E) = E1 /\ (G1 .edgesBetween (dom f)) & rng (F _E) c= E2 /\ (G2 .edgesBetween (rng f)) )
proof end;

definition
let G1, G2 be non-Dmulti _Graph;
let f be directed PVertexMapping of G1,G2;
func DPVM2PGM f -> directed PGraphMapping of G1,G2 means :Def11: :: GLIB_011:def 11
( it _V = f & dom (it _E) = G1 .edgesBetween (dom f) & rng (it _E) c= G2 .edgesBetween (rng f) );
existence
ex b1 being directed PGraphMapping of G1,G2 st
( b1 _V = f & dom (b1 _E) = G1 .edgesBetween (dom f) & rng (b1 _E) c= G2 .edgesBetween (rng f) )
proof end;
uniqueness
for b1, b2 being directed PGraphMapping of G1,G2 st b1 _V = f & dom (b1 _E) = G1 .edgesBetween (dom f) & rng (b1 _E) c= G2 .edgesBetween (rng f) & b2 _V = f & dom (b2 _E) = G1 .edgesBetween (dom f) & rng (b2 _E) c= G2 .edgesBetween (rng f) holds
b1 = b2
by GLIB_010:41;
end;

:: deftheorem Def11 defines DPVM2PGM GLIB_011:def 11 :
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2
for b4 being directed PGraphMapping of G1,G2 holds
( b4 = DPVM2PGM f iff ( b4 _V = f & dom (b4 _E) = G1 .edgesBetween (dom f) & rng (b4 _E) c= G2 .edgesBetween (rng f) ) );

theorem Th30: :: GLIB_011:30
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 holds (DPVM2PGM f) _V = f by Def11;

registration
let G1, G2 be non-Dmulti _Graph;
let f be directed PVertexMapping of G1,G2;
reduce (DPVM2PGM f) _V to f;
reducibility
(DPVM2PGM f) _V = f
by Th30;
end;

theorem :: GLIB_011:31
for G1, G2 being non-multi _Graph
for f being directed PVertexMapping of G1,G2 holds PVM2PGM f = DPVM2PGM f
proof end;

theorem Th32: :: GLIB_011:32
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is total holds
PVM2PGM f is total
proof end;

theorem Th33: :: GLIB_011:33
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is total holds
DPVM2PGM f is total
proof end;

theorem Th34: :: GLIB_011:34
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is one-to-one holds
PVM2PGM f is one-to-one
proof end;

theorem Th35: :: GLIB_011:35
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is one-to-one holds
DPVM2PGM f is one-to-one
proof end;

theorem Th36: :: GLIB_011:36
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is onto & f is continuous holds
PVM2PGM f is onto
proof end;

theorem Th37: :: GLIB_011:37
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is onto & f is Dcontinuous holds
DPVM2PGM f is onto
proof end;

theorem :: GLIB_011:38
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is continuous & f is one-to-one holds
PVM2PGM f is semi-continuous
proof end;

theorem Th39: :: GLIB_011:39
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is continuous holds
PVM2PGM f is continuous
proof end;

theorem :: GLIB_011:40
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is one-to-one holds
( DPVM2PGM f is semi-Dcontinuous & DPVM2PGM f is semi-continuous )
proof end;

theorem Th41: :: GLIB_011:41
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is Dcontinuous holds
DPVM2PGM f is Dcontinuous
proof end;

theorem :: GLIB_011:42
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is one-to-one holds
PVM2PGM f is one-to-one by Th34;

theorem :: GLIB_011:43
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is one-to-one holds
DPVM2PGM f is one-to-one by Th35;

theorem :: GLIB_011:44
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is total & f is one-to-one holds
PVM2PGM f is weak_SG-embedding
proof end;

theorem :: GLIB_011:45
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is total & f is one-to-one holds
DPVM2PGM f is weak_SG-embedding
proof end;

theorem :: GLIB_011:46
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is continuous holds
PVM2PGM f is strong_SG-embedding
proof end;

theorem Th47: :: GLIB_011:47
for G1, G2 being non-multi _Graph
for f being PVertexMapping of G1,G2 st f is isomorphism holds
PVM2PGM f is isomorphism
proof end;

theorem Th48: :: GLIB_011:48
for G1, G2 being non-Dmulti _Graph
for f being directed PVertexMapping of G1,G2 st f is Disomorphism holds
DPVM2PGM f is Disomorphism
proof end;

theorem :: GLIB_011:49
for G1, G2 being non-multi _Graph holds
( G2 is G1 -isomorphic iff ex f being PVertexMapping of G1,G2 st f is isomorphism )
proof end;

theorem :: GLIB_011:50
for G1, G2 being non-Dmulti _Graph holds
( G2 is G1 -Disomorphic iff ex f being directed PVertexMapping of G1,G2 st f is Disomorphism )
proof end;