:: by Sebastian Koch

::

:: Received August 29, 2019

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

:: into FUNCT_1 ?

:: into FUNCT_1 ?

theorem Th2: :: GLIB_010:2

for A being one-to-one Function

for C, D being Function st D * A = C | (dom A) holds

C * (A ") = D | (dom (A "))

for C, D being Function st D * A = C | (dom A) holds

C * (A ") = D | (dom (A "))

proof end;

:: BEGIN into GLIB_003 ?

registration

let G be non _finite _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is _finite

not G .set (ELabelSelector,X) is _finite

not G .set (VLabelSelector,X) is _finite

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is _finite

proof end;

coherence not G .set (ELabelSelector,X) is _finite

proof end;

coherence not G .set (VLabelSelector,X) is _finite

proof end;

registration

let G be non loopless _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is loopless

not G .set (ELabelSelector,X) is loopless

not G .set (VLabelSelector,X) is loopless

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is loopless

proof end;

coherence not G .set (ELabelSelector,X) is loopless

proof end;

coherence not G .set (VLabelSelector,X) is loopless

proof end;

registration

let G be non non-multi _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is non-multi

not G .set (ELabelSelector,X) is non-multi

not G .set (VLabelSelector,X) is non-multi

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is non-multi

proof end;

coherence not G .set (ELabelSelector,X) is non-multi

proof end;

coherence not G .set (VLabelSelector,X) is non-multi

proof end;

registration

let G be non non-Dmulti _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is non-Dmulti

not G .set (ELabelSelector,X) is non-Dmulti

not G .set (VLabelSelector,X) is non-Dmulti

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is non-Dmulti

proof end;

coherence not G .set (ELabelSelector,X) is non-Dmulti

proof end;

coherence not G .set (VLabelSelector,X) is non-Dmulti

proof end;

registration

let G be non connected _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is connected

not G .set (ELabelSelector,X) is connected

not G .set (VLabelSelector,X) is connected

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is connected

proof end;

coherence not G .set (ELabelSelector,X) is connected

proof end;

coherence not G .set (VLabelSelector,X) is connected

proof end;

registration

let G be non acyclic _Graph;

let X be set ;

coherence

not G .set (WeightSelector,X) is acyclic

not G .set (ELabelSelector,X) is acyclic

not G .set (VLabelSelector,X) is acyclic

end;
let X be set ;

coherence

not G .set (WeightSelector,X) is acyclic

proof end;

coherence not G .set (ELabelSelector,X) is acyclic

proof end;

coherence not G .set (VLabelSelector,X) is acyclic

proof end;

definition

let G be _Graph;

end;
attr G is elabel-full means :Def1: :: GLIB_010:def 1

( ELabelSelector in dom G & ex f being ManySortedSet of the_Edges_of G st G . ELabelSelector = f );

( ELabelSelector in dom G & ex f being ManySortedSet of the_Edges_of G st G . ELabelSelector = f );

attr G is vlabel-full means :Def2: :: GLIB_010:def 2

( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f );

( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f );

:: deftheorem Def1 defines elabel-full GLIB_010:def 1 :

for G being _Graph holds

( G is elabel-full iff ( ELabelSelector in dom G & ex f being ManySortedSet of the_Edges_of G st G . ELabelSelector = f ) );

for G being _Graph holds

( G is elabel-full iff ( ELabelSelector in dom G & ex f being ManySortedSet of the_Edges_of G st G . ELabelSelector = f ) );

:: deftheorem Def2 defines vlabel-full GLIB_010:def 2 :

for G being _Graph holds

( G is vlabel-full iff ( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f ) );

for G being _Graph holds

( G is vlabel-full iff ( VLabelSelector in dom G & ex f being ManySortedSet of the_Vertices_of G st G . VLabelSelector = f ) );

registration

for b_{1} being _Graph st b_{1} is elabel-full holds

b_{1} is [ELabeled]

for b_{1} being _Graph st b_{1} is vlabel-full holds

b_{1} is [VLabeled]
end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] elabel-full -> [ELabeled] for set ;

coherence for b

b

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] vlabel-full -> [VLabeled] for set ;

coherence for b

b

proof end;

:: deftheorem Def3 defines elabel-distinct GLIB_010:def 3 :

for G being EGraph holds

( G is elabel-distinct iff the_ELabel_of G is one-to-one );

for G being EGraph holds

( G is elabel-distinct iff the_ELabel_of G is one-to-one );

:: deftheorem Def4 defines vlabel-distinct GLIB_010:def 4 :

for G being VGraph holds

( G is vlabel-distinct iff the_VLabel_of G is one-to-one );

for G being VGraph holds

( G is vlabel-distinct iff the_VLabel_of G is one-to-one );

registration

let G be _Graph;

coherence

( G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-full & G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct )

( G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-full & G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-distinct )

end;
coherence

( G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-full & G .set (ELabelSelector,(id (the_Edges_of G))) is elabel-distinct )

proof end;

coherence ( G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-full & G .set (VLabelSelector,(id (the_Vertices_of G))) is vlabel-distinct )

proof end;

registration

ex b_{1} being EGraph st

( b_{1} is elabel-distinct & b_{1} is elabel-full )

ex b_{1} being VGraph st

( b_{1} is vlabel-distinct & b_{1} is vlabel-full )
end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] elabel-full elabel-distinct for set ;

existence ex b

( b

proof end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [VLabeled] vlabel-full vlabel-distinct for set ;

existence ex b

( b

proof end;

definition

let G be elabel-full _Graph;

:: original: the_ELabel_of

redefine func the_ELabel_of G -> ManySortedSet of the_Edges_of G;

coherence

the_ELabel_of G is ManySortedSet of the_Edges_of G

end;
:: original: the_ELabel_of

redefine func the_ELabel_of G -> ManySortedSet of the_Edges_of G;

coherence

the_ELabel_of G is ManySortedSet of the_Edges_of G

proof end;

definition

let G be vlabel-full _Graph;

:: original: the_VLabel_of

redefine func the_VLabel_of G -> ManySortedSet of the_Vertices_of G;

coherence

the_VLabel_of G is ManySortedSet of the_Vertices_of G

end;
:: original: the_VLabel_of

redefine func the_VLabel_of G -> ManySortedSet of the_Vertices_of G;

coherence

the_VLabel_of G is ManySortedSet of the_Vertices_of G

proof end;

registration

let G be elabel-full _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is elabel-full

G .set (VLabelSelector,X) is elabel-full

end;
let X be set ;

coherence

G .set (WeightSelector,X) is elabel-full

proof end;

coherence G .set (VLabelSelector,X) is elabel-full

proof end;

registration

let G be vlabel-full _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is vlabel-full

G .set (ELabelSelector,X) is vlabel-full

end;
let X be set ;

coherence

G .set (WeightSelector,X) is vlabel-full

proof end;

coherence G .set (ELabelSelector,X) is vlabel-full

proof end;

registration

let G be elabel-distinct EGraph;

let X be set ;

coherence

G .set (WeightSelector,X) is elabel-distinct

G .set (VLabelSelector,X) is elabel-distinct

end;
let X be set ;

coherence

G .set (WeightSelector,X) is elabel-distinct

proof end;

coherence G .set (VLabelSelector,X) is elabel-distinct

proof end;

registration

let G be vlabel-distinct VGraph;

let X be set ;

coherence

G .set (WeightSelector,X) is vlabel-distinct

G .set (ELabelSelector,X) is vlabel-distinct

end;
let X be set ;

coherence

G .set (WeightSelector,X) is vlabel-distinct

proof end;

coherence G .set (ELabelSelector,X) is vlabel-distinct

proof end;

registration

ex b_{1} being EVGraph st

( b_{1} is elabel-full & b_{1} is elabel-distinct & b_{1} is vlabel-full & b_{1} is vlabel-distinct )
end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [ELabeled] [VLabeled] elabel-full vlabel-full elabel-distinct vlabel-distinct for set ;

existence ex b

( b

proof end;

:: END into GLIB_003 ?

registration

let G1 be WGraph;

let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (WeightSelector,(the_Weight_of G1)) is [Weighted]

end;
let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (WeightSelector,(the_Weight_of G1)) is [Weighted]

proof end;

registration

let G1 be EGraph;

let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (ELabelSelector,(the_ELabel_of G1)) is [ELabeled]

end;
let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (ELabelSelector,(the_ELabel_of G1)) is [ELabeled]

proof end;

registration

let G1 be VGraph;

let V be set ;

let G2 be reverseEdgeDirections of G1,V;

coherence

G2 .set (VLabelSelector,(the_VLabel_of G1)) is [VLabeled]

end;
let V be set ;

let G2 be reverseEdgeDirections of G1,V;

coherence

G2 .set (VLabelSelector,(the_VLabel_of G1)) is [VLabeled]

proof end;

registration

let G1 be elabel-full _Graph;

let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-full

end;
let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-full

proof end;

registration

let G1 be vlabel-full _Graph;

let V be set ;

let G2 be reverseEdgeDirections of G1,V;

coherence

G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-full

end;
let V be set ;

let G2 be reverseEdgeDirections of G1,V;

coherence

G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-full

proof end;

registration

let G1 be elabel-distinct EGraph;

let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-distinct

end;
let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (ELabelSelector,(the_ELabel_of G1)) is elabel-distinct

proof end;

registration

let G1 be vlabel-distinct VGraph;

let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-distinct

end;
let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (VLabelSelector,(the_VLabel_of G1)) is vlabel-distinct

proof end;

definition

let G be GraphStruct;

end;
attr G is [Ordered] means :Def6: :: GLIB_010:def 6

( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) );

( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) );

:: deftheorem Def6 defines [Ordered] GLIB_010:def 6 :

for G being GraphStruct holds

( G is [Ordered] iff ( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) ) );

for G being GraphStruct holds

( G is [Ordered] iff ( OrderingSelector in dom G & G . OrderingSelector is Enumeration of (the_Vertices_of G) ) );

Lm1: not OrderingSelector in _GraphSelectors

by GLIB_000:def 5, GLIB_000:1, ENUMSET1:def 2;

registration

let G be _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is [Graph-like] by Lm1, GLIB_000:10;

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is [Graph-like] by Lm1, GLIB_000:10;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let G be _Graph;

let X be Enumeration of (the_Vertices_of G);

coherence

G .set (OrderingSelector,X) is [Ordered]

end;
let X be Enumeration of (the_Vertices_of G);

coherence

G .set (OrderingSelector,X) is [Ordered]

proof end;

registration

ex b_{1} being GraphStruct st

( b_{1} is [Graph-like] & b_{1} is [Weighted] & b_{1} is [ELabeled] & b_{1} is [VLabeled] & b_{1} is [Ordered] )
end;

cluster Relation-like NAT -defined Function-like finite [Graph-like] [Weighted] [ELabeled] [VLabeled] [Ordered] for set ;

existence ex b

( b

proof end;

:: the definitions of O,WO,EO,VO,WEO,WVO,EVO and WEVOGraph are omitted

:: as is would simply clutter the already rich graph notation

:: as is would simply clutter the already rich graph notation

definition

let G be [Ordered] _Graph;

coherence

G . OrderingSelector is Enumeration of (the_Vertices_of G);

by Def6;

end;
func the_Ordering_of G -> Enumeration of (the_Vertices_of G) equals :: GLIB_010:def 7

G . OrderingSelector;

correctness G . OrderingSelector;

coherence

G . OrderingSelector is Enumeration of (the_Vertices_of G);

by Def6;

:: deftheorem defines the_Ordering_of GLIB_010:def 7 :

for G being [Ordered] _Graph holds the_Ordering_of G = G . OrderingSelector;

for G being [Ordered] _Graph holds the_Ordering_of G = G . OrderingSelector;

registration

let G be elabel-full _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is elabel-full

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is elabel-full

proof end;

registration

let G be vlabel-full _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is vlabel-full

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is vlabel-full

proof end;

registration

let G be elabel-distinct EGraph;

let X be set ;

coherence

G .set (OrderingSelector,X) is elabel-distinct

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is elabel-distinct

proof end;

registration

let G be vlabel-distinct VGraph;

let X be set ;

coherence

G .set (OrderingSelector,X) is vlabel-distinct

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is vlabel-distinct

proof end;

registration
end;

registration

let G be non _finite _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is _finite

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is _finite

proof end;

registration

let G be loopless _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is loopless

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is loopless

proof end;

registration

let G be non loopless _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is loopless

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is loopless

proof end;

registration

let G be _trivial _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is _trivial

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is _trivial

proof end;

registration

let G be non _trivial _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is _trivial

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is _trivial

proof end;

registration

let G be non-multi _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is non-multi

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is non-multi

proof end;

registration

let G be non non-multi _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is non-multi

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is non-multi

proof end;

registration

let G be non-Dmulti _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is non-Dmulti

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is non-Dmulti

proof end;

registration

let G be non non-Dmulti _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is non-Dmulti

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is non-Dmulti

proof end;

registration

let G be connected _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is connected by Th3, GLIB_002:8;

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is connected by Th3, GLIB_002:8;

registration

let G be non connected _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is connected

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is connected

proof end;

registration

let G be acyclic _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is acyclic by Th3, GLIB_002:44;

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is acyclic by Th3, GLIB_002:44;

registration

let G be non acyclic _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is acyclic

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is acyclic

proof end;

registration

let G be edgeless _Graph;

let X be set ;

coherence

G .set (OrderingSelector,X) is edgeless by Th3, GLIB_008:52;

end;
let X be set ;

coherence

G .set (OrderingSelector,X) is edgeless by Th3, GLIB_008:52;

registration

let G be non edgeless _Graph;

let X be set ;

coherence

not G .set (OrderingSelector,X) is edgeless

end;
let X be set ;

coherence

not G .set (OrderingSelector,X) is edgeless

proof end;

registration

let G be [Ordered] _Graph;

let X be set ;

coherence

G .set (WeightSelector,X) is [Ordered]

G .set (ELabelSelector,X) is [Ordered]

G .set (VLabelSelector,X) is [Ordered]

end;
let X be set ;

coherence

G .set (WeightSelector,X) is [Ordered]

proof end;

coherence G .set (ELabelSelector,X) is [Ordered]

proof end;

coherence G .set (VLabelSelector,X) is [Ordered]

proof end;

:: Subgraph properties for ordered graphs are mostly omitted

:: because removing vertices of the graph creates gaps in the ordering.

:: A theorem describing how to fill these gaps (in such a way that:

:: for v1,v2 in V(G2) holds O(G2).v1 c= O(G2).v2 implies O(G1).v1 c= O(G1).v2)

:: is desirable, but will not be discussed here.

:: because removing vertices of the graph creates gaps in the ordering.

:: A theorem describing how to fill these gaps (in such a way that:

:: for v1,v2 in V(G2) holds O(G2).v1 c= O(G2).v2 implies O(G1).v1 c= O(G1).v2)

:: is desirable, but will not be discussed here.

registration

let G1 be [Ordered] _Graph;

let G2 be spanning Subgraph of G1;

coherence

G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered]

end;
let G2 be spanning Subgraph of G1;

coherence

G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered]

proof end;

registration

let G1 be [Ordered] _Graph;

let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered]

end;
let E be set ;

let G2 be reverseEdgeDirections of G1,E;

coherence

G2 .set (OrderingSelector,(the_Ordering_of G1)) is [Ordered]

proof end;

Lm2: for G1, G2 being _Graph ex f, g being Function st

( [{},{}] = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) )

proof end;

definition

let G1, G2 be _Graph;

ex b_{1} being object ex f, g being Function st

( b_{1} = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) )

end;
mode PGraphMapping of G1,G2 -> object means :Def8: :: GLIB_010:def 8

ex f, g being Function st

( it = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) );

existence ex f, g being Function st

( it = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) );

ex b

( b

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) )

proof end;

:: deftheorem Def8 defines PGraphMapping GLIB_010:def 8 :

for G1, G2 being _Graph

for b_{3} being object holds

( b_{3} is PGraphMapping of G1,G2 iff ex f, g being Function st

( b_{3} = [f,g] & dom f c= the_Vertices_of G1 & rng f c= the_Vertices_of G2 & dom g c= the_Edges_of G1 & rng g c= the_Edges_of G2 & ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) ) );

for G1, G2 being _Graph

for b

( b

( b

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) ) );

Lm3: for G1, G2 being _Graph holds [{},{}] is PGraphMapping of G1,G2

proof end;

registration

let G1, G2 be _Graph;

coherence

for b_{1} being PGraphMapping of G1,G2 holds b_{1} is pair

end;
coherence

for b

proof end;

notation

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

synonym F _V for G1 `1 ;

synonym F _E for G1 `2 ;

end;
let F be PGraphMapping of G1,G2;

synonym F _V for G1 `1 ;

synonym F _E for G1 `2 ;

registration
end;

registration

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

coherence

for b_{1} being set st b_{1} = _V holds

( b_{1} is Function-like & b_{1} is Relation-like )

for b_{1} being set st b_{1} = _E holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let F be PGraphMapping of G1,G2;

coherence

for b

( b

proof end;

coherence for b

( b

proof end;

registration

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

coherence

for b_{1} being Function st b_{1} = _V holds

( b_{1} is the_Vertices_of G1 -defined & b_{1} is the_Vertices_of G2 -valued )

for b_{1} being Function st b_{1} = _E holds

( b_{1} is the_Edges_of G1 -defined & b_{1} is the_Edges_of G2 -valued )

end;
let F be PGraphMapping of G1,G2;

coherence

for b

( b

proof end;

coherence for b

( b

proof end;

definition

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

:: original: _V

redefine func F _V -> PartFunc of (the_Vertices_of G1),(the_Vertices_of G2);

coherence

_V is PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

redefine func F _E -> PartFunc of (the_Edges_of G1),(the_Edges_of G2);

coherence

_E is PartFunc of (the_Edges_of G1),(the_Edges_of G2)

end;
let F be PGraphMapping of G1,G2;

:: original: _V

redefine func F _V -> PartFunc of (the_Vertices_of G1),(the_Vertices_of G2);

coherence

_V is PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

proof end;

:: original: _Eredefine func F _E -> PartFunc of (the_Edges_of G1),(the_Edges_of G2);

coherence

_E is PartFunc of (the_Edges_of G1),(the_Edges_of G2)

proof end;

theorem Th4: :: GLIB_010:4

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds

(F _E) . e Joins (F _V) . v,(F _V) . w,G2

for F being PGraphMapping of G1,G2

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e Joins v,w,G1 holds

(F _E) . e Joins (F _V) . v,(F _V) . w,G2

proof end;

theorem Th5: :: GLIB_010:5

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for e being object st e in dom (F _E) holds

( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) )

for F being PGraphMapping of G1,G2

for e being object st e in dom (F _E) holds

( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) )

proof end;

theorem Th6: :: GLIB_010:6

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for e being object st e in rng (F _E) holds

( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )

for F being PGraphMapping of G1,G2

for e being object st e in rng (F _E) holds

( (the_Source_of G2) . e in rng (F _V) & (the_Target_of G2) . e in rng (F _V) )

proof end;

theorem Th7: :: GLIB_010:7

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( dom (F _E) c= G1 .edgesBetween (dom (F _V)) & rng (F _E) c= G2 .edgesBetween (rng (F _V)) )

for F being PGraphMapping of G1,G2 holds

( dom (F _E) c= G1 .edgesBetween (dom (F _V)) & rng (F _E) c= G2 .edgesBetween (rng (F _V)) )

proof end;

theorem Th8: :: GLIB_010:8

for G1, G2 being _Graph

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) holds

[f,g] is PGraphMapping of G1,G2

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G1 holds

g . e Joins f . v,f . w,G2 ) holds

[f,g] is PGraphMapping of G1,G2

proof end;

theorem Th9: :: GLIB_010:9

for G1, G2, G3, G4 being _Graph

for F being PGraphMapping of G1,G2 st G1 == G3 & G2 == G4 holds

F is PGraphMapping of G3,G4

for F being PGraphMapping of G1,G2 st G1 == G3 & G2 == G4 holds

F is PGraphMapping of G3,G4

proof end;

theorem Th10: :: GLIB_010:10

for G1, G2, G3, G4 being _Graph

for F being PGraphMapping of G1,G2 st ex E1, E2 being set st

( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) holds

F is PGraphMapping of G3,G4

for F being PGraphMapping of G1,G2 st ex E1, E2 being set st

( G3 is reverseEdgeDirections of G1,E1 & G4 is reverseEdgeDirections of G2,E2 ) holds

F is PGraphMapping of G3,G4

proof end;

definition

let G be _Graph;

[(id (the_Vertices_of G)),(id (the_Edges_of G))] is PGraphMapping of G,G

end;
func id G -> PGraphMapping of G,G equals :: GLIB_010:def 9

[(id (the_Vertices_of G)),(id (the_Edges_of G))];

coherence [(id (the_Vertices_of G)),(id (the_Edges_of G))];

[(id (the_Vertices_of G)),(id (the_Edges_of G))] is PGraphMapping of G,G

proof end;

:: deftheorem defines id GLIB_010:def 9 :

for G being _Graph holds id G = [(id (the_Vertices_of G)),(id (the_Edges_of G))];

for G being _Graph holds id G = [(id (the_Vertices_of G)),(id (the_Edges_of G))];

theorem :: GLIB_010:12

for G1 being _Graph

for E being set

for G2 being reverseEdgeDirections of G1,E holds

( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )

for E being set

for G2 being reverseEdgeDirections of G1,E holds

( id G1 = id G2 & id G1 is PGraphMapping of G1,G2 )

proof end;

definition

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

end;
let F be PGraphMapping of G1,G2;

attr F is total means :Def11: :: GLIB_010:def 11

( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 );

( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 );

attr F is onto means :Def12: :: GLIB_010:def 12

( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 );

( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 );

attr F is directed means :Def14: :: GLIB_010:def 14

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds

(F _E) . e DJoins (F _V) . v,(F _V) . w,G2;

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds

(F _E) . e DJoins (F _V) . v,(F _V) . w,G2;

attr F is semi-continuous means :Def15: :: GLIB_010:def 15

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 holds

e Joins v,w,G1;

for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 holds

e Joins v,w,G1;

attr F is continuous means :Def16: :: GLIB_010:def 16

for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 );

for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 );

:: deftheorem Def10 defines empty GLIB_010:def 10 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is empty iff dom (F _V) is empty );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is empty iff dom (F _V) is empty );

:: deftheorem Def11 defines total GLIB_010:def 11 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is total iff ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is total iff ( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) );

:: deftheorem Def12 defines onto GLIB_010:def 12 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is onto iff ( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is onto iff ( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 ) );

:: deftheorem Def13 defines one-to-one GLIB_010:def 13 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is one-to-one iff ( F _V is one-to-one & F _E is one-to-one ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is one-to-one iff ( F _V is one-to-one & F _E is one-to-one ) );

:: deftheorem Def14 defines directed GLIB_010:def 14 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is directed iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds

(F _E) . e DJoins (F _V) . v,(F _V) . w,G2 );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is directed iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds

(F _E) . e DJoins (F _V) . v,(F _V) . w,G2 );

:: deftheorem Def15 defines semi-continuous GLIB_010:def 15 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is semi-continuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 holds

e Joins v,w,G1 );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is semi-continuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 holds

e Joins v,w,G1 );

:: deftheorem Def16 defines continuous GLIB_010:def 16 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is continuous iff for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is continuous iff for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 Joins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

( e Joins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) );

:: deftheorem Def17 defines semi-Dcontinuous GLIB_010:def 17 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 holds

e DJoins v,w,G1 );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 holds

e DJoins v,w,G1 );

:: deftheorem Def18 defines Dcontinuous GLIB_010:def 18 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is Dcontinuous iff for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is Dcontinuous iff for e9, v, w being object st v in dom (F _V) & w in dom (F _V) & e9 DJoins (F _V) . v,(F _V) . w,G2 holds

ex e being object st

( e DJoins v,w,G1 & e in dom (F _E) & (F _E) . e = e9 ) );

:: at first properties of these attributes for the PGM are studied

:: regardless of the kinds of graph involved

:: regardless of the kinds of graph involved

theorem Th13: :: GLIB_010:13

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is directed iff for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

for F being PGraphMapping of G1,G2 holds

( F is directed iff for e being object st e in dom (F _E) holds

( (the_Source_of G2) . ((F _E) . e) = (F _V) . ((the_Source_of G1) . e) & (the_Target_of G2) . ((F _E) . e) = (F _V) . ((the_Target_of G1) . e) ) )

proof end;

:: |dom F_E is probably not required, as the PGM property

:: enforces such a relationship between F_V and F_E

:: enforces such a relationship between F_V and F_E

theorem :: GLIB_010:14

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is directed iff ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) ) )

for F being PGraphMapping of G1,G2 holds

( F is directed iff ( (the_Source_of G2) * (F _E) = (F _V) * ((the_Source_of G1) | (dom (F _E))) & (the_Target_of G2) * (F _E) = (F _V) * ((the_Target_of G1) | (dom (F _E))) ) )

proof end;

theorem Th16: :: GLIB_010:16

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) holds

( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) )

for F being PGraphMapping of G1,G2 holds

( F is semi-Dcontinuous iff for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) holds

( e DJoins v,w,G1 iff (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) )

proof end;

registration

let G1, G2 be _Graph;

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

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

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

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

end;
cluster pair empty one-to-one directed semi-continuous continuous semi-Dcontinuous Dcontinuous for PGraphMapping of G1,G2;

existence ex b

( b

proof end;

cluster pair non empty one-to-one directed semi-continuous semi-Dcontinuous for PGraphMapping of G1,G2;

existence ex b

( not b

proof end;

registration

let G1, G2 be _Graph;

let F be empty PGraphMapping of G1,G2;

coherence

for b_{1} being set st b_{1} = F _V holds

b_{1} is empty

for b_{1} being set st b_{1} = F _E holds

b_{1} is empty

end;
let F be empty PGraphMapping of G1,G2;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

coherence

for b_{1} being set st b_{1} = F _V holds

not b_{1} is empty

end;
let F be non empty PGraphMapping of G1,G2;

coherence

for b

not b

proof end;

registration

let G1, G2 be _Graph;

let F be one-to-one PGraphMapping of G1,G2;

coherence

for b_{1} being Function st b_{1} = F _V holds

b_{1} is one-to-one
by Def13;

coherence

for b_{1} being Function st b_{1} = F _E holds

b_{1} is one-to-one
by Def13;

end;
let F be one-to-one PGraphMapping of G1,G2;

coherence

for b

b

coherence

for b

b

theorem Th17: :: GLIB_010:17

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F is semi-continuous

for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F is semi-continuous

proof end;

theorem Th18: :: GLIB_010:18

for G1, G2 being _Graph

for F being directed PGraphMapping of G1,G2 st F _V is one-to-one holds

F is semi-Dcontinuous

for F being directed PGraphMapping of G1,G2 st F _V is one-to-one holds

F is semi-Dcontinuous

proof end;

theorem Th19: :: GLIB_010:19

for G1, G2 being _Graph

for F being semi-continuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds

F is continuous

for F being semi-continuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds

F is continuous

proof end;

theorem Th20: :: GLIB_010:20

for G1, G2 being _Graph

for F being semi-Dcontinuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds

F is Dcontinuous

for F being semi-Dcontinuous PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 holds

F is Dcontinuous

proof end;

theorem Th21: :: GLIB_010:21

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds

F is continuous

for F being PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds

F is continuous

proof end;

theorem Th22: :: GLIB_010:22

for G1, G2 being _Graph

for F being directed PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds

F is Dcontinuous

for F being directed PGraphMapping of G1,G2 st F _V is one-to-one & rng (F _E) = the_Edges_of G2 holds

F is Dcontinuous

proof end;

theorem :: GLIB_010:23

for G1, G2 being _Graph

for F being continuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is semi-continuous

for F being continuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is semi-continuous

proof end;

theorem Th24: :: GLIB_010:24

for G1, G2 being _Graph

for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is semi-Dcontinuous

for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is semi-Dcontinuous

proof end;

theorem Th25: :: GLIB_010:25

for G1, G2 being _Graph

for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is directed

for F being Dcontinuous PGraphMapping of G1,G2 st F _E is one-to-one holds

F is directed

proof end;

theorem Th26: :: GLIB_010:26

for G1, G2 being _Graph

for F being semi-continuous PGraphMapping of G1,G2

for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) holds

v1 = v2

for F being semi-continuous PGraphMapping of G1,G2

for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v1,(F _V) . w,G2 ) holds

v1 = v2

proof end;

:: a special case of the following theorem is when G2 is without isolated

:: vertices and F is onto

:: vertices and F is onto

theorem :: GLIB_010:27

for G1, G2 being _Graph

for F being semi-continuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) holds

F _V is one-to-one

for F being semi-continuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e Joins (F _V) . v,(F _V) . w,G2 ) ) holds

F _V is one-to-one

proof end;

theorem Th28: :: GLIB_010:28

for G1, G2 being _Graph

for F being semi-Dcontinuous PGraphMapping of G1,G2

for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) holds

v1 = v2

for F being semi-Dcontinuous PGraphMapping of G1,G2

for v1, v2 being object st v1 in dom (F _V) & v2 in dom (F _V) & (F _V) . v1 = (F _V) . v2 & ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v1,(F _V) . w,G2 ) holds

v1 = v2

proof end;

:: again, a special case of the following theorem is when G2 is without

:: isolated vertices and F is onto

:: isolated vertices and F is onto

theorem :: GLIB_010:29

for G1, G2 being _Graph

for F being semi-Dcontinuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) ) holds

F _V is one-to-one

for F being semi-Dcontinuous PGraphMapping of G1,G2 st ( for v being object st v in dom (F _V) holds

ex e, w being object st

( e in dom (F _E) & w in dom (F _V) & (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 ) ) holds

F _V is one-to-one

proof end;

registration

let G1, G2 be _Graph;

coherence

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

b_{1} is semi-continuous
by Th17;

coherence

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

b_{1} is semi-Dcontinuous
by Th18;

coherence

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

b_{1} is continuous
by Th21;

coherence

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

b_{1} is Dcontinuous
by Th22;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is semi-continuous & b_{1} is onto holds

b_{1} is continuous
by Th19;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is semi-Dcontinuous holds

( b_{1} is directed & b_{1} is semi-continuous )

for b_{1} being PGraphMapping of G1,G2 st b_{1} is semi-Dcontinuous & b_{1} is onto holds

b_{1} is Dcontinuous
by Th20;

coherence

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

b_{1} is continuous

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

( b_{1} is directed & b_{1} is semi-Dcontinuous )
by Th25, Th24;

coherence

for b_{1} being PGraphMapping 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 PGraphMapping of G1,G2 st b_{1} is total holds

not b_{1} is empty
;

coherence

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

not b_{1} is empty
;

end;
coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

( b

proof end;

coherence for b

b

coherence

for b

b

proof end;

coherence for b

( b

coherence

for b

( b

coherence

for b

not b

coherence

for b

not b

registration

let G be _Graph;

coherence

( id G is total & not id G is empty & id G is onto & id G is one-to-one & id G is Dcontinuous )

end;
coherence

( id G is total & not id G is empty & id G is onto & id G is one-to-one & id G is Dcontinuous )

proof end;

theorem Th30: :: GLIB_010:30

for G1, G2 being _Graph

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 holds

g . e DJoins f . v,f . w,G2 ) holds

[f,g] is directed PGraphMapping of G1,G2

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e DJoins v,w,G1 holds

g . e DJoins f . v,f . w,G2 ) holds

[f,g] is directed PGraphMapping of G1,G2

proof end;

theorem Th31: :: GLIB_010:31

for G1, G2 being _Graph

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) holds

[f,g] is semi-continuous PGraphMapping of G1,G2

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e Joins v,w,G1 iff g . e Joins f . v,f . w,G2 ) ) holds

[f,g] is semi-continuous PGraphMapping of G1,G2

proof end;

theorem :: GLIB_010:32

for G1, G2 being _Graph

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e DJoins v,w,G1 iff g . e DJoins f . v,f . w,G2 ) ) holds

[f,g] is semi-Dcontinuous PGraphMapping of G1,G2

for f being PartFunc of (the_Vertices_of G1),(the_Vertices_of G2)

for g being PartFunc of (the_Edges_of G1),(the_Edges_of G2) st ( for e being object st e in dom g holds

( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f holds

( e DJoins v,w,G1 iff g . e DJoins f . v,f . w,G2 ) ) holds

[f,g] is semi-Dcontinuous PGraphMapping of G1,G2

proof end;

theorem Th34: :: GLIB_010:34

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is total holds

for v being Vertex of G1 holds (F _V) . v is Vertex of G2

for F being PGraphMapping of G1,G2 st F is total holds

for v being Vertex of G1 holds (F _V) . v is Vertex of G2

proof end;

theorem Th35: :: GLIB_010:35

for G1, G2 being _Graph

for F being PGraphMapping 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 PGraphMapping 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 Th36: :: GLIB_010:36

for G1, G2 being _Graph

for F being continuous PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 & G1 is loopless holds

G2 is loopless

for F being continuous PGraphMapping of G1,G2 st rng (F _V) = the_Vertices_of G2 & G1 is loopless holds

G2 is loopless

proof end;

theorem :: GLIB_010:37

for G1, G2 being _Graph

for F being semi-continuous PGraphMapping of G1,G2 st F is onto & G1 is loopless holds

G2 is loopless by Th36;

for F being semi-continuous PGraphMapping of G1,G2 st F is onto & G1 is loopless holds

G2 is loopless by Th36;

theorem :: GLIB_010:38

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 & G1 is edgeless holds

G2 is edgeless ;

for F being PGraphMapping of G1,G2 st rng (F _E) = the_Edges_of G2 & G1 is edgeless holds

G2 is edgeless ;

theorem :: GLIB_010:39

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is onto & G1 is edgeless holds

G2 is edgeless ;

for F being PGraphMapping of G1,G2 st F is onto & G1 is edgeless holds

G2 is edgeless ;

:: next properties of these attributes for the PGM are studied

:: when G1 or G2 has a certain property

:: when G1 or G2 has a certain property

theorem :: GLIB_010:40

for G1 being _Graph

for G2 being non-multi _Graph

for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

for G2 being non-multi _Graph

for F1, F2 being PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

proof end;

theorem :: GLIB_010:41

for G1 being _Graph

for G2 being non-Dmulti _Graph

for F1, F2 being directed PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

for G2 being non-Dmulti _Graph

for F1, F2 being directed PGraphMapping of G1,G2 st F1 _V = F2 _V & dom (F1 _E) = dom (F2 _E) holds

F1 = F2

proof end;

theorem :: GLIB_010:42

for G1 being non-multi _Graph

for G2 being _Graph

for F being semi-continuous PGraphMapping of G1,G2 holds F _E is one-to-one

for G2 being _Graph

for F being semi-continuous PGraphMapping of G1,G2 holds F _E is one-to-one

proof end;

theorem :: GLIB_010:43

for G1 being non-multi _Graph

for G2 being _Graph

for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F _E is one-to-one

for G2 being _Graph

for F being PGraphMapping of G1,G2 st F _V is one-to-one holds

F _E is one-to-one

proof end;

theorem :: GLIB_010:44

for G1 being non-Dmulti _Graph

for G2 being _Graph

for F being directed PGraphMapping of G1,G2 st F _V is one-to-one holds

F _E is one-to-one

for G2 being _Graph

for F being directed PGraphMapping of G1,G2 st F _V is one-to-one holds

F _E is one-to-one

proof end;

registration

let G1 be _Graph;

let G2 be loopless _Graph;

coherence

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

b_{1} is semi-Dcontinuous

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

b_{1} is Dcontinuous

end;
let G2 be loopless _Graph;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let G1 be _trivial _Graph;

let G2 be _Graph;

coherence

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

for b_{1} being PGraphMapping of G1,G2 st b_{1} is semi-continuous holds

b_{1} is semi-Dcontinuous

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

b_{1} is Dcontinuous

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 _trivial non-Dmulti _Graph;

let G2 be _Graph;

coherence

for b_{1} being PGraphMapping of G1,G2 holds b_{1} is one-to-one

end;
let G2 be _Graph;

coherence

for b

proof end;

registration

let G1 be _trivial edgeless _Graph;

let G2 be _Graph;

coherence

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

b_{1} is total

end;
let G2 be _Graph;

coherence

for b

b

proof end;

registration

let G1 be _Graph;

let G2 be _trivial edgeless _Graph;

coherence

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

b_{1} is onto

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

( b_{1} is semi-continuous & b_{1} is continuous )
by GLIB_000:def 13;

end;
let G2 be _trivial edgeless _Graph;

coherence

for b

b

proof end;

coherence for b

( b

:: define the concept of subgraph embedding and isomorphism

definition

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

end;
let F be PGraphMapping of G1,G2;

attr F is strong_SG-embedding means :: GLIB_010:def 20

( F is total & F is one-to-one & F is continuous );

( F is total & F is one-to-one & F is continuous );

:: the next one is not really important (since directed isomorphism works

:: just as well), but the term will be used with PVertexMappings later

:: anyway, so it is introduced here shortly as well.

:: just as well), but the term will be used with PVertexMappings later

:: anyway, so it is introduced here shortly as well.

attr F is Disomorphism means :: GLIB_010:def 22

( F is directed & F is total & F is one-to-one & F is onto );

( F is directed & F is total & F is one-to-one & F is onto );

:: deftheorem defines weak_SG-embedding GLIB_010:def 19 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is weak_SG-embedding iff ( F is total & F is one-to-one ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is weak_SG-embedding iff ( F is total & F is one-to-one ) );

:: deftheorem defines strong_SG-embedding GLIB_010:def 20 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is strong_SG-embedding iff ( F is total & F is one-to-one & F is continuous ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is strong_SG-embedding iff ( F is total & F is one-to-one & F is continuous ) );

:: deftheorem defines isomorphism GLIB_010:def 21 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is isomorphism iff ( F is total & F is one-to-one & F is onto ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is isomorphism iff ( F is total & F is one-to-one & F is onto ) );

:: deftheorem defines Disomorphism GLIB_010:def 22 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is Disomorphism iff ( F is directed & F is total & F is one-to-one & F is onto ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F is Disomorphism iff ( F is directed & F is total & F is one-to-one & F is onto ) );

registration

let G1, G2 be _Graph;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is weak_SG-embedding holds

( b_{1} is total & not b_{1} is empty & b_{1} is one-to-one & b_{1} is semi-continuous )
;

coherence

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

b_{1} is weak_SG-embedding
;

for b_{1} being PGraphMapping of G1,G2 st b_{1} is strong_SG-embedding holds

( b_{1} is total & not b_{1} is empty & b_{1} is one-to-one & b_{1} is continuous & b_{1} is weak_SG-embedding )
;

coherence

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

b_{1} is strong_SG-embedding
;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is weak_SG-embedding & b_{1} is continuous holds

b_{1} is strong_SG-embedding
;

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

( b_{1} is onto & b_{1} is semi-continuous & b_{1} is continuous & b_{1} is total & not b_{1} is empty & b_{1} is one-to-one & b_{1} is weak_SG-embedding & b_{1} is strong_SG-embedding )
;

coherence

for b_{1} being PGraphMapping 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
;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is strong_SG-embedding & b_{1} is onto holds

b_{1} is isomorphism
;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is weak_SG-embedding & b_{1} is continuous & b_{1} is onto holds

b_{1} is isomorphism
;

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

( b_{1} is directed & b_{1} is isomorphism & b_{1} is continuous & b_{1} is total & not b_{1} is empty & b_{1} is semi-Dcontinuous & b_{1} is semi-continuous & b_{1} is one-to-one & b_{1} is weak_SG-embedding & b_{1} is strong_SG-embedding )
;

coherence

for b_{1} being PGraphMapping of G1,G2 st b_{1} is directed & b_{1} is isomorphism holds

( b_{1} is Dcontinuous & b_{1} is Disomorphism )
;

end;
coherence

for b

( b

coherence

for b

b

cluster strong_SG-embedding -> non empty total one-to-one continuous weak_SG-embedding for PGraphMapping of G1,G2;

coherence for b

( b

coherence

for b

b

coherence

for b

b

cluster isomorphism -> non empty total onto one-to-one semi-continuous continuous weak_SG-embedding strong_SG-embedding for PGraphMapping of G1,G2;

coherence for b

( b

coherence

for b

b

coherence

for b

b

coherence

for b

b

cluster Disomorphism -> non empty total one-to-one directed semi-continuous continuous semi-Dcontinuous weak_SG-embedding strong_SG-embedding isomorphism for PGraphMapping of G1,G2;

coherence for b

( b

coherence

for b

( b

registration

let G be _Graph;

coherence

( id G is weak_SG-embedding & id G is strong_SG-embedding & id G is isomorphism & id G is Disomorphism ) ;

end;
coherence

( id G is weak_SG-embedding & id G is strong_SG-embedding & id G is isomorphism & id G is Disomorphism ) ;

registration

let G be _Graph;

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

( b_{1} is weak_SG-embedding & b_{1} is strong_SG-embedding & b_{1} is isomorphism & b_{1} is Disomorphism )

end;
cluster pair weak_SG-embedding strong_SG-embedding isomorphism Disomorphism for PGraphMapping of G,G;

existence ex b

( b

proof end;

theorem Th45: :: GLIB_010:45

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds

( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )

for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds

( G1 .order() c= G2 .order() & G1 .size() c= G2 .size() )

proof end;

theorem Th46: :: GLIB_010:46

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds

card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))

for F being PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds

card (G1 .edgesBetween (X,Y)) c= card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))

proof end;

theorem Th47: :: GLIB_010:47

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for X being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds

card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X))

for F being PGraphMapping of G1,G2

for X being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds

card (G1 .edgesBetween X) c= card (G2 .edgesBetween ((F _V) .: X))

proof end;

theorem Th48: :: GLIB_010:48

for G1, G2 being _Graph

for F being directed PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds

card (G1 .edgesDBetween (X,Y)) c= card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

for F being directed PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding holds

card (G1 .edgesDBetween (X,Y)) c= card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

proof end;

theorem Th49: :: GLIB_010:49

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds

( ( G2 is _trivial implies G1 is _trivial ) & ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )

for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds

( ( G2 is _trivial implies G1 is _trivial ) & ( G2 is non-multi implies G1 is non-multi ) & ( G2 is simple implies G1 is simple ) & ( G2 is _finite implies G1 is _finite ) )

proof end;

theorem Th50: :: GLIB_010:50

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding holds

( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )

for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding holds

( ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G2 is Dsimple implies G1 is Dsimple ) )

