:: 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 b₁ being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) st
for v, w being Vertex of G1 st v in dom b₁ & w in dom b₁ & v,w are_adjacent holds
b₁ /. v,b₁ /. w are_adjacent

proof end;

end;

:: deftheorem Def1 defines PVertexMapping GLIB_011:def 1 :
for G1, G2 being _Graph
for b₃ being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds
( b₃ is PVertexMapping of G1,G2 iff for v, w being Vertex of G1 st v in dom b₃ & w in dom b₃ & v,w are_adjacent holds
b₃ /. v,b₃ /. 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 b₁ being PVertexMapping of G1,G2 st b₁ is Dcontinuous holds
b₁ is continuous

proof end;

cluster empty -> one-to-one directed continuous Dcontinuous for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is empty holds
( b₁ is one-to-one & b₁ is Dcontinuous & b₁ is directed & b₁ is continuous ) ;

cluster total -> non empty for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is total holds
not b₁ is empty ;

cluster onto -> non empty for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is onto holds
not b₁ 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 b₁ being PVertexMapping of G1,G2 st b₁ is Dcontinuous holds
b₁ 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 b₁ being PVertexMapping of G1,G2 st b₁ is directed & b₁ is continuous holds
b₁ is Dcontinuous

proof end;

end;

registration

let G1 be _trivial _Graph;
let G2 be _Graph;

cluster -> directed for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 holds b₁ is directed

proof end;

cluster continuous -> Dcontinuous for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is continuous holds
b₁ is Dcontinuous

proof end;

cluster non empty -> total for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st not b₁ is empty holds
b₁ 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 b₁ being PVertexMapping of G1,G2 st not b₁ is empty holds
b₁ 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 b₁ being PVertexMapping of G1,G2 holds
( b₁ is Dcontinuous & b₁ 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 b₁ being PVertexMapping of G1,G2 st
( b₁ is empty & b₁ is one-to-one & b₁ is directed & b₁ is continuous & b₁ 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 b₁ being PVertexMapping of G1,G2 st
( not b₁ is empty & b₁ is one-to-one & b₁ 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 b₁ being PVertexMapping of G1,G2 st
( not b₁ is empty & b₁ is one-to-one & b₁ is directed & b₁ is continuous & b₁ 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 b₁ being PVertexMapping of G1,G2 st
( not b₁ is empty & b₁ is one-to-one & b₁ is directed & b₁ is continuous & b₁ 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 b₁ being PVertexMapping of G1,G2 st b₁ is isomorphism holds
( b₁ is total & b₁ is one-to-one & b₁ is onto & b₁ is continuous )

proof end;

cluster Disomorphism -> one-to-one total onto directed continuous Dcontinuous isomorphism for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is Disomorphism holds
( b₁ is total & b₁ is one-to-one & b₁ is onto & b₁ is isomorphism & b₁ is continuous & b₁ is directed & b₁ 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 b₁ being PVertexMapping of G1,G2 st b₁ is total & b₁ is one-to-one & b₁ is onto & b₁ is continuous holds
b₁ 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 b₁ being PVertexMapping of G1,G2 st b₁ is total & b₁ is one-to-one & b₁ is onto & b₁ is directed & b₁ is Dcontinuous holds
b₁ 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 b₁ being PVertexMapping of G,G st
( b₁ is Disomorphism & b₁ 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 b₁ being PVertexMapping of G1,G2 st b₁ is invertible holds
( b₁ is one-to-one & b₁ is continuous ) ;

cluster one-to-one continuous -> invertible for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is one-to-one & b₁ is continuous holds
b₁ is invertible ;

cluster isomorphism -> invertible for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is isomorphism holds
b₁ is invertible ;

cluster Disomorphism -> invertible for PVertexMapping of G1,G2;

coherence
for b₁ being PVertexMapping of G1,G2 st b₁ is Disomorphism holds
b₁ 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 b₁ being PVertexMapping of G1,G2 st
( b₁ is empty & b₁ 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 b₁ being PVertexMapping of G1,G2 st
( not b₁ is empty & b₁ is directed & b₁ 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 b₁ being PVertexMapping of G1,G2 st
( not b₁ is empty & b₁ is directed & b₁ 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 b₁ being PVertexMapping of G2,G1 st b₁ = f " holds
( b₁ is one-to-one & b₁ is continuous & b₁ 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 b₁ being PGraphMapping of G1,G2 st
( b₁ _V = f & dom (b₁ _E) = G1 .edgesBetween (dom f) & rng (b₁ _E) c= G2 .edgesBetween (rng f) )

proof end;

uniqueness
for b₁, b₂ being PGraphMapping of G1,G2 st b₁ _V = f & dom (b₁ _E) = G1 .edgesBetween (dom f) & rng (b₁ _E) c= G2 .edgesBetween (rng f) & b₂ _V = f & dom (b₂ _E) = G1 .edgesBetween (dom f) & rng (b₂ _E) c= G2 .edgesBetween (rng f) holds
b₁ = b₂ 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 b₄ being PGraphMapping of G1,G2 holds
( b₄ = PVM2PGM f iff ( b₄ _V = f & dom (b₄ _E) = G1 .edgesBetween (dom f) & rng (b₄ _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 b₁ being directed PGraphMapping of G1,G2 st
( b₁ _V = f & dom (b₁ _E) = G1 .edgesBetween (dom f) & rng (b₁ _E) c= G2 .edgesBetween (rng f) )

proof end;

uniqueness
for b₁, b₂ being directed PGraphMapping of G1,G2 st b₁ _V = f & dom (b₁ _E) = G1 .edgesBetween (dom f) & rng (b₁ _E) c= G2 .edgesBetween (rng f) & b₂ _V = f & dom (b₂ _E) = G1 .edgesBetween (dom f) & rng (b₂ _E) c= G2 .edgesBetween (rng f) holds
b₁ = b₂ 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 b₄ being directed PGraphMapping of G1,G2 holds
( b₄ = DPVM2PGM f iff ( b₄ _V = f & dom (b₄ _E) = G1 .edgesBetween (dom f) & rng (b₄ _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;