:: by Sebastian Koch

::

:: Received August 29, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

definition

let G1, G2 be _Graph;

ex b_{1} being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) st

for v, w being Vertex of G1 st v in dom b_{1} & w in dom b_{1} & v,w are_adjacent holds

b_{1} /. v,b_{1} /. w are_adjacent

end;
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 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 ;

ex b

for v, w being Vertex of G1 st v in dom b

b

proof end;

:: deftheorem Def1 defines PVertexMapping GLIB_011:def 1 :

for G1, G2 being _Graph

for b_{3} being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) holds

( b_{3} is PVertexMapping of G1,G2 iff for v, w being Vertex of G1 st v in dom b_{3} & w in dom b_{3} & v,w are_adjacent holds

b_{3} /. v,b_{3} /. w are_adjacent );

for G1, G2 being _Graph

for b

( b

b

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 )

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;

end;
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;

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 ;

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 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 );

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 );

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 );

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 )

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;

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;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is Dcontinuous holds

b_{1} is continuous

for b_{1} being PVertexMapping of G1,G2 st b_{1} is empty holds

( b_{1} is one-to-one & b_{1} is Dcontinuous & b_{1} is directed & b_{1} is continuous )
;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is total holds

not b_{1} is empty
;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is onto holds

not b_{1} is empty

end;
coherence

for b

b

proof end;

coherence for b

( b

coherence

for b

not b

coherence

for b

not b

proof end;

registration

let G1 be simple _Graph;

let G2 be _Graph;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is Dcontinuous holds

b_{1} is directed

end;
let G2 be _Graph;

coherence

for b

b

proof end;

registration

let G1 be _Graph;

let G2 be simple _Graph;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is directed & b_{1} is continuous holds

b_{1} is Dcontinuous

end;
let G2 be simple _Graph;

coherence

for b

b

proof end;

registration

let G1 be _trivial _Graph;

let G2 be _Graph;

coherence

for b_{1} being PVertexMapping of G1,G2 holds b_{1} is directed

for b_{1} being PVertexMapping of G1,G2 st b_{1} is continuous holds

b_{1} is Dcontinuous

for b_{1} being PVertexMapping of G1,G2 st not b_{1} is empty holds

b_{1} is total

end;
let G2 be _Graph;

coherence

for b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration

let G1 be _Graph;

let G2 be _trivial _Graph;

coherence

for b_{1} being PVertexMapping of G1,G2 st not b_{1} is empty holds

b_{1} is onto

end;
let G2 be _trivial _Graph;

coherence

for b

b

proof end;

registration

let G1 be _Graph;

let G2 be loopless _trivial _Graph;

coherence

for b_{1} being PVertexMapping of G1,G2 holds

( b_{1} is Dcontinuous & b_{1} is continuous )

end;
let G2 be loopless _trivial _Graph;

coherence

for b

( b

proof end;

registration

let G1, G2 be _Graph;

ex b_{1} being PVertexMapping of G1,G2 st

( b_{1} is empty & b_{1} is one-to-one & b_{1} is directed & b_{1} is continuous & b_{1} is Dcontinuous )

end;
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

( b

proof 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 )

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;

ex b_{1} being PVertexMapping of G1,G2 st

( not b_{1} is empty & b_{1} is one-to-one & b_{1} is directed )

end;
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

( not b

proof end;

registration

let G1, G2 be loopless _Graph;

ex b_{1} being PVertexMapping of G1,G2 st

( not b_{1} is empty & b_{1} is one-to-one & b_{1} is directed & b_{1} is continuous & b_{1} is Dcontinuous )

end;
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

( not b

proof end;

registration

let G1, G2 be non loopless _Graph;

ex b_{1} being PVertexMapping of G1,G2 st

( not b_{1} is empty & b_{1} is one-to-one & b_{1} is directed & b_{1} is continuous & b_{1} is Dcontinuous )

end;
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

( not b

proof 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 ) )

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 ) )

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;

end;
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)})) ) );

( 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)})) ) ) );

( 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)})) ) ) );

:: 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)})) ) ) );

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)})) ) ) ) );

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;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is isomorphism holds

( b_{1} is total & b_{1} is one-to-one & b_{1} is onto & b_{1} is continuous )

for b_{1} being PVertexMapping of G1,G2 st b_{1} is Disomorphism holds

( b_{1} is total & b_{1} is one-to-one & b_{1} is onto & b_{1} is isomorphism & b_{1} is continuous & b_{1} is directed & b_{1} is Dcontinuous )

end;
coherence

for b

( b

proof end;

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

coherence for b

( b

proof 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)}))

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;

( f is isomorphism iff ( f is total & f is one-to-one & f is onto & f is continuous ) ) by Th8;

end;
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 total & f is one-to-one & f is onto & f is continuous );

( f is isomorphism iff ( f is total & f is one-to-one & f is onto & f is continuous ) ) by Th8;

:: 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 ) );

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;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is total & b_{1} is one-to-one & b_{1} is onto & b_{1} is continuous holds

b_{1} is isomorphism
;

end;
coherence

for b

b

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)})) )

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;

( f is Disomorphism iff ( f is total & f is one-to-one & f is onto & f is directed & f is Dcontinuous ) ) by Th9;

end;
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 total & f is one-to-one & f is onto & f is directed & f is Dcontinuous );

( f is Disomorphism iff ( f is total & f is one-to-one & f is onto & f is directed & f is Dcontinuous ) ) by Th9;

:: 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 ) );

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;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is total & b_{1} is one-to-one & b_{1} is onto & b_{1} is directed & b_{1} is Dcontinuous holds

b_{1} is Disomorphism
;

end;
coherence

for b

b

registration

let G be _Graph;

ex b_{1} being PVertexMapping of G,G st

( b_{1} is Disomorphism & b_{1} is isomorphism )

end;
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

( b

proof 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 ) );

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;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is invertible holds

( b_{1} is one-to-one & b_{1} is continuous )
;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is one-to-one & b_{1} is continuous holds

b_{1} is invertible
;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is isomorphism holds

b_{1} is invertible
;

coherence

for b_{1} being PVertexMapping of G1,G2 st b_{1} is Disomorphism holds

b_{1} is invertible
;

ex b_{1} being PVertexMapping of G1,G2 st

( b_{1} is empty & b_{1} is invertible )

end;
coherence

for b

( b

coherence

for b

b

coherence

for b

b

coherence

for b

b

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

( b

proof end;

registration

let G1, G2 be loopless _Graph;

ex b_{1} being PVertexMapping of G1,G2 st

( not b_{1} is empty & b_{1} is directed & b_{1} is invertible )

end;
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

( not b

proof end;

registration

let G1, G2 be non loopless _Graph;

ex b_{1} being PVertexMapping of G1,G2 st

( not b_{1} is empty & b_{1} is directed & b_{1} is invertible )

end;
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

( not b

proof 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

end;
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;

registration

let G1, G2 be _Graph;

let f be invertible PVertexMapping of G1,G2;

coherence

for b_{1} being PVertexMapping of G2,G1 st b_{1} = f " holds

( b_{1} is one-to-one & b_{1} is continuous & b_{1} is invertible )

end;
let f be invertible PVertexMapping of G1,G2;

coherence

for b

( b

proof 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

end;
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;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 )

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 )

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;

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)) )

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;

ex b_{1} being PGraphMapping of G1,G2 st

( b_{1} _V = f & dom (b_{1} _E) = G1 .edgesBetween (dom f) & rng (b_{1} _E) c= G2 .edgesBetween (rng f) )

for b_{1}, b_{2} being PGraphMapping of G1,G2 st b_{1} _V = f & dom (b_{1} _E) = G1 .edgesBetween (dom f) & rng (b_{1} _E) c= G2 .edgesBetween (rng f) & b_{2} _V = f & dom (b_{2} _E) = G1 .edgesBetween (dom f) & rng (b_{2} _E) c= G2 .edgesBetween (rng f) holds

b_{1} = b_{2}
by GLIB_010:40;

end;
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 ( it _V = f & dom (it _E) = G1 .edgesBetween (dom f) & rng (it _E) c= G2 .edgesBetween (rng f) );

ex b

( b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines PVM2PGM GLIB_011:def 10 :

for G1, G2 being non-multi _Graph

for f being PVertexMapping of G1,G2

for b_{4} being PGraphMapping of G1,G2 holds

( b_{4} = PVM2PGM f iff ( b_{4} _V = f & dom (b_{4} _E) = G1 .edgesBetween (dom f) & rng (b_{4} _E) c= G2 .edgesBetween (rng f) ) );

for G1, G2 being non-multi _Graph

for f being PVertexMapping of G1,G2

for b

( b

registration

let G1, G2 be non-multi _Graph;

let f be PVertexMapping of G1,G2;

reducibility

(PVM2PGM f) _V = f by Th28;

end;
let f be PVertexMapping of G1,G2;

reducibility

(PVM2PGM f) _V = f by Th28;

:: 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)) )

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;

ex b_{1} being directed PGraphMapping of G1,G2 st

( b_{1} _V = f & dom (b_{1} _E) = G1 .edgesBetween (dom f) & rng (b_{1} _E) c= G2 .edgesBetween (rng f) )

for b_{1}, b_{2} being directed PGraphMapping of G1,G2 st b_{1} _V = f & dom (b_{1} _E) = G1 .edgesBetween (dom f) & rng (b_{1} _E) c= G2 .edgesBetween (rng f) & b_{2} _V = f & dom (b_{2} _E) = G1 .edgesBetween (dom f) & rng (b_{2} _E) c= G2 .edgesBetween (rng f) holds

b_{1} = b_{2}
by GLIB_010:41;

end;
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 ( it _V = f & dom (it _E) = G1 .edgesBetween (dom f) & rng (it _E) c= G2 .edgesBetween (rng f) );

ex b

( b

proof end;

uniqueness for b

b

:: 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_{4} being directed PGraphMapping of G1,G2 holds

( b_{4} = DPVM2PGM f iff ( b_{4} _V = f & dom (b_{4} _E) = G1 .edgesBetween (dom f) & rng (b_{4} _E) c= G2 .edgesBetween (rng f) ) );

for G1, G2 being non-Dmulti _Graph

for f being directed PVertexMapping of G1,G2

for b

( b

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;

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;

reducibility

(DPVM2PGM f) _V = f by Th30;

end;
let f be directed PVertexMapping of G1,G2;

reducibility

(DPVM2PGM f) _V = f by Th30;

theorem :: GLIB_011:31

for G1, G2 being non-multi _Graph

for f being directed PVertexMapping of G1,G2 holds PVM2PGM f = DPVM2PGM f

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

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

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

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

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

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

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

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

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 )

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

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;

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;

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

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

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

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

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

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 )

( 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 )

( G2 is G1 -Disomorphic iff ex f being directed PVertexMapping of G1,G2 st f is Disomorphism )

proof end;

:: An example why this isn't always the case is the embedding of P_3 into K_3