proof end;

theorem Th51: :: GLIB_010:51

for G1, G2 being _finite _Graph

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G1 .order() = G2 .order() & G1 .size() = G2 .size() holds

F is isomorphism

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G1 .order() = G2 .order() & G1 .size() = G2 .size() holds

F is isomorphism

proof end;

theorem Th52: :: GLIB_010:52

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is complete holds

G1 is complete

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is complete holds

G1 is complete

proof end;

:: isomorphism as an attribute

definition

let G1, G2 be _Graph;

end;
attr G2 is G1 -isomorphic means :Def23: :: GLIB_010:def 23

ex F being PGraphMapping of G1,G2 st F is isomorphism ;

ex F being PGraphMapping of G1,G2 st F is isomorphism ;

attr G2 is G1 -Disomorphic means :Def24: :: GLIB_010:def 24

ex F being PGraphMapping of G1,G2 st F is Disomorphism ;

ex F being PGraphMapping of G1,G2 st F is Disomorphism ;

:: deftheorem Def23 defines -isomorphic GLIB_010:def 23 :

for G1, G2 being _Graph holds

( G2 is G1 -isomorphic iff ex F being PGraphMapping of G1,G2 st F is isomorphism );

for G1, G2 being _Graph holds

( G2 is G1 -isomorphic iff ex F being PGraphMapping of G1,G2 st F is isomorphism );

:: deftheorem Def24 defines -Disomorphic GLIB_010:def 24 :

for G1, G2 being _Graph holds

( G2 is G1 -Disomorphic iff ex F being PGraphMapping of G1,G2 st F is Disomorphism );

for G1, G2 being _Graph holds

( G2 is G1 -Disomorphic iff ex F being PGraphMapping of G1,G2 st F is Disomorphism );

registration

let G be _Graph;

for b_{1} being _Graph st b_{1} is G -Disomorphic holds

b_{1} is G -isomorphic
;

end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] G -Disomorphic -> G -isomorphic for set ;

coherence for b

b

registration

let G be _Graph;

ex b_{1} being _Graph st

( b_{1} is G -Disomorphic & b_{1} is G -isomorphic )

end;
cluster Relation-like NAT -defined Function-like finite [Graph-like] G -isomorphic G -Disomorphic for set ;

existence ex b

( b

proof end;

registration

let G1 be _Graph;

let G2 be G1 -isomorphic _Graph;

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

( b_{1} is isomorphism & b_{1} is strong_SG-embedding & b_{1} is weak_SG-embedding & b_{1} is total & not b_{1} is empty & b_{1} is one-to-one & b_{1} is onto & b_{1} is semi-continuous & b_{1} is continuous )

end;
let G2 be G1 -isomorphic _Graph;

cluster pair non empty total onto one-to-one semi-continuous continuous weak_SG-embedding strong_SG-embedding isomorphism for PGraphMapping of G1,G2;

existence ex b

( b

proof end;

:: this is the main reason for using an attribute instead of predicate

:: for isomorphism

:: for isomorphism

definition

let G1 be _Graph;

let G2 be G1 -isomorphic _Graph;

mode Isomorphism of G1,G2 is isomorphism PGraphMapping of G1,G2;

end;
let G2 be G1 -isomorphic _Graph;

mode Isomorphism of G1,G2 is isomorphism PGraphMapping of G1,G2;

registration

let G1 be _Graph;

let G2 be G1 -Disomorphic _Graph;

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

( b_{1} is isomorphism & b_{1} is strong_SG-embedding & b_{1} is weak_SG-embedding & b_{1} is total & not b_{1} is empty & b_{1} is one-to-one & b_{1} is onto & b_{1} is directed & b_{1} is semi-Dcontinuous & b_{1} is Dcontinuous )

end;
let G2 be G1 -Disomorphic _Graph;

cluster pair non empty total onto one-to-one directed semi-Dcontinuous Dcontinuous weak_SG-embedding strong_SG-embedding isomorphism for PGraphMapping of G1,G2;

existence ex b

( b

proof end;

definition

let G1 be _Graph;

let G2 be G1 -Disomorphic _Graph;

mode DIsomorphism of G1,G2 is Disomorphism PGraphMapping of G1,G2;

end;
let G2 be G1 -Disomorphic _Graph;

mode DIsomorphism of G1,G2 is Disomorphism PGraphMapping of G1,G2;

:: define weight-/label-/ordering-preserving mappings

definition

let G1, G2 be WGraph;

let F be PGraphMapping of G1,G2;

end;
let F be PGraphMapping of G1,G2;

attr F is weight-preserving means :: GLIB_010:def 25

(the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E));

(the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E));

:: deftheorem defines weight-preserving GLIB_010:def 25 :

for G1, G2 being WGraph

for F being PGraphMapping of G1,G2 holds

( F is weight-preserving iff (the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E)) );

for G1, G2 being WGraph

for F being PGraphMapping of G1,G2 holds

( F is weight-preserving iff (the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E)) );

definition

let G1, G2 be EGraph;

let F be PGraphMapping of G1,G2;

end;
let F be PGraphMapping of G1,G2;

attr F is elabel-preserving means :: GLIB_010:def 26

(the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E));

(the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E));

:: deftheorem defines elabel-preserving GLIB_010:def 26 :

for G1, G2 being EGraph

for F being PGraphMapping of G1,G2 holds

( F is elabel-preserving iff (the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E)) );

for G1, G2 being EGraph

for F being PGraphMapping of G1,G2 holds

( F is elabel-preserving iff (the_ELabel_of G2) * (F _E) = (the_ELabel_of G1) | (dom (F _E)) );

definition

let G1, G2 be VGraph;

let F be PGraphMapping of G1,G2;

end;
let F be PGraphMapping of G1,G2;

attr F is vlabel-preserving means :: GLIB_010:def 27

(the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V));

(the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V));

:: deftheorem defines vlabel-preserving GLIB_010:def 27 :

for G1, G2 being VGraph

for F being PGraphMapping of G1,G2 holds

( F is vlabel-preserving iff (the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V)) );

for G1, G2 being VGraph

for F being PGraphMapping of G1,G2 holds

( F is vlabel-preserving iff (the_VLabel_of G2) * (F _V) = (the_VLabel_of G1) | (dom (F _V)) );

definition

let G1, G2 be [Ordered] _Graph;

let F be PGraphMapping of G1,G2;

end;
let F be PGraphMapping of G1,G2;

attr F is ordering-preserving means :: GLIB_010:def 28

(the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V));

(the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V));

:: deftheorem defines ordering-preserving GLIB_010:def 28 :

for G1, G2 being [Ordered] _Graph

for F being PGraphMapping of G1,G2 holds

( F is ordering-preserving iff (the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V)) );

for G1, G2 being [Ordered] _Graph

for F being PGraphMapping of G1,G2 holds

( F is ordering-preserving iff (the_Ordering_of G2) * (F _V) = (the_Ordering_of G1) | (dom (F _V)) );

:: define domain and range of graph mappings

definition

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

the plain inducedSubgraph of G1, dom (F _V), dom (F _E) is inducedSubgraph of G1, dom (F _V), dom (F _E) ;

the plain inducedSubgraph of G2, rng (F _V), rng (F _E) is inducedSubgraph of G2, rng (F _V), rng (F _E) ;

end;
let F be PGraphMapping of G1,G2;

func dom F -> inducedSubgraph of G1, dom (F _V), dom (F _E) equals :: GLIB_010:def 29

the plain inducedSubgraph of G1, dom (F _V), dom (F _E);

coherence the plain inducedSubgraph of G1, dom (F _V), dom (F _E);

the plain inducedSubgraph of G1, dom (F _V), dom (F _E) is inducedSubgraph of G1, dom (F _V), dom (F _E) ;

func rng F -> inducedSubgraph of G2, rng (F _V), rng (F _E) equals :: GLIB_010:def 30

the plain inducedSubgraph of G2, rng (F _V), rng (F _E);

coherence the plain inducedSubgraph of G2, rng (F _V), rng (F _E);

the plain inducedSubgraph of G2, rng (F _V), rng (F _E) is inducedSubgraph of G2, rng (F _V), rng (F _E) ;

:: deftheorem defines dom GLIB_010:def 29 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds dom F = the plain inducedSubgraph of G1, dom (F _V), dom (F _E);

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds dom F = the plain inducedSubgraph of G1, dom (F _V), dom (F _E);

:: deftheorem defines rng GLIB_010:def 30 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds rng F = the plain inducedSubgraph of G2, rng (F _V), rng (F _E);

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds rng F = the plain inducedSubgraph of G2, rng (F _V), rng (F _E);

registration

let G1, G2 be _Graph;

let F be PGraphMapping of G1,G2;

coherence

dom F is plain ;

coherence

rng F is plain ;

end;
let F be PGraphMapping of G1,G2;

coherence

dom F is plain ;

coherence

rng F is plain ;

theorem Th54: :: GLIB_010:54

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2 holds

( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) & the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )

for F being non empty PGraphMapping of G1,G2 holds

( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) & the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )

proof end;

theorem Th55: :: GLIB_010:55

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2 holds

( F is total iff dom F == G1 )

for F being non empty PGraphMapping of G1,G2 holds

( F is total iff dom F == G1 )

proof end;

theorem :: GLIB_010:56

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2 holds

( F is onto iff rng F == G2 )

for F being non empty PGraphMapping of G1,G2 holds

( F is onto iff rng F == G2 )

proof end;

:: define restrictions of graph mappings

definition

let G1, G2 be _Graph;

let H be Subgraph of G1;

let F be PGraphMapping of G1,G2;

[((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))] is PGraphMapping of H,G2

end;
let H be Subgraph of G1;

let F be PGraphMapping of G1,G2;

func F | H -> PGraphMapping of H,G2 equals :: GLIB_010:def 31

[((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];

coherence [((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];

[((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))] is PGraphMapping of H,G2

proof end;

:: deftheorem defines | GLIB_010:def 31 :

for G1, G2 being _Graph

for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds F | H = [((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];

for G1, G2 being _Graph

for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds F | H = [((F _V) | (the_Vertices_of H)),((F _E) | (the_Edges_of H))];

theorem Th57: :: GLIB_010:57

for G1, G2 being _Graph

for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds

( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds

( ( F is empty implies F | H is empty ) & ( F is total implies F | H is total ) & ( F is one-to-one implies F | H is one-to-one ) & ( F is weak_SG-embedding implies F | H is weak_SG-embedding ) & ( F is semi-continuous implies F | H is semi-continuous ) & ( not F is onto implies not F | H is onto ) & ( F is directed implies F | H is directed ) & ( F is semi-Dcontinuous implies F | H is semi-Dcontinuous ) )

proof end;

theorem Th58: :: GLIB_010:58

for G1, G2 being _Graph

for V being set

for H being inducedSubgraph of G1,V

for F being PGraphMapping of G1,G2 holds

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

for V being set

for H being inducedSubgraph of G1,V

for F being PGraphMapping of G1,G2 holds

( ( F is continuous implies F | H is continuous ) & ( F is strong_SG-embedding implies F | H is strong_SG-embedding ) & ( F is Dcontinuous implies F | H is Dcontinuous ) )

proof end;

registration

let G1, G2 be _Graph;

let H be Subgraph of G1;

let F be empty PGraphMapping of G1,G2;

coherence

F | H is empty ;

end;
let H be Subgraph of G1;

let F be empty PGraphMapping of G1,G2;

coherence

F | H is empty ;

registration

let G1, G2 be _Graph;

let H be Subgraph of G1;

let F be one-to-one PGraphMapping of G1,G2;

coherence

F | H is one-to-one by Th57;

end;
let H be Subgraph of G1;

let F be one-to-one PGraphMapping of G1,G2;

coherence

F | H is one-to-one by Th57;

registration

let G1, G2 be _Graph;

let H be Subgraph of G1;

let F be semi-continuous PGraphMapping of G1,G2;

coherence

F | H is semi-continuous by Th57;

end;
let H be Subgraph of G1;

let F be semi-continuous PGraphMapping of G1,G2;

coherence

F | H is semi-continuous by Th57;

registration

let G1, G2 be _Graph;

let V be set ;

let H be inducedSubgraph of G1,V;

let F be continuous PGraphMapping of G1,G2;

coherence

F | H is continuous by Th58;

end;
let V be set ;

let H be inducedSubgraph of G1,V;

let F be continuous PGraphMapping of G1,G2;

coherence

F | H is continuous by Th58;

registration

let G1, G2 be _Graph;

let H be Subgraph of G1;

let F be directed PGraphMapping of G1,G2;

coherence

F | H is directed by Th57;

end;
let H be Subgraph of G1;

let F be directed PGraphMapping of G1,G2;

coherence

F | H is directed by Th57;

registration

let G1, G2 be _Graph;

let H be Subgraph of G1;

let F be semi-Dcontinuous PGraphMapping of G1,G2;

coherence

F | H is semi-Dcontinuous by Th57;

end;
let H be Subgraph of G1;

let F be semi-Dcontinuous PGraphMapping of G1,G2;

coherence

F | H is semi-Dcontinuous by Th57;

registration

let G1, G2 be _Graph;

let V be set ;

let H be inducedSubgraph of G1,V;

let F be Dcontinuous PGraphMapping of G1,G2;

coherence

F | H is Dcontinuous by Th58;

end;
let V be set ;

let H be inducedSubgraph of G1,V;

let F be Dcontinuous PGraphMapping of G1,G2;

coherence

F | H is Dcontinuous by Th58;

registration

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

coherence

F | (dom F) is total

end;
let F be non empty PGraphMapping of G1,G2;

coherence

F | (dom F) is total

proof end;

theorem Th59: :: GLIB_010:59

for G1, G2 being _Graph

for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds

( dom ((F | H) _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom ((F | H) _E) = (dom (F _E)) /\ (the_Edges_of H) ) by RELAT_1:61;

for H being Subgraph of G1

for F being PGraphMapping of G1,G2 holds

( dom ((F | H) _V) = (dom (F _V)) /\ (the_Vertices_of H) & dom ((F | H) _E) = (dom (F _E)) /\ (the_Edges_of H) ) by RELAT_1:61;

theorem :: GLIB_010:60

for G1, G2 being WGraph

for H being WSubgraph of G1

for F being PGraphMapping of G1,G2 st F is weight-preserving holds

F | H is weight-preserving

for H being WSubgraph of G1

for F being PGraphMapping of G1,G2 st F is weight-preserving holds

F | H is weight-preserving

proof end;

theorem :: GLIB_010:61

for G1, G2 being EGraph

for H being ESubgraph of G1

for F being PGraphMapping of G1,G2 st F is elabel-preserving holds

F | H is elabel-preserving

for H being ESubgraph of G1

for F being PGraphMapping of G1,G2 st F is elabel-preserving holds

F | H is elabel-preserving

proof end;

theorem :: GLIB_010:62

for G1, G2 being VGraph

for H being VSubgraph of G1

for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

F | H is vlabel-preserving

for H being VSubgraph of G1

for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

F | H is vlabel-preserving

proof end;

definition

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be PGraphMapping of G1,G2;

[((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))] is PGraphMapping of G1,H

end;
let H be Subgraph of G2;

let F be PGraphMapping of G1,G2;

func H |` F -> PGraphMapping of G1,H equals :: GLIB_010:def 32

[((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))];

coherence [((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))];

[((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))] is PGraphMapping of G1,H

proof end;

:: deftheorem defines |` GLIB_010:def 32 :

for G1, G2 being _Graph

for H being Subgraph of G2

for F being PGraphMapping of G1,G2 holds H |` F = [((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))];

for G1, G2 being _Graph

for H being Subgraph of G2

for F being PGraphMapping of G1,G2 holds H |` F = [((the_Vertices_of H) |` (F _V)),((the_Edges_of H) |` (F _E))];

theorem Th63: :: GLIB_010:63

for G1, G2 being _Graph

for H being Subgraph of G2

for F being PGraphMapping of G1,G2 holds

( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )

for H being Subgraph of G2

for F being PGraphMapping of G1,G2 holds

( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )

proof end;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be empty PGraphMapping of G1,G2;

coherence

H |` F is empty by Th63;

end;
let H be Subgraph of G2;

let F be empty PGraphMapping of G1,G2;

coherence

H |` F is empty by Th63;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be one-to-one PGraphMapping of G1,G2;

coherence

H |` F is one-to-one by Th63;

end;
let H be Subgraph of G2;

let F be one-to-one PGraphMapping of G1,G2;

coherence

H |` F is one-to-one by Th63;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be semi-continuous PGraphMapping of G1,G2;

coherence

H |` F is semi-continuous by Th63;

end;
let H be Subgraph of G2;

let F be semi-continuous PGraphMapping of G1,G2;

coherence

H |` F is semi-continuous by Th63;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be continuous PGraphMapping of G1,G2;

coherence

H |` F is continuous by Th63;

end;
let H be Subgraph of G2;

let F be continuous PGraphMapping of G1,G2;

coherence

H |` F is continuous by Th63;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be directed PGraphMapping of G1,G2;

coherence

H |` F is directed by Th63;

end;
let H be Subgraph of G2;

let F be directed PGraphMapping of G1,G2;

coherence

H |` F is directed by Th63;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be semi-Dcontinuous PGraphMapping of G1,G2;

coherence

H |` F is semi-Dcontinuous by Th63;

end;
let H be Subgraph of G2;

let F be semi-Dcontinuous PGraphMapping of G1,G2;

coherence

H |` F is semi-Dcontinuous by Th63;

registration

let G1, G2 be _Graph;

let H be Subgraph of G2;

let F be Dcontinuous PGraphMapping of G1,G2;

coherence

H |` F is Dcontinuous by Th63;

end;
let H be Subgraph of G2;

let F be Dcontinuous PGraphMapping of G1,G2;

coherence

H |` F is Dcontinuous by Th63;

registration

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

coherence

(rng F) |` F is onto

end;
let F be non empty PGraphMapping of G1,G2;

coherence

(rng F) |` F is onto

proof end;

theorem :: GLIB_010:64

for G1, G2 being _Graph

for H being Subgraph of G2

for F being PGraphMapping of G1,G2 holds

( rng ((H |` F) _V) = (rng (F _V)) /\ (the_Vertices_of H) & rng ((H |` F) _E) = (rng (F _E)) /\ (the_Edges_of H) ) by RELAT_1:88;

for H being Subgraph of G2

for F being PGraphMapping of G1,G2 holds

( rng ((H |` F) _V) = (rng (F _V)) /\ (the_Vertices_of H) & rng ((H |` F) _E) = (rng (F _E)) /\ (the_Edges_of H) ) by RELAT_1:88;

theorem :: GLIB_010:65

for G1, G2 being WGraph

for H being WSubgraph of G2

for F being PGraphMapping of G1,G2 st F is weight-preserving holds

H |` F is weight-preserving

for H being WSubgraph of G2

for F being PGraphMapping of G1,G2 st F is weight-preserving holds

H |` F is weight-preserving

proof end;

theorem :: GLIB_010:66

for G1, G2 being EGraph

for H being ESubgraph of G2

for F being PGraphMapping of G1,G2 st F is elabel-preserving holds

H |` F is elabel-preserving

for H being ESubgraph of G2

for F being PGraphMapping of G1,G2 st F is elabel-preserving holds

H |` F is elabel-preserving

proof end;

theorem :: GLIB_010:67

for G1, G2 being VGraph

for H being VSubgraph of G2

for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

H |` F is vlabel-preserving

for H being VSubgraph of G2

for F being PGraphMapping of G1,G2 st F is vlabel-preserving holds

H |` F is vlabel-preserving

proof end;

theorem :: GLIB_010:68

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for H1 being Subgraph of G1

for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

for F being PGraphMapping of G1,G2

for H1 being Subgraph of G1

for H2 being Subgraph of G2 holds (H2 |` F) | H1 = H2 |` (F | H1)

proof end;

:: define inverse of graph mappings

definition

let G1, G2 be _Graph;

let F be one-to-one PGraphMapping of G1,G2;

coherence

[((F _V) "),((F _E) ")] is PGraphMapping of G2,G1

end;
let F be one-to-one PGraphMapping of G1,G2;

coherence

[((F _V) "),((F _E) ")] is PGraphMapping of G2,G1

proof end;

:: deftheorem defines " GLIB_010:def 33 :

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 holds F " = [((F _V) "),((F _E) ")];

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 holds F " = [((F _V) "),((F _E) ")];

registration

let G1, G2 be _Graph;

let F be one-to-one PGraphMapping of G1,G2;

coherence

( F " is one-to-one & F " is semi-continuous )

end;
let F be one-to-one PGraphMapping of G1,G2;

coherence

( F " is one-to-one & F " is semi-continuous )

proof end;

registration

let G1, G2 be _Graph;

let F be empty one-to-one PGraphMapping of G1,G2;

coherence

F " is empty

end;
let F be empty one-to-one PGraphMapping of G1,G2;

coherence

F " is empty

proof end;

registration

let G1, G2 be _Graph;

let F be non empty one-to-one PGraphMapping of G1,G2;

coherence

not F " is empty

end;
let F be non empty one-to-one PGraphMapping of G1,G2;

coherence

not F " is empty

proof end;

registration

let G1, G2 be _Graph;

let F be one-to-one semi-Dcontinuous PGraphMapping of G1,G2;

coherence

F " is semi-Dcontinuous

end;
let F be one-to-one semi-Dcontinuous PGraphMapping of G1,G2;

coherence

F " is semi-Dcontinuous

proof end;

theorem :: GLIB_010:69

theorem Th71: :: GLIB_010:71

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 holds

( F is total iff F " is onto ) by FUNCT_1:33;

for F being one-to-one PGraphMapping of G1,G2 holds

( F is total iff F " is onto ) by FUNCT_1:33;

theorem Th72: :: GLIB_010:72

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 holds

( F is onto iff F " is total ) by FUNCT_1:33;

for F being one-to-one PGraphMapping of G1,G2 holds

( F is onto iff F " is total ) by FUNCT_1:33;

theorem :: GLIB_010:73

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 st F is total & F is continuous holds

F " is continuous

for F being one-to-one PGraphMapping of G1,G2 st F is total & F is continuous holds

F " is continuous

proof end;

theorem Th74: :: GLIB_010:74

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 st F is total & F is Dcontinuous holds

F " is Dcontinuous

for F being one-to-one PGraphMapping of G1,G2 st F is total & F is Dcontinuous holds

F " is Dcontinuous

proof end;

theorem Th75: :: GLIB_010:75

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 holds

( F is isomorphism iff F " is isomorphism ) by Th71, Th72;

for F being one-to-one PGraphMapping of G1,G2 holds

( F is isomorphism iff F " is isomorphism ) by Th71, Th72;

theorem :: GLIB_010:76

for G1, G2 being WGraph

for F being one-to-one PGraphMapping of G1,G2 holds

( F is weight-preserving iff F " is weight-preserving )

for F being one-to-one PGraphMapping of G1,G2 holds

( F is weight-preserving iff F " is weight-preserving )

proof end;

theorem :: GLIB_010:77

for G1, G2 being EGraph

for F being one-to-one PGraphMapping of G1,G2 holds

( F is elabel-preserving iff F " is elabel-preserving )

for F being one-to-one PGraphMapping of G1,G2 holds

( F is elabel-preserving iff F " is elabel-preserving )

proof end;

theorem :: GLIB_010:78

for G1, G2 being VGraph

for F being one-to-one PGraphMapping of G1,G2 holds

( F is vlabel-preserving iff F " is vlabel-preserving )

for F being one-to-one PGraphMapping of G1,G2 holds

( F is vlabel-preserving iff F " is vlabel-preserving )

proof end;

theorem Th81: :: GLIB_010:81

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2 holds

( dom F = rng (F ") & rng F = dom (F ") )

for F being non empty one-to-one PGraphMapping of G1,G2 holds

( dom F = rng (F ") & rng F = dom (F ") )

proof end;

theorem Th82: :: GLIB_010:82

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2

for H being Subgraph of G1 holds (F | H) " = H |` (F ")

for F being one-to-one PGraphMapping of G1,G2

for H being Subgraph of G1 holds (F | H) " = H |` (F ")

proof end;

theorem :: GLIB_010:83

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2

for H being Subgraph of G2 holds (H |` F) " = (F ") | H

for F being one-to-one PGraphMapping of G1,G2

for H being Subgraph of G2 holds (H |` F) " = (F ") | H

proof end;

:: properties derived by use of F"

theorem Th84: :: GLIB_010:84

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is isomorphism holds

( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

for F being PGraphMapping of G1,G2 st F is isomorphism holds

( G1 .order() = G2 .order() & G1 .size() = G2 .size() )

proof end;

theorem :: GLIB_010:85

for G1, G2 being _finite _Graph

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & ex F0 being PGraphMapping of G1,G2 st F0 is isomorphism holds

F is isomorphism

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & ex F0 being PGraphMapping of G1,G2 st F0 is isomorphism holds

F is isomorphism

proof end;

theorem :: GLIB_010:86

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))

for F being PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesBetween (X,Y)) = card (G2 .edgesBetween (((F _V) .: X),((F _V) .: Y)))

proof end;

theorem :: GLIB_010:87

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for X being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))

for F being PGraphMapping of G1,G2

for X being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesBetween X) = card (G2 .edgesBetween ((F _V) .: X))

proof end;

theorem :: GLIB_010:88

for G1, G2 being _Graph

for F being directed PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

for F being directed PGraphMapping of G1,G2

for X, Y being Subset of (the_Vertices_of G1) st F is isomorphism holds

card (G1 .edgesDBetween (X,Y)) = card (G2 .edgesDBetween (((F _V) .: X),((F _V) .: Y)))

proof end;

theorem :: GLIB_010:89

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is isomorphism holds

( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) )

for F being PGraphMapping of G1,G2 st F is isomorphism holds

( ( G1 is _trivial implies G2 is _trivial ) & ( G2 is _trivial implies G1 is _trivial ) & ( G1 is loopless implies G2 is loopless ) & ( G2 is loopless implies G1 is loopless ) & ( G1 is edgeless implies G2 is edgeless ) & ( G2 is edgeless implies G1 is edgeless ) & ( G1 is non-multi implies G2 is non-multi ) & ( G2 is non-multi implies G1 is non-multi ) & ( G1 is simple implies G2 is simple ) & ( G2 is simple implies G1 is simple ) & ( G1 is _finite implies G2 is _finite ) & ( G2 is _finite implies G1 is _finite ) & ( G1 is complete implies G2 is complete ) & ( G2 is complete implies G1 is complete ) )

proof end;

theorem :: GLIB_010:90

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is isomorphism holds

( ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G1 is Dsimple implies G2 is Dsimple ) & ( G2 is Dsimple implies G1 is Dsimple ) )

for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is isomorphism holds

( ( G1 is non-Dmulti implies G2 is non-Dmulti ) & ( G2 is non-Dmulti implies G1 is non-Dmulti ) & ( G1 is Dsimple implies G2 is Dsimple ) & ( G2 is Dsimple implies G1 is Dsimple ) )

proof end;

Lm4: for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) c= card ((rng F) .loops())

proof end;

theorem :: GLIB_010:91

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) = card ((rng F) .loops())

for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) = card ((rng F) .loops())

proof end;

theorem Th92: :: GLIB_010:92

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 st F is total holds

card (G1 .loops()) c= card (G2 .loops())

for F being one-to-one PGraphMapping of G1,G2 st F is total holds

card (G1 .loops()) c= card (G2 .loops())

proof end;

theorem Th93: :: GLIB_010:93

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 st F is onto holds

card (G2 .loops()) c= card (G1 .loops())

for F being one-to-one PGraphMapping of G1,G2 st F is onto holds

card (G2 .loops()) c= card (G1 .loops())

proof end;

theorem :: GLIB_010:94

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds

card (G1 .loops()) = card (G2 .loops())

for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds

card (G1 .loops()) = card (G2 .loops())

proof end;

theorem Th97: :: GLIB_010:97

for G1 being _Graph

for G2 being b_{1} -isomorphic _Graph

for G3 being b_{2} -isomorphic _Graph

for F being Isomorphism of G1,G2 st ex E being set st G3 is reverseEdgeDirections of G1,E holds

F " is Isomorphism of G2,G3

for G2 being b

for G3 being b

for F being Isomorphism of G1,G2 st ex E being set st G3 is reverseEdgeDirections of G1,E holds

F " is Isomorphism of G2,G3

proof end;

theorem :: GLIB_010:98

for G1 being _Graph

for G2 being b_{1} -isomorphic _Graph

for G3 being b_{2} -isomorphic _Graph

for F being Isomorphism of G1,G2 st G1 == G3 holds

F " is Isomorphism of G2,G3

for G2 being b

for G3 being b

for F being Isomorphism of G1,G2 st G1 == G3 holds

F " is Isomorphism of G2,G3

proof end;

theorem :: GLIB_010:99

for G1 being _Graph

for G2 being b_{1} -Disomorphic _Graph

for G3 being b_{2} -Disomorphic _Graph

for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

for G2 being b

for G3 being b

for F being DIsomorphism of G1,G2 st G1 == G3 holds

F " is DIsomorphism of G2,G3

proof end;

:: define composition of graph mappings

definition

let G1, G2, G3 be _Graph;

let F1 be PGraphMapping of G1,G2;

let F2 be PGraphMapping of G2,G3;

[((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))] is PGraphMapping of G1,G3

end;
let F1 be PGraphMapping of G1,G2;

let F2 be PGraphMapping of G2,G3;

func F2 * F1 -> PGraphMapping of G1,G3 equals :: GLIB_010:def 34

[((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))];

coherence [((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))];

[((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))] is PGraphMapping of G1,G3

proof end;

:: deftheorem defines * GLIB_010:def 34 :

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 holds F2 * F1 = [((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))];

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 holds F2 * F1 = [((F2 _V) * (F1 _V)),((F2 _E) * (F1 _E))];

theorem :: GLIB_010:100

theorem :: GLIB_010:101

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F2 * F1 is onto holds

F2 is onto

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F2 * F1 is onto holds

F2 is onto

proof end;

theorem :: GLIB_010:102

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds

F1 is total

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F2 * F1 is total holds

F1 is total

proof end;

registration

let G1, G2, G3 be _Graph;

let F1 be one-to-one PGraphMapping of G1,G2;

let F2 be one-to-one PGraphMapping of G2,G3;

coherence

F2 * F1 is one-to-one ;

end;
let F1 be one-to-one PGraphMapping of G1,G2;

let F2 be one-to-one PGraphMapping of G2,G3;

coherence

F2 * F1 is one-to-one ;

registration

let G1, G2, G3 be _Graph;

let F1 be semi-continuous PGraphMapping of G1,G2;

let F2 be semi-continuous PGraphMapping of G2,G3;

coherence

F2 * F1 is semi-continuous

end;
let F1 be semi-continuous PGraphMapping of G1,G2;

let F2 be semi-continuous PGraphMapping of G2,G3;

coherence

F2 * F1 is semi-continuous

proof end;

registration

let G1, G2, G3 be _Graph;

let F1 be continuous PGraphMapping of G1,G2;

let F2 be continuous PGraphMapping of G2,G3;

coherence

F2 * F1 is continuous

end;
let F1 be continuous PGraphMapping of G1,G2;

let F2 be continuous PGraphMapping of G2,G3;

coherence

F2 * F1 is continuous

proof end;

registration

let G1, G2, G3 be _Graph;

let F1 be directed PGraphMapping of G1,G2;

let F2 be directed PGraphMapping of G2,G3;

coherence

F2 * F1 is directed

end;
let F1 be directed PGraphMapping of G1,G2;

let F2 be directed PGraphMapping of G2,G3;

coherence

F2 * F1 is directed

proof end;

registration

let G1, G2, G3 be _Graph;

let F1 be semi-Dcontinuous PGraphMapping of G1,G2;

let F2 be semi-Dcontinuous PGraphMapping of G2,G3;

coherence

F2 * F1 is semi-Dcontinuous

end;
let F1 be semi-Dcontinuous PGraphMapping of G1,G2;

let F2 be semi-Dcontinuous PGraphMapping of G2,G3;

coherence

F2 * F1 is semi-Dcontinuous

proof end;

registration

let G1, G2, G3 be _Graph;

let F1 be Dcontinuous PGraphMapping of G1,G2;

let F2 be Dcontinuous PGraphMapping of G2,G3;

coherence

F2 * F1 is Dcontinuous

end;
let F1 be Dcontinuous PGraphMapping of G1,G2;

let F2 be Dcontinuous PGraphMapping of G2,G3;

coherence

F2 * F1 is Dcontinuous

proof end;

registration

let G1, G2, G3 be _Graph;

let F1 be empty PGraphMapping of G1,G2;

let F2 be PGraphMapping of G2,G3;

coherence

F2 * F1 is empty ;

end;
let F1 be empty PGraphMapping of G1,G2;

let F2 be PGraphMapping of G2,G3;

coherence

F2 * F1 is empty ;

registration

let G1, G2, G3 be _Graph;

let F1 be PGraphMapping of G1,G2;

let F2 be empty PGraphMapping of G2,G3;

coherence

F2 * F1 is empty ;

end;
let F1 be PGraphMapping of G1,G2;

let F2 be empty PGraphMapping of G2,G3;

coherence

F2 * F1 is empty ;

theorem Th104: :: GLIB_010:104

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is total & F2 is total holds

F2 * F1 is total

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is total & F2 is total holds

F2 * F1 is total

proof end;

theorem Th106: :: GLIB_010:106

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds

F2 * F1 is onto

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is onto & F2 is onto holds

F2 * F1 is onto

proof end;

theorem :: GLIB_010:107

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is weak_SG-embedding & F2 is weak_SG-embedding holds

F2 * F1 is weak_SG-embedding by Th104;

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is weak_SG-embedding & F2 is weak_SG-embedding holds

F2 * F1 is weak_SG-embedding by Th104;

theorem :: GLIB_010:108

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is strong_SG-embedding & F2 is strong_SG-embedding holds

F2 * F1 is strong_SG-embedding by Th104;

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is strong_SG-embedding & F2 is strong_SG-embedding holds

F2 * F1 is strong_SG-embedding by Th104;

theorem Th109: :: GLIB_010:109

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is isomorphism & F2 is isomorphism holds

F2 * F1 is isomorphism by Th104, Th106;

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is isomorphism & F2 is isomorphism holds

F2 * F1 is isomorphism by Th104, Th106;

theorem Th110: :: GLIB_010:110

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds

F2 * F1 is Disomorphism

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is Disomorphism & F2 is Disomorphism holds

F2 * F1 is Disomorphism

proof end;

theorem :: GLIB_010:111

for G1, G2, G3 being WGraph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is weight-preserving & F2 is weight-preserving holds

F2 * F1 is weight-preserving

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is weight-preserving & F2 is weight-preserving holds

F2 * F1 is weight-preserving

proof end;

theorem :: GLIB_010:112

for G1, G2, G3 being EGraph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is elabel-preserving & F2 is elabel-preserving holds

F2 * F1 is elabel-preserving

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is elabel-preserving & F2 is elabel-preserving holds

F2 * F1 is elabel-preserving

proof end;

theorem :: GLIB_010:113

for G1, G2, G3 being VGraph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds

F2 * F1 is vlabel-preserving

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3 st F1 is vlabel-preserving & F2 is vlabel-preserving holds

F2 * F1 is vlabel-preserving

proof end;

theorem :: GLIB_010:114

for G1, G2, G3, G4 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3

for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3

for F3 being PGraphMapping of G3,G4 holds F3 * (F2 * F1) = (F3 * F2) * F1

proof end;

theorem :: GLIB_010:115

for G1, G2 being _Graph

for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds

( F * (F ") = id G2 & (F ") * F = id G1 )

for F being one-to-one PGraphMapping of G1,G2 st F is isomorphism holds

( F * (F ") = id G2 & (F ") * F = id G1 )

proof end;

theorem :: GLIB_010:116

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 holds

( F * (id G1) = F & (id G2) * F = F )

for F being PGraphMapping of G1,G2 holds

( F * (id G1) = F & (id G2) * F = F )

proof end;

theorem :: GLIB_010:117

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3

for H being Subgraph of G1 holds F2 * (F1 | H) = (F2 * F1) | H

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3

for H being Subgraph of G1 holds F2 * (F1 | H) = (F2 * F1) | H

proof end;

theorem :: GLIB_010:118

for G1, G2, G3 being _Graph

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3

for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

for F1 being PGraphMapping of G1,G2

for F2 being PGraphMapping of G2,G3

for H being Subgraph of G3 holds (H |` F2) * F1 = H |` (F2 * F1)

proof end;

registration

let G1 be _Graph;

let G2 be G1 -isomorphic _Graph;

for b_{1} being _Graph st b_{1} is G2 -isomorphic holds

b_{1} is G1 -isomorphic

end;
let G2 be G1 -isomorphic _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] G2 -isomorphic -> G1 -isomorphic for set ;

coherence for b

b

proof end;

registration

let G1 be _Graph;

let G2 be G1 -Disomorphic _Graph;

for b_{1} being _Graph st b_{1} is G2 -Disomorphic holds

b_{1} is G1 -Disomorphic

end;
let G2 be G1 -Disomorphic _Graph;

cluster Relation-like NAT -defined Function-like finite [Graph-like] G2 -Disomorphic -> G1 -Disomorphic for set ;

coherence for b

b

proof end;

:: deftheorem Def35 defines -defined GLIB_010:def 35 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for W1 being Walk of G1 holds

( W1 is F -defined iff ( W1 .vertices() c= dom (F _V) & W1 .edges() c= dom (F _E) ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for W1 being Walk of G1 holds

( W1 is F -defined iff ( W1 .vertices() c= dom (F _V) & W1 .edges() c= dom (F _E) ) );

:: deftheorem Def36 defines -valued GLIB_010:def 36 :

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for W2 being Walk of G2 holds

( W2 is F -valued iff ( W2 .vertices() c= rng (F _V) & W2 .edges() c= rng (F _E) ) );

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for W2 being Walk of G2 holds

( W2 is F -valued iff ( W2 .vertices() c= rng (F _V) & W2 .edges() c= rng (F _E) ) );

registration

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

ex b_{1} being Walk of G1 st

( b_{1} is F -defined & b_{1} is V5() )

ex b_{1} being Walk of G2 st

( b_{1} is F -valued & b_{1} is V5() )

end;
let F be non empty PGraphMapping of G1,G2;

cluster V5() Relation-like NAT -defined (the_Vertices_of G1) \/ (the_Edges_of G1) -valued Function-like FinSequence-like F -defined for Walk of G1;

existence ex b

( b

proof end;

cluster V5() Relation-like NAT -defined (the_Vertices_of G2) \/ (the_Edges_of G2) -valued Function-like FinSequence-like F -valued for Walk of G2;

existence ex b

( b

proof end;

theorem :: GLIB_010:119

for G1, G2 being _Graph

for F being empty PGraphMapping of G1,G2

for W1 being Walk of G1 holds not W1 is F -defined by XBOOLE_1:3;

for F being empty PGraphMapping of G1,G2

for W1 being Walk of G1 holds not W1 is F -defined by XBOOLE_1:3;

theorem :: GLIB_010:120

for G1, G2 being _Graph

for F being empty PGraphMapping of G1,G2

for W2 being Walk of G2 holds not W2 is F -valued by XBOOLE_1:3;

for F being empty PGraphMapping of G1,G2

for W2 being Walk of G2 holds not W2 is F -valued by XBOOLE_1:3;

theorem Th121: :: GLIB_010:121

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for W1 being Walk of G1 st F is total holds

W1 is F -defined ;

for F being PGraphMapping of G1,G2

for W1 being Walk of G1 st F is total holds

W1 is F -defined ;

theorem Th122: :: GLIB_010:122

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2

for W2 being Walk of G2 st F is onto holds

W2 is F -valued ;

for F being PGraphMapping of G1,G2

for W2 being Walk of G2 st F is onto holds

W2 is F -valued ;

registration

let G1, G2 be _Graph;

let F be one-to-one PGraphMapping of G1,G2;

coherence

for b_{1} being Walk of G1 st b_{1} is F -defined holds

b_{1} is F " -valued
by FUNCT_1:33;

coherence

for b_{1} being Walk of G2 st b_{1} is F -valued holds

b_{1} is F " -defined
by FUNCT_1:33;

end;
let F be one-to-one PGraphMapping of G1,G2;

coherence

for b

b

coherence

for b

b

definition

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

let W1 be F -defined Walk of G1;

ex b_{1} being Walk of G2 st

( (F _V) * (W1 .vertexSeq()) = b_{1} .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b_{1} .edgeSeq() )

for b_{1}, b_{2} being Walk of G2 st (F _V) * (W1 .vertexSeq()) = b_{1} .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b_{1} .edgeSeq() & (F _V) * (W1 .vertexSeq()) = b_{2} .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b_{2} .edgeSeq() holds

b_{1} = b_{2}
by GLIB_009:26;

end;
let F be non empty PGraphMapping of G1,G2;

let W1 be F -defined Walk of G1;

func F .: W1 -> Walk of G2 means :Def37: :: GLIB_010:def 37

( (F _V) * (W1 .vertexSeq()) = it .vertexSeq() & (F _E) * (W1 .edgeSeq()) = it .edgeSeq() );

existence ( (F _V) * (W1 .vertexSeq()) = it .vertexSeq() & (F _E) * (W1 .edgeSeq()) = it .edgeSeq() );

ex b

( (F _V) * (W1 .vertexSeq()) = b

proof end;

uniqueness for b

b

:: deftheorem Def37 defines .: GLIB_010:def 37 :

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1

for b_{5} being Walk of G2 holds

( b_{5} = F .: W1 iff ( (F _V) * (W1 .vertexSeq()) = b_{5} .vertexSeq() & (F _E) * (W1 .edgeSeq()) = b_{5} .edgeSeq() ) );

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b

for b

( b

registration

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

let W1 be F -defined Walk of G1;

coherence

F .: W1 is F -valued

end;
let F be non empty PGraphMapping of G1,G2;

let W1 be F -defined Walk of G1;

coherence

F .: W1 is F -valued

proof end;

definition

let G1, G2 be _Graph;

let F be non empty PGraphMapping of G1,G2;

let W1 be F -defined Walk of G1;

:: original: .:

redefine func F .: W1 -> F -valued Walk of G2;

correctness

coherence

F .: W1 is F -valued Walk of G2;

;

end;
let F be non empty PGraphMapping of G1,G2;

let W1 be F -defined Walk of G1;

:: original: .:

redefine func F .: W1 -> F -valued Walk of G2;

correctness

coherence

F .: W1 is F -valued Walk of G2;

;

definition

let G1, G2 be _Graph;

let F be non empty one-to-one PGraphMapping of G1,G2;

let W2 be F -valued Walk of G2;

coherence

(F ") .: W2 is F -defined Walk of G1

end;
let F be non empty one-to-one PGraphMapping of G1,G2;

let W2 be F -valued Walk of G2;

coherence

(F ") .: W2 is F -defined Walk of G1

proof end;

:: deftheorem defines " GLIB_010:def 38 :

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b_{3} -valued Walk of G2 holds F " W2 = (F ") .: W2;

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

Lm5: for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

( (F _V) * ((F " W2) .vertexSeq()) = W2 .vertexSeq() & (F _E) * ((F " W2) .edgeSeq()) = W2 .edgeSeq() )

proof end;

definition

let G1, G2 be _Graph;

let F be non empty one-to-one PGraphMapping of G1,G2;

let W2 be F -valued Walk of G2;

for b_{1} being F -defined Walk of G1 holds

( b_{1} = F " W2 iff ( (F _V) * (b_{1} .vertexSeq()) = W2 .vertexSeq() & (F _E) * (b_{1} .edgeSeq()) = W2 .edgeSeq() ) )

end;
let F be non empty one-to-one PGraphMapping of G1,G2;

let W2 be F -valued Walk of G2;

redefine func F " W2 means :: GLIB_010:def 39

( (F _V) * (it .vertexSeq()) = W2 .vertexSeq() & (F _E) * (it .edgeSeq()) = W2 .edgeSeq() );

compatibility ( (F _V) * (it .vertexSeq()) = W2 .vertexSeq() & (F _E) * (it .edgeSeq()) = W2 .edgeSeq() );

for b

( b

proof end;

:: deftheorem defines " GLIB_010:def 39 :

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b_{3} -valued Walk of G2

for b_{5} being b_{3} -defined Walk of G1 holds

( b_{5} = F " W2 iff ( (F _V) * (b_{5} .vertexSeq()) = W2 .vertexSeq() & (F _E) * (b_{5} .edgeSeq()) = W2 .edgeSeq() ) );

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

for b

( b

theorem Th123: :: GLIB_010:123

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds F " (F .: W1) = W1

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b

proof end;

theorem :: GLIB_010:124

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b_{3} -valued Walk of G2 holds F .: (F " W2) = W2

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

proof end;

theorem Th125: :: GLIB_010:125

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds

( W1 .length() = (F .: W1) .length() & len W1 = len (F .: W1) )

for F being non empty PGraphMapping of G1,G2

for W1 being b

( W1 .length() = (F .: W1) .length() & len W1 = len (F .: W1) )

proof end;

theorem :: GLIB_010:126

theorem Th127: :: GLIB_010:127

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds

( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )

for F being non empty PGraphMapping of G1,G2

for W1 being b

( (F _V) . (W1 .first()) = (F .: W1) .first() & (F _V) . (W1 .last()) = (F .: W1) .last() )

proof end;

theorem :: GLIB_010:128

theorem Th129: :: GLIB_010:129

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1

for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

for F being non empty PGraphMapping of G1,G2

for W1 being b

for n being odd Element of NAT st n <= len W1 holds

(F _V) . (W1 . n) = (F .: W1) . n

proof end;

theorem :: GLIB_010:130

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1

for n being even Element of NAT st 1 <= n & n <= len W1 holds

(F _E) . (W1 . n) = (F .: W1) . n

for F being non empty PGraphMapping of G1,G2

for W1 being b

for n being even Element of NAT st 1 <= n & n <= len W1 holds

(F _E) . (W1 . n) = (F .: W1) . n

proof end;

theorem Th131: :: GLIB_010:131

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1

for v, w being object st W1 is_Walk_from v,w holds

( v in dom (F _V) & w in dom (F _V) )

for F being non empty PGraphMapping of G1,G2

for W1 being b

for v, w being object st W1 is_Walk_from v,w holds

( v in dom (F _V) & w in dom (F _V) )

proof end;

theorem Th132: :: GLIB_010:132

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1

for v, w being object st W1 is_Walk_from v,w holds

F .: W1 is_Walk_from (F _V) . v,(F _V) . w

for F being non empty PGraphMapping of G1,G2

for W1 being b

for v, w being object st W1 is_Walk_from v,w holds

F .: W1 is_Walk_from (F _V) . v,(F _V) . w

proof end;

theorem :: GLIB_010:133

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1

for v, w being object holds

( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) )

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b

for v, w being object holds

( W1 is_Walk_from v,w iff ( v in dom (F _V) & w in dom (F _V) & F .: W1 is_Walk_from (F _V) . v,(F _V) . w ) )

proof end;

theorem :: GLIB_010:134

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 st (F _V) . (W1 .first()) = (F _V) . (W1 .last()) holds

W1 .first() = W1 .last()

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b

W1 .first() = W1 .last()

proof end;

theorem :: GLIB_010:135

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds (F .: W1) .vertices() = (F _V) .: (W1 .vertices())

for F being non empty PGraphMapping of G1,G2

for W1 being b

proof end;

theorem Th136: :: GLIB_010:136

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds (F .: W1) .edges() = (F _E) .: (W1 .edges())

for F being non empty PGraphMapping of G1,G2

for W1 being b

proof end;

theorem Th137: :: GLIB_010:137

for G1, G2 being _Graph

for F being non empty PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds

( ( W1 is V5() implies F .: W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )

for F being non empty PGraphMapping of G1,G2

for W1 being b

( ( W1 is V5() implies F .: W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) )

proof end;

theorem Th138: :: GLIB_010:138

for G1, G2 being _Graph

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b_{3} -defined Walk of G1 holds

( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b

( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

proof end;

:: properties derived using walks

theorem Th139: :: GLIB_010:139

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is acyclic holds

G1 is acyclic

for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is acyclic holds

G1 is acyclic

proof end;

theorem :: GLIB_010:140

for G1, G2 being _Graph

for F being PGraphMapping of G1,G2 st F is isomorphism holds

( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )

for F being PGraphMapping of G1,G2 st F is isomorphism holds

( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )

proof end;

theorem Th141: :: GLIB_010:141

for G1, G2 being _Graph

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )

proof end;

theorem Th142: :: GLIB_010:142

for G1, G2 being _Graph

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2

for F0 being PGraphMapping of G1,G2 ex F being PGraphMapping of G3,G4 st

( F = F0 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

proof end;

theorem Th143: :: GLIB_010:143

for G1 being _Graph

for G2 being b_{1} -isomorphic _Graph

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

for G2 being b

for E1, E2 being set

for G3 being reverseEdgeDirections of G1,E1

for G4 being reverseEdgeDirections of G2,E2 holds G4 is G3 -isomorphic

proof end;

theorem Th144: :: GLIB_010:144

for G3, G4 being _Graph

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

proof end;

theorem Th145: :: GLIB_010:145

for G3, G4 being _Graph

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2

for F0 being PGraphMapping of G3,G4

for f being one-to-one Function st dom f = V1 \ (the_Vertices_of G3) & rng f = V2 \ (the_Vertices_of G4) holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* f),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

proof end;

theorem Th146: :: GLIB_010:146

for G3 being _Graph

for G4 being b_{1} -isomorphic _Graph

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds

G2 is G1 -isomorphic

for G4 being b

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds

G2 is G1 -isomorphic

proof end;

theorem Th147: :: GLIB_010:147

for G3 being _Graph

for G4 being b_{1} -Disomorphic _Graph

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds

G2 is G1 -Disomorphic

for G4 being b

for V1, V2 being set

for G1 being addVertices of G3,V1

for G2 being addVertices of G4,V2 st card (V1 \ (the_Vertices_of G3)) = card (V2 \ (the_Vertices_of G4)) holds

G2 is G1 -Disomorphic

proof end;

theorem Th148: :: GLIB_010:148

for G3, G4 being _Graph

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) & ( F0 is Dcontinuous implies F is Dcontinuous ) )

proof end;

theorem :: GLIB_010:149

for G3, G4 being _Graph

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2

for F0 being PGraphMapping of G3,G4 st not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),(F0 _E)] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

proof end;

theorem :: GLIB_010:150

for G3 being _Graph

for G4 being b_{1} -isomorphic _Graph

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

for G4 being b

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

proof end;

theorem :: GLIB_010:151

for G3 being _Graph

for G4 being b_{1} -Disomorphic _Graph

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -Disomorphic )

for G4 being b

for v1, v2 being object

for G1 being addVertex of G3,v1

for G2 being addVertex of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -Disomorphic )

proof end;

:: for F to be (semi-)continous, it is not enough for F0

:: to be (semi-)continuous. To see this, let G3 be the edgeless graph

:: with 2 vertices, G4 be the trivial edgeless graph, F0 the total PGM

:: from G3 to G4 and v1 <> v3. F0 is (semi-)continuous, but F is not,

:: since that would result in e2 Joins F_V.v1, F_V.v1, G2

:: (because F_V.v1 = F_V.v3), but not e1 Joins v1, v1, G1.

:: If v2 and v4 are additionally not isolated in rng F0, F would be

:: (semi-)continuous, but that theorem isn't proven here.

:: to be (semi-)continuous. To see this, let G3 be the edgeless graph

:: with 2 vertices, G4 be the trivial edgeless graph, F0 the total PGM

:: from G3 to G4 and v1 <> v3. F0 is (semi-)continuous, but F is not,

:: since that would result in e2 Joins F_V.v1, F_V.v1, G2

:: (because F_V.v1 = F_V.v3), but not e1 Joins v1, v1, G1.

:: If v2 and v4 are additionally not isolated in rng F0, F would be

:: (semi-)continuous, but that theorem isn't proven here.

theorem Th152: :: GLIB_010:152

for G3, G4 being _Graph

for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) )

for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) )

proof end;

theorem :: GLIB_010:153

for G3, G4 being _Graph

for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & ( ( (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 ) or ( (F0 _V) . v1 = v4 & (F0 _V) . v3 = v2 ) ) holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

proof end;

:: For (semi-)Dcontinuous, the same remarks as above apply.

theorem Th154: :: GLIB_010:154

for G3, G4 being _Graph

for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )

for v1, v3 being Vertex of G3

for v2, v4 being Vertex of G4

for e1, e2 being object

for G1 being addEdge of G3,v1,e1,v3

for G2 being addEdge of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & v1 in dom (F0 _V) & v3 in dom (F0 _V) & (F0 _V) . v1 = v2 & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [(F0 _V),((F0 _E) +* (e1 .--> e2))] & ( F0 is directed implies F is directed ) & ( F0 is Disomorphism implies F is Disomorphism ) )

proof end;

:: Similar to addEdge, the (semi-)(D)continuous properties are not

:: always carried over from F0 to F due to possible isolated vertices.

:: always carried over from F0 to F due to possible isolated vertices.

theorem Th155: :: GLIB_010:155

for G3, G4 being _Graph

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v1,e1,v3

for G2 being addAdjVertex of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v1,e1,v3

for G2 being addAdjVertex of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

proof end;

theorem :: GLIB_010:156

for G3, G4 being _Graph

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v1,e1,v3

for G2 being addAdjVertex of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v1,e1,v3

for G2 being addAdjVertex of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

proof end;

theorem Th157: :: GLIB_010:157

for G3, G4 being _Graph

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is directed implies F is directed ) )

proof end;

theorem :: GLIB_010:158

for G3, G4 being _Graph

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

proof end;

theorem :: GLIB_010:159

for G3, G4 being _Graph

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v1,e1,v3

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v1,e1,v3

for G2 being addAdjVertex of G4,v4,e2,v2

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

proof end;

theorem :: GLIB_010:160

for G3, G4 being _Graph

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

for v3 being Vertex of G3

for v4 being Vertex of G4

for e1, e2, v1, v2 being object

for G1 being addAdjVertex of G3,v3,e1,v1

for G2 being addAdjVertex of G4,v2,e2,v4

for F0 being PGraphMapping of G3,G4 st not e1 in the_Edges_of G3 & not e2 in the_Edges_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & v3 in dom (F0 _V) & (F0 _V) . v3 = v4 holds

ex F being PGraphMapping of G1,G2 st

( F = [((F0 _V) +* (v1 .--> v2)),((F0 _E) +* (e1 .--> e2))] & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

proof end;

theorem :: GLIB_010:161

for G being _Graph

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V holds G2 is G1 -isomorphic

for v being object

for V being set

for G1, G2 being addAdjVertexAll of G,v,V holds G2 is G1 -isomorphic

proof end;

theorem Th162: :: GLIB_010:162

for G3, G4 being _Graph

for v1, v2 being object

for V1, V2 being set

for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

for v1, v2 being object

for V1, V2 being set

for G1 being addAdjVertexAll of G3,v1,V1

for G2 being addAdjVertexAll of G4,v2,V2

for F0 being PGraphMapping of G3,G4 st V1 c= the_Vertices_of G3 & V2 c= the_Vertices_of G4 & not v1 in the_Vertices_of G3 & not v2 in the_Vertices_of G4 & (F0 _V) | V1 is one-to-one & dom ((F0 _V) | V1) = V1 & rng ((F0 _V) | V1) = V2 holds

ex F being PGraphMapping of G1,G2 st

( F _V = (F0 _V) +* (v1 .--> v2) & (F _E) | (dom (F0 _E)) = F0 _E & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )

proof end;

theorem :: GLIB_010:163

for G3 being _Graph

for G4 being b_{1} -isomorphic _Graph

for v1, v2 being object

for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

for G4 being b

for v1, v2 being object

for G1 being addAdjVertexAll of G3,v1

for G2 being addAdjVertexAll of G4,v2 holds

not ( ( v1 in the_Vertices_of G3 implies v2 in the_Vertices_of G4 ) & ( v2 in the_Vertices_of G4 implies v1 in the_Vertices_of G3 ) & not G2 is G1 -isomorphic )

proof end;

theorem Th164: :: GLIB_010:164

for G1, G2 being _Graph

for G3 being removeLoops of G1

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

for G3 being removeLoops of G1

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is total implies F is total ) & ( F0 is onto implies F is onto ) & ( F0 is directed implies F is directed ) & ( F0 is semi-Dcontinuous implies F is semi-Dcontinuous ) )

proof end;

theorem Th165: :: GLIB_010:165

for G1, G2 being _Graph

for G3 being removeLoops of G1

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

for G3 being removeLoops of G1

for G4 being removeLoops of G2

for F0 being one-to-one PGraphMapping of G1,G2 ex F being one-to-one PGraphMapping of G3,G4 st

( F = F0 | G3 & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) & ( F0 is Disomorphism implies F is Disomorphism ) )

proof end;

theorem Th166: :: GLIB_010:166

for G1 being _Graph

for G2 being b_{1} -isomorphic _Graph

for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -isomorphic

for G2 being b

for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -isomorphic

proof end;

theorem Th167: :: GLIB_010:167

for G1 being _Graph

for G2 being b_{1} -Disomorphic _Graph

for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

for G2 being b

for G3 being removeLoops of G1

for G4 being removeLoops of G2 holds G4 is G3 -Disomorphic

proof end;

theorem Th168: :: GLIB_010:168

for G1 being _Graph

for G2 being b_{1} -isomorphic _Graph

for G3 being removeParallelEdges of G1

for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

for G2 being b

for G3 being removeParallelEdges of G1

for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

proof end;

theorem Th170: :: GLIB_010:170

for G1 being _Graph

for G2 being b_{1} -Disomorphic _Graph

for G3 being removeDParallelEdges of G1

for G4 being removeDParallelEdges of G2 holds G4 is G3 -Disomorphic

for G2 being b

for G3 being removeDParallelEdges of G1

for G4 being removeDParallelEdges of G2 holds G4 is G3 -Disomorphic

proof end;

theorem Th172: :: GLIB_010:172

for G1 being _Graph

for G2 being b_{1} -isomorphic _Graph

for G3 being SimpleGraph of G1

for G4 being SimpleGraph of G2 holds G4 is G3 -isomorphic

for G2 being b

for G3 being SimpleGraph of G1

for G4 being SimpleGraph of G2 holds G4 is G3 -isomorphic

proof end;

theorem Th174: :: GLIB_010:174

for G1 being _Graph

for G2 being b_{1} -Disomorphic _Graph

for G3 being DSimpleGraph of G1

for G4 being DSimpleGraph of G2 holds G4 is G3 -Disomorphic

for G2 being b

for G3 being DSimpleGraph of G1

for G4 being DSimpleGraph of G2 holds G4 is G3 -Disomorphic

proof end;

theorem :: GLIB_010:176

for G1, G2 being loopless _trivial _Graph

for F being non empty PGraphMapping of G1,G2 holds

( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )

for F being non empty PGraphMapping of G1,G2 holds

( F is Disomorphism & F = [( the Vertex of G1 .--> the Vertex of G2),{}] )

proof end;

theorem :: GLIB_010:177

for G1, G2 being _trivial _Graph st G1 .size() = G2 .size() holds

ex F being PGraphMapping of G1,G2 st F is Disomorphism

ex F being PGraphMapping of G1,G2 st F is Disomorphism

proof end;

:: sadly, the attribute notation is not compatible with the following notation

::registration

:: let G be trivial loopless _Graph;

:: cluster trivial loopless -> G-Disomorphic for _Graph;

:: coherence;

::end;

:: but normal theorems will do

:: Right Now, this is the only class of graphs that can

:: solely be determined by its attributes. More will come in the future.

::registration

:: let G be trivial loopless _Graph;

:: cluster trivial loopless -> G-Disomorphic for _Graph;

:: coherence;

::end;

:: but normal theorems will do

:: Right Now, this is the only class of graphs that can

:: solely be determined by its attributes. More will come in the future.