:: About Graph Mappings
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI,
ARYTM_3, CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PBOOLE, PARTFUN1,
FINSET_1, ZFMISC_1, RELAT_2, GLIB_002, FUNCOP_1, GLIB_001, ABIAN,
AOFA_I00, FACIRC_1, MCART_1, FUNCT_2, GLIB_003, GLIB_009, MOD_4, INT_1,
WAYBEL_0, RCOMP_1, MSAFREE2, RING_3, GLIB_006, GLIB_007, FUNCT_4,
ORDINAL2, CHORD, CARD_2, SCMYCIEL, SGRAPH1, REWRITE1, GLIB_010;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1,
SETWISEO, EQREL_1, FUNCOP_1, FUNCT_4, PARTFUN2, FINSET_1, CARD_1, PBOOLE,
CARD_2, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1,
VALUED_0, NAT_D, FINSEQ_1, BSPACE, FINSEQ_4, ABIAN, GLIB_000, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_2, GROUP_6, GLIB_001, GLIB_002, GLIB_003,
AOFA_I00, CHORD, GLIB_006, GLIB_007, GLIB_008, GLIB_009, FUNCT_7;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1,
GLIB_008, FUNCT_7, GLIB_009;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, GLIB_000, GLIB_002, GLIB_003, INT_1, CARD_1, RELSET_1,
XTUPLE_0, GLIB_001, ABIAN, GLIB_006, GLIB_008, NECKLACE, FUNCT_7,
GLIB_009;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: Preliminaries
:: into FUNCT_1 ?
theorem :: GLIB_010:1
for A,B,C,D being Function st D*A = C|dom A
holds (D|dom B)*A = C|dom(B*A);
:: into FUNCT_1 ?
theorem :: GLIB_010:2
for A being one-to-one Function, C,D being Function st D*A = C|dom A
holds C*(A") = D|dom(A");
:: BEGIN into GLIB_003 ?
registration
let G be non _finite _Graph, X be set;
cluster G.set(WeightSelector, X) -> non _finite;
cluster G.set(ELabelSelector, X) -> non _finite;
cluster G.set(VLabelSelector, X) -> non _finite;
end;
registration
let G be non loopless _Graph, X be set;
cluster G.set(WeightSelector, X) -> non loopless;
cluster G.set(ELabelSelector, X) -> non loopless;
cluster G.set(VLabelSelector, X) -> non loopless;
end;
registration
let G be non non-multi _Graph, X be set;
cluster G.set(WeightSelector, X) -> non non-multi;
cluster G.set(ELabelSelector, X) -> non non-multi;
cluster G.set(VLabelSelector, X) -> non non-multi;
end;
registration
let G be non non-Dmulti _Graph, X be set;
cluster G.set(WeightSelector, X) -> non non-Dmulti;
cluster G.set(ELabelSelector, X) -> non non-Dmulti;
cluster G.set(VLabelSelector, X) -> non non-Dmulti;
end;
registration
let G be non connected _Graph, X be set;
cluster G.set(WeightSelector, X) -> non connected;
cluster G.set(ELabelSelector, X) -> non connected;
cluster G.set(VLabelSelector, X) -> non connected;
end;
registration
let G be non acyclic _Graph, X be set;
cluster G.set(WeightSelector, X) -> non acyclic;
cluster G.set(ELabelSelector, X) -> non acyclic;
cluster G.set(VLabelSelector, X) -> non acyclic;
end;
definition
let G be _Graph;
attr G is elabel-full means
:: GLIB_010:def 1
ELabelSelector in dom G &
ex f being ManySortedSet of the_Edges_of G st G.ELabelSelector = f;
attr G is vlabel-full means
:: GLIB_010:def 2
VLabelSelector in dom G &
ex f being ManySortedSet of the_Vertices_of G st G.VLabelSelector = f;
end;
registration
cluster elabel-full -> [ELabeled] for _Graph;
cluster vlabel-full -> [VLabeled] for _Graph;
end;
definition
let G be EGraph;
attr G is elabel-distinct means
:: GLIB_010:def 3
the_ELabel_of G is one-to-one;
end;
definition
let G be VGraph;
attr G is vlabel-distinct means
:: GLIB_010:def 4
the_VLabel_of G is one-to-one;
end;
registration
let G be _Graph;
cluster G.set(ELabelSelector, id the_Edges_of G) -> elabel-full
elabel-distinct;
cluster G.set(VLabelSelector, id the_Vertices_of G) -> vlabel-full
vlabel-distinct;
end;
registration
cluster elabel-distinct elabel-full for EGraph;
cluster vlabel-distinct vlabel-full for VGraph;
end;
definition
let G be elabel-full _Graph;
redefine func the_ELabel_of G -> ManySortedSet of the_Edges_of G;
end;
definition
let G be vlabel-full _Graph;
redefine func the_VLabel_of G -> ManySortedSet of the_Vertices_of G;
end;
registration
let G be elabel-distinct EGraph;
cluster the_ELabel_of G -> one-to-one;
end;
registration
let G be vlabel-distinct VGraph;
cluster the_VLabel_of G -> one-to-one;
end;
registration
let G be elabel-full _Graph, X be set;
cluster G.set(WeightSelector, X) -> elabel-full;
cluster G.set(VLabelSelector, X) -> elabel-full;
end;
registration
let G be vlabel-full _Graph, X be set;
cluster G.set(WeightSelector, X) -> vlabel-full;
cluster G.set(ELabelSelector, X) -> vlabel-full;
end;
registration
let G be elabel-distinct EGraph, X be set;
cluster G.set(WeightSelector, X) -> elabel-distinct;
cluster G.set(VLabelSelector, X) -> elabel-distinct;
end;
registration
let G be vlabel-distinct VGraph, X be set;
cluster G.set(WeightSelector, X) -> vlabel-distinct;
cluster G.set(ELabelSelector, X) -> vlabel-distinct;
end;
registration
cluster elabel-full elabel-distinct vlabel-full vlabel-distinct for EVGraph;
end;
:: END into GLIB_003 ?
registration
let G1 be WGraph, E be set, G2 be reverseEdgeDirections of G1, E;
cluster G2.set(WeightSelector, the_Weight_of G1) -> [Weighted];
end;
registration
let G1 be EGraph, E be set, G2 be reverseEdgeDirections of G1, E;
cluster G2.set(ELabelSelector, the_ELabel_of G1) -> [ELabeled];
end;
registration
let G1 be VGraph, V be set, G2 be reverseEdgeDirections of G1, V;
cluster G2.set(VLabelSelector, the_VLabel_of G1) -> [VLabeled];
end;
registration
let G1 be elabel-full _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
cluster G2.set(ELabelSelector, the_ELabel_of G1) -> elabel-full;
end;
registration
let G1 be vlabel-full _Graph, V be set, G2 be reverseEdgeDirections of G1, V;
cluster G2.set(VLabelSelector, the_VLabel_of G1) -> vlabel-full;
end;
registration
let G1 be elabel-distinct EGraph, E be set;
let G2 be reverseEdgeDirections of G1, E;
cluster G2.set(ELabelSelector, the_ELabel_of G1) -> elabel-distinct;
end;
registration
let G1 be vlabel-distinct VGraph, E be set;
let G2 be reverseEdgeDirections of G1, E;
cluster G2.set(VLabelSelector, the_VLabel_of G1) -> vlabel-distinct;
end;
begin :: Ordering of a Graph
definition
func OrderingSelector -> Element of NAT equals
:: GLIB_010:def 5
8;
end;
definition
let G be GraphStruct;
attr G is [Ordered] means
:: GLIB_010:def 6
OrderingSelector in dom G & G.OrderingSelector
is Enumeration of the_Vertices_of G;
end;
registration
let G be _Graph, X be set;
cluster G.set(OrderingSelector, X) -> [Graph-like];
end;
registration
let G be _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non plain;
end;
registration
let G be WGraph, X be set;
cluster G.set(OrderingSelector, X) -> [Weighted];
end;
registration
let G be EGraph, X be set;
cluster G.set(OrderingSelector, X) -> [ELabeled];
end;
registration
let G be VGraph, X be set;
cluster G.set(OrderingSelector, X) -> [VLabeled];
end;
registration
let G be _Graph, X be Enumeration of the_Vertices_of G;
cluster G.set(OrderingSelector, X) -> [Ordered];
end;
registration
cluster [Graph-like] [Weighted] [ELabeled] [VLabeled] [Ordered]
for GraphStruct;
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
definition
let G be [Ordered] _Graph;
func the_Ordering_of G -> Enumeration of the_Vertices_of G equals
:: GLIB_010:def 7
G.OrderingSelector;
end;
theorem :: GLIB_010:3
for G being _Graph, X being set holds G == G.set(OrderingSelector, X);
registration
let G be elabel-full _Graph, X be set;
cluster G.set(OrderingSelector, X) -> elabel-full;
end;
registration
let G be vlabel-full _Graph, X be set;
cluster G.set(OrderingSelector, X) -> vlabel-full;
end;
registration
let G be elabel-distinct EGraph, X be set;
cluster G.set(OrderingSelector, X) -> elabel-distinct;
end;
registration
let G be vlabel-distinct VGraph, X be set;
cluster G.set(OrderingSelector, X) -> vlabel-distinct;
end;
registration
let G be _finite _Graph, X be set;
cluster G.set(OrderingSelector, X) -> _finite;
end;
registration
let G be non _finite _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non _finite;
end;
registration
let G be loopless _Graph, X be set;
cluster G.set(OrderingSelector, X) -> loopless;
end;
registration
let G be non loopless _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non loopless;
end;
registration
let G be _trivial _Graph, X be set;
cluster G.set(OrderingSelector, X) -> _trivial;
end;
registration
let G be non _trivial _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non _trivial;
end;
registration
let G be non-multi _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non-multi;
end;
registration
let G be non non-multi _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non non-multi;
end;
registration
let G be non-Dmulti _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non-Dmulti;
end;
registration
let G be non non-Dmulti _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non non-Dmulti;
end;
registration
let G be connected _Graph, X be set;
cluster G.set(OrderingSelector, X) -> connected;
end;
registration
let G be non connected _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non connected;
end;
registration
let G be acyclic _Graph, X be set;
cluster G.set(OrderingSelector, X) -> acyclic;
end;
registration
let G be non acyclic _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non acyclic;
end;
registration
let G be edgeless _Graph, X be set;
cluster G.set(OrderingSelector, X) -> edgeless;
end;
registration
let G be non edgeless _Graph, X be set;
cluster G.set(OrderingSelector, X) -> non edgeless;
end;
registration
let G be [Ordered] _Graph, X be set;
cluster G.set(WeightSelector, X) -> [Ordered];
cluster G.set(ELabelSelector, X) -> [Ordered];
cluster G.set(VLabelSelector, X) -> [Ordered];
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.
registration
let G1 be [Ordered] _Graph, G2 be spanning Subgraph of G1;
cluster G2.set(OrderingSelector, the_Ordering_of G1) -> [Ordered];
end;
registration
let G1 be [Ordered] _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
cluster G2.set(OrderingSelector, the_Ordering_of G1) -> [Ordered];
end;
begin
definition
let G1, G2 be _Graph;
mode PGraphMapping of G1, G2 means
:: GLIB_010:def 8 :: P is short for "partial"
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 holds e in dom g implies
(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 implies g.e Joins f.v,f.w,G2;
end;
registration
let G1, G2 be _Graph;
cluster -> pair for PGraphMapping of G1, G2;
end;
notation
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
synonym F_V for F`1;
synonym F_E for F`2;
end;
registration
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
reduce [ F_V , F_E ] to F;
end;
registration
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
cluster F_V -> Function-like Relation-like for set;
cluster F_E -> Function-like Relation-like for set;
end;
registration
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
cluster F_V -> the_Vertices_of G1-defined the_Vertices_of G2-valued
for Function;
cluster F_E -> the_Edges_of G1-defined the_Edges_of G2-valued
for Function;
end;
definition
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
redefine func F_V -> PartFunc of the_Vertices_of G1, the_Vertices_of G2;
redefine func F_E -> PartFunc of the_Edges_of G1, the_Edges_of G2;
end;
theorem :: GLIB_010:4
for G1, G2 being _Graph, 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
holds e Joins v,w,G1 implies F_E.e Joins F_V.v, F_V.w, G2;
theorem :: GLIB_010:5
for G1, G2 being _Graph, 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;
theorem :: GLIB_010:6
for G1, G2 being _Graph, 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;
theorem :: GLIB_010:7
for G1, G2 being _Graph, 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);
theorem :: 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 holds e in dom g implies
(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 implies g.e Joins f.v,f.w,G2)
holds [f,g] is PGraphMapping of G1, G2;
theorem :: GLIB_010:9
for G1, G2, G3, G4 being _Graph, F being PGraphMapping of G1, G2
st G1 == G3 & G2 == G4 holds F is PGraphMapping of G3, G4;
theorem :: GLIB_010:10
for G1, G2, G3, G4 being _Graph, 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;
definition
let G be _Graph;
func id G -> PGraphMapping of G, G equals
:: GLIB_010:def 9
[id the_Vertices_of G, id the_Edges_of G];
end;
theorem :: GLIB_010:11
for G1, G2 being _Graph st G1 == G2
holds id G1 = id G2 & id G1 is PGraphMapping of G1, G2;
theorem :: GLIB_010:12
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds id G1 = id G2 & id G1 is PGraphMapping of G1, G2;
definition
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
attr F is empty means
:: GLIB_010:def 10
dom F_V is empty;
attr F is total means
:: GLIB_010:def 11 :: this is the basic homomorphism definition
dom F_V = the_Vertices_of G1 & dom F_E = the_Edges_of G1;
attr F is onto means
:: GLIB_010:def 12
rng F_V = the_Vertices_of G2 & rng F_E = the_Edges_of G2;
attr F is one-to-one means
:: GLIB_010:def 13
F_V is one-to-one & F_E is one-to-one;
attr F is directed means
:: 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
holds e DJoins v,w,G1 implies F_E.e DJoins F_V.v, F_V.w, G2;
attr F is semi-continuous means
:: 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
holds F_E.e Joins F_V.v, F_V.w, G2 implies e Joins v,w,G1;
attr F is continuous means
:: 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
ex e being object st e Joins v,w,G1 & e in dom F_E & F_E.e = e9;
attr F is semi-Dcontinuous means
:: GLIB_010:def 17
for e,v,w being object st e in dom F_E & v in dom F_V & w in dom F_V
holds F_E.e DJoins F_V.v, F_V.w, G2 implies e DJoins v,w,G1;
attr F is Dcontinuous means
:: GLIB_010:def 18
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
ex e being object st e DJoins v,w,G1 & e in dom F_E & F_E.e = e9;
end;
:: at first properties of these attributes for the PGM are studied
:: regardless of the kinds of graph involved
theorem :: GLIB_010:13
for G1, G2 being _Graph, 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);
:: |dom F_E is probably not required, as the PGM property
:: enforces such a relationship between F_V and F_E
theorem :: GLIB_010:14
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:15
for G1, G2 being _Graph, 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
holds e Joins v,w,G1 iff F_E.e Joins F_V.v, F_V.w, G2;
theorem :: GLIB_010:16
for G1, G2 being _Graph, 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;
registration
let G1, G2 be _Graph;
cluster empty one-to-one Dcontinuous directed continuous
semi-Dcontinuous semi-continuous for PGraphMapping of G1, G2;
cluster non empty one-to-one directed semi-Dcontinuous semi-continuous
for PGraphMapping of G1, G2;
end;
registration
let G1, G2 be _Graph, F be empty PGraphMapping of G1, G2;
cluster F_V -> empty for set;
cluster F_E -> empty for set;
end;
registration
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
cluster F_V -> non empty for set;
end;
registration
let G1, G2 be _Graph, F be one-to-one PGraphMapping of G1, G2;
cluster F_V -> one-to-one for Function;
cluster F_E -> one-to-one for Function;
end;
theorem :: GLIB_010:17
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F_V is one-to-one holds F is semi-continuous;
theorem :: GLIB_010:18
for G1, G2 being _Graph, F being directed PGraphMapping of G1, G2
st F_V is one-to-one holds F is semi-Dcontinuous;
theorem :: GLIB_010:19
for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2
st rng F_E = the_Edges_of G2 holds F is continuous;
theorem :: GLIB_010:20
for G1, G2 being _Graph, F being semi-Dcontinuous PGraphMapping of G1, G2
st rng F_E = the_Edges_of G2 holds F is Dcontinuous;
theorem :: GLIB_010:21
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F_V is one-to-one & rng F_E = the_Edges_of G2 holds F is continuous;
theorem :: GLIB_010:22
for G1, G2 being _Graph, 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;
theorem :: GLIB_010:23
for G1, G2 being _Graph, F being continuous PGraphMapping of G1, G2
st F_E is one-to-one holds F is semi-continuous;
theorem :: GLIB_010:24
for G1, G2 being _Graph, F being Dcontinuous PGraphMapping of G1, G2
st F_E is one-to-one holds F is semi-Dcontinuous;
theorem :: GLIB_010:25
for G1, G2 being _Graph, F being Dcontinuous PGraphMapping of G1, G2
st F_E is one-to-one holds F is directed;
theorem :: GLIB_010:26
for G1, G2 being _Graph
for F being semi-continuous PGraphMapping of G1, G2, 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;
:: a special case of the following theorem is when G2 is without isolated
:: 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;
theorem :: GLIB_010:28
for G1, G2 being _Graph
for F being semi-Dcontinuous PGraphMapping of G1, G2, 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;
:: again, a special case of the following theorem is when G2 is without
:: 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;
registration
let G1, G2 be _Graph;
cluster one-to-one -> semi-continuous for PGraphMapping of G1, G2;
cluster one-to-one directed -> semi-Dcontinuous for PGraphMapping of G1, G2;
cluster one-to-one onto -> continuous for PGraphMapping of G1, G2;
cluster directed one-to-one onto -> Dcontinuous for PGraphMapping of G1, G2;
cluster semi-continuous onto -> continuous for PGraphMapping of G1, G2;
cluster semi-Dcontinuous -> directed semi-continuous
for PGraphMapping of G1, G2;
cluster semi-Dcontinuous onto -> Dcontinuous for PGraphMapping of G1, G2;
cluster Dcontinuous -> continuous for PGraphMapping of G1, G2;
cluster Dcontinuous one-to-one -> directed semi-Dcontinuous
for PGraphMapping of G1, G2;
cluster empty -> one-to-one Dcontinuous directed continuous
for PGraphMapping of G1, G2;
cluster total -> non empty for PGraphMapping of G1, G2;
cluster onto -> non empty for PGraphMapping of G1, G2;
end;
registration
let G be _Graph;
cluster id G -> total non empty onto one-to-one Dcontinuous;
end;
theorem :: 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 holds e in dom g implies
(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 implies g.e DJoins f.v,f.w,G2)
holds [f,g] is directed PGraphMapping of G1, G2;
theorem :: 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 holds e in dom g implies
(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;
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 holds e in dom g implies
(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;
theorem :: GLIB_010:33
for G1, G2 being _Graph
holds [{},{}] is empty one-to-one Dcontinuous PGraphMapping of G1, G2;
theorem :: GLIB_010:34
for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is total
for v being Vertex of G1 holds F_V.v is Vertex of G2;
theorem :: GLIB_010:35
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:36
for G1, G2 being _Graph, F being continuous PGraphMapping of G1, G2
st rng F_V = the_Vertices_of G2 holds G1 is loopless implies G2 is loopless;
theorem :: GLIB_010:37
for G1, G2 being _Graph, F being semi-continuous PGraphMapping of G1, G2
st F is onto holds G1 is loopless implies G2 is loopless;
theorem :: GLIB_010:38
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st rng F_E = the_Edges_of G2 holds G1 is edgeless implies G2 is edgeless;
theorem :: GLIB_010:39
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto holds G1 is edgeless implies G2 is edgeless;
:: next properties of these attributes for the PGM are studied
:: when G1 or G2 has a certain property
theorem :: GLIB_010:40
for G1 being _Graph, 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;
theorem :: GLIB_010:41
for G1 being _Graph, 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;
theorem :: GLIB_010:42
for G1 being non-multi _Graph, G2 being _Graph
for F being semi-continuous PGraphMapping of G1, G2
holds F_E is one-to-one;
theorem :: GLIB_010:43
for G1 being non-multi _Graph, G2 being _Graph
for F being PGraphMapping of G1, G2
st F_V is one-to-one holds F_E is one-to-one;
theorem :: GLIB_010:44
for G1 being non-Dmulti _Graph, G2 be _Graph
for F being directed PGraphMapping of G1, G2
st F_V is one-to-one holds F_E is one-to-one;
registration
let G1 be _Graph, G2 be loopless _Graph;
cluster directed semi-continuous -> semi-Dcontinuous
for PGraphMapping of G1, G2;
cluster directed continuous -> Dcontinuous for PGraphMapping of G1, G2;
end;
registration
let G1 be _trivial _Graph, G2 be _Graph;
cluster -> directed for PGraphMapping of G1, G2;
cluster semi-continuous -> semi-Dcontinuous for PGraphMapping of G1, G2;
cluster continuous -> Dcontinuous for PGraphMapping of G1, G2;
end;
registration
let G1 be _trivial non-Dmulti _Graph, G2 be _Graph;
cluster -> one-to-one for PGraphMapping of G1, G2;
end;
registration
let G1 be _trivial edgeless _Graph, G2 be _Graph;
cluster non empty -> total for PGraphMapping of G1, G2;
end;
registration
let G1 be _Graph, G2 be _trivial edgeless _Graph;
cluster non empty -> onto for PGraphMapping of G1, G2;
cluster -> semi-continuous continuous for PGraphMapping of G1, G2;
end;
:: define the concept of subgraph embedding and isomorphism
definition
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
attr F is weak_SG-embedding means
:: GLIB_010:def 19 :: SG is short for subgraph
F is total one-to-one;
attr F is strong_SG-embedding means
:: GLIB_010:def 20
F is total one-to-one continuous;
attr F is isomorphism means
:: GLIB_010:def 21
F is total one-to-one onto;
:: 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.
attr F is Disomorphism means
:: GLIB_010:def 22
F is directed total one-to-one onto;
end;
registration
let G1, G2 be _Graph;
cluster weak_SG-embedding -> total non empty one-to-one semi-continuous
for PGraphMapping of G1, G2;
cluster total one-to-one -> weak_SG-embedding for PGraphMapping of G1, G2;
cluster strong_SG-embedding -> total non empty one-to-one continuous
weak_SG-embedding for PGraphMapping of G1, G2;
cluster total one-to-one continuous -> strong_SG-embedding
for PGraphMapping of G1, G2;
cluster weak_SG-embedding continuous -> strong_SG-embedding
for PGraphMapping of G1, G2;
cluster isomorphism -> onto semi-continuous continuous total non empty
one-to-one weak_SG-embedding strong_SG-embedding
for PGraphMapping of G1, G2;
cluster total one-to-one onto continuous -> isomorphism
for PGraphMapping of G1, G2;
cluster strong_SG-embedding onto -> isomorphism for PGraphMapping of G1, G2;
cluster weak_SG-embedding continuous onto -> isomorphism
for PGraphMapping of G1, G2;
cluster Disomorphism -> directed isomorphism continuous total non empty
semi-Dcontinuous semi-continuous one-to-one weak_SG-embedding
strong_SG-embedding for PGraphMapping of G1, G2;
cluster directed isomorphism -> Dcontinuous Disomorphism
for PGraphMapping of G1, G2;
end;
registration
let G be _Graph;
cluster id G
-> weak_SG-embedding strong_SG-embedding isomorphism Disomorphism;
end;
registration
let G be _Graph;
cluster weak_SG-embedding strong_SG-embedding isomorphism Disomorphism
for PGraphMapping of G, G;
end;
theorem :: GLIB_010:45
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding
holds G1.order() c= G2.order() & G1.size() c= G2.size();
theorem :: GLIB_010:46
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:47
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:48
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:49
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:50
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is directed weak_SG-embedding holds
(G2 is non-Dmulti implies G1 is non-Dmulti) &
(G2 is Dsimple implies G1 is Dsimple);
theorem :: GLIB_010:51
for G1, G2 being _finite _Graph, F being PGraphMapping of G1, G2
st F is strong_SG-embedding & G1.order() = G2.order() & G1.size() = G2.size()
holds F is isomorphism;
theorem :: GLIB_010:52
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is strong_SG-embedding holds G2 is complete implies G1 is complete;
:: isomorphism as an attribute
definition
let G1, G2 be _Graph;
attr G2 is G1-isomorphic means
:: GLIB_010:def 23
ex F being PGraphMapping of G1, G2 st F is isomorphism;
attr G2 is G1-Disomorphic means
:: GLIB_010:def 24
ex F being PGraphMapping of G1, G2 st F is Disomorphism;
end;
registration
let G be _Graph;
cluster G-Disomorphic -> G-isomorphic for _Graph;
end;
registration
let G be _Graph;
cluster G-Disomorphic G-isomorphic for _Graph;
end;
theorem :: GLIB_010:53
for G being _Graph
holds G is G-Disomorphic G-isomorphic;
registration
let G1 be _Graph, G2 be G1-isomorphic _Graph;
cluster isomorphism strong_SG-embedding weak_SG-embedding
total non empty one-to-one onto semi-continuous continuous
for PGraphMapping of G1, G2;
end;
:: this is the main reason for using an attribute instead of predicate
:: for isomorphism
definition
let G1 be _Graph, G2 be G1-isomorphic _Graph;
mode Isomorphism of G1, G2 is isomorphism PGraphMapping of G1, G2;
end;
registration
let G1 be _Graph, G2 be G1-Disomorphic _Graph;
cluster isomorphism strong_SG-embedding weak_SG-embedding
total non empty one-to-one onto directed semi-Dcontinuous Dcontinuous
for PGraphMapping of G1, G2;
end;
definition
let G1 be _Graph, G2 be G1-Disomorphic _Graph;
mode DIsomorphism of G1, G2 is Disomorphism PGraphMapping of G1, G2;
end;
:: define weight-/label-/ordering-preserving mappings
definition
let G1, G2 be WGraph, 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;
end;
definition
let G1, G2 be EGraph, 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;
end;
definition
let G1, G2 be VGraph, 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;
end;
definition
let G1, G2 be [Ordered] _Graph, 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;
end;
registration
let G be WGraph;
cluster id G -> weight-preserving;
end;
registration
let G be EGraph;
cluster id G -> elabel-preserving;
end;
registration
let G be VGraph;
cluster id G -> vlabel-preserving;
end;
registration
let G be [Ordered] _Graph;
cluster id G -> ordering-preserving;
end;
:: define domain and range of graph mappings
definition
let G1, G2 be _Graph, 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;
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;
end;
registration
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
cluster dom F -> plain;
cluster rng F -> plain;
end;
theorem :: GLIB_010:54
for G1, G2 being _Graph, 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;
theorem :: GLIB_010:55
for G1, G2 be _Graph, F being non empty PGraphMapping of G1, G2
holds F is total iff dom F == G1;
theorem :: GLIB_010:56
for G1, G2 be _Graph, F being non empty PGraphMapping of G1, G2
holds F is onto iff rng F == G2;
:: define restrictions of graph mappings
definition
let G1, G2 be _Graph, H be Subgraph of G1, 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 ];
end;
theorem :: GLIB_010:57
for G1, G2 being _Graph, 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) &
(F is non onto implies F | H is non onto) &
(F is directed implies F | H is directed) &
(F is semi-Dcontinuous implies F | H is semi-Dcontinuous);
theorem :: GLIB_010:58
for G1, G2 being _Graph, V being set, 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);
registration
let G1, G2 be _Graph, H be Subgraph of G1;
let F be empty PGraphMapping of G1, G2;
cluster F | H -> empty;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G1;
let F be one-to-one PGraphMapping of G1, G2;
cluster F | H -> one-to-one;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G1;
let F be semi-continuous PGraphMapping of G1, G2;
cluster F | H -> semi-continuous;
end;
registration
let G1, G2 be _Graph, V be set, H be inducedSubgraph of G1, V;
let F be continuous PGraphMapping of G1, G2;
cluster F | H -> continuous;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G1;
let F be directed PGraphMapping of G1, G2;
cluster F | H -> directed;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G1;
let F be semi-Dcontinuous PGraphMapping of G1, G2;
cluster F | H -> semi-Dcontinuous;
end;
registration
let G1, G2 be _Graph, V be set, H be inducedSubgraph of G1, V;
let F be Dcontinuous PGraphMapping of G1, G2;
cluster F | H -> Dcontinuous;
end;
registration
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
cluster F | dom F -> total;
end;
theorem :: GLIB_010:59
for G1, G2 being _Graph, H being Subgraph of G1,
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;
theorem :: GLIB_010:60
for G1, G2 being WGraph, H being WSubgraph of G1,
F being PGraphMapping of G1, G2
st F is weight-preserving holds F | H is weight-preserving;
theorem :: GLIB_010:61
for G1, G2 being EGraph, H being ESubgraph of G1,
F being PGraphMapping of G1, G2
st F is elabel-preserving holds F | H is elabel-preserving;
theorem :: GLIB_010:62
for G1, G2 being VGraph, H being VSubgraph of G1,
F being PGraphMapping of G1, G2
st F is vlabel-preserving holds F | H is vlabel-preserving;
definition
let G1, G2 be _Graph, H be Subgraph of G2, 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 ];
end;
theorem :: GLIB_010:63
for G1, G2 being _Graph, 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) &
(F is non total implies H |` F is non 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);
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be empty PGraphMapping of G1, G2;
cluster H |` F -> empty;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be one-to-one PGraphMapping of G1, G2;
cluster H |` F -> one-to-one;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be semi-continuous PGraphMapping of G1, G2;
cluster H |` F -> semi-continuous;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be continuous PGraphMapping of G1, G2;
cluster H |` F -> continuous;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be directed PGraphMapping of G1, G2;
cluster H |` F -> directed;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be semi-Dcontinuous PGraphMapping of G1, G2;
cluster H |` F -> semi-Dcontinuous;
end;
registration
let G1, G2 be _Graph, H be Subgraph of G2;
let F be Dcontinuous PGraphMapping of G1, G2;
cluster H |` F -> Dcontinuous;
end;
registration
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
cluster rng F |` F -> onto;
end;
theorem :: GLIB_010:64
for G1, G2 being _Graph, H being Subgraph of G2,
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;
theorem :: GLIB_010:65
for G1, G2 being WGraph, H being WSubgraph of G2,
F being PGraphMapping of G1, G2
st F is weight-preserving holds H |` F is weight-preserving;
theorem :: GLIB_010:66
for G1, G2 being EGraph, H being ESubgraph of G2,
F being PGraphMapping of G1, G2
st F is elabel-preserving holds H |` F is elabel-preserving;
theorem :: GLIB_010:67
for G1, G2 being VGraph, H being VSubgraph of G2,
F being PGraphMapping of G1, G2
st F is vlabel-preserving holds H |` F is vlabel-preserving;
theorem :: GLIB_010:68
for G1, G2 being _Graph, F being PGraphMapping of G1, G2,
H1 being Subgraph of G1, H2 being Subgraph of G2
holds (H2|`F)|H1 = H2|`(F|H1);
:: define inverse of graph mappings
definition
let G1, G2 be _Graph, F be one-to-one PGraphMapping of G1, G2;
func F" -> PGraphMapping of G2, G1 equals
:: GLIB_010:def 33
[ F_V" , F_E" ];
end;
registration
let G1, G2 be _Graph, F be one-to-one PGraphMapping of G1, G2;
cluster F" -> one-to-one semi-continuous;
end;
registration
let G1, G2 be _Graph, F be empty one-to-one PGraphMapping of G1, G2;
cluster F" -> empty;
end;
registration
let G1, G2 be _Graph, F be non empty one-to-one PGraphMapping of G1, G2;
cluster F" -> non empty;
end;
registration
let G1, G2 be _Graph;
let F be one-to-one semi-Dcontinuous PGraphMapping of G1, G2;
cluster F" -> semi-Dcontinuous;
end;
theorem :: GLIB_010:69
:: this would otherwise need Proof outside of this article
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
holds F"_V = F_V" & F"_E = F_E";
theorem :: GLIB_010:70
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
holds (F")" = F;
theorem :: GLIB_010:71
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
holds F is total iff F" is onto;
theorem :: GLIB_010:72
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
holds F is onto iff F" is total;
theorem :: GLIB_010:73
for G1, G2 being _Graph, F be one-to-one PGraphMapping of G1, G2
st F is total continuous holds F" is continuous;
theorem :: GLIB_010:74
for G1, G2 being _Graph, F be one-to-one PGraphMapping of G1, G2
st F is total Dcontinuous holds F" is Dcontinuous;
theorem :: GLIB_010:75
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
holds F is isomorphism iff F" is isomorphism;
theorem :: GLIB_010:76
for G1, G2 being WGraph, F being one-to-one PGraphMapping of G1, G2
holds F is weight-preserving iff F" is weight-preserving;
theorem :: GLIB_010:77
for G1, G2 being EGraph, F being one-to-one PGraphMapping of G1, G2
holds F is elabel-preserving iff F" is elabel-preserving;
theorem :: GLIB_010:78
for G1, G2 being VGraph, F being one-to-one PGraphMapping of G1, G2
holds F is vlabel-preserving iff F" is vlabel-preserving;
theorem :: GLIB_010:79
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
st F is onto for v being Vertex of G2 holds F"_V.v is Vertex of G1;
theorem :: GLIB_010:80
for G being _Graph holds (id G)" = id G;
theorem :: GLIB_010:81
for G1, G2 be _Graph, F being non empty one-to-one PGraphMapping of G1, G2
holds dom F = rng(F") & rng F = dom(F");
theorem :: GLIB_010:82
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2,
H being Subgraph of G1 holds (F|H)" = H |` (F");
theorem :: GLIB_010:83
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2,
H being Subgraph of G2 holds (H |` F)" = F" | H;
:: properties derived by use of F"
theorem :: GLIB_010:84
for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is isomorphism
holds G1.order() = G2.order() & G1.size() = G2.size();
theorem :: GLIB_010:85
for G1, G2 being _finite _Graph, F being PGraphMapping of G1, G2
st F is strong_SG-embedding
holds (ex F0 being PGraphMapping of G1, G2 st F0 is isomorphism)
implies F is isomorphism;
theorem :: GLIB_010:86
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:87
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:88
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:89
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds
(G1 is _trivial iff G2 is _trivial) &
(G1 is loopless iff G2 is loopless) &
(G1 is edgeless iff G2 is edgeless) &
(G1 is non-multi iff G2 is non-multi) &
(G1 is simple iff G2 is simple) &
(G1 is _finite iff G2 is _finite) &
(G1 is complete iff G2 is complete);
theorem :: GLIB_010:90
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Dcontinuous isomorphism holds
(G1 is non-Dmulti iff G2 is non-Dmulti) &
(G1 is Dsimple iff G2 is Dsimple);
theorem :: GLIB_010:91
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
holds card((dom F).loops()) = card((rng F).loops());
theorem :: GLIB_010:92
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
st F is total holds card(G1.loops()) c= card(G2.loops());
theorem :: GLIB_010:93
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
st F is onto holds card(G2.loops()) c= card(G1.loops());
theorem :: GLIB_010:94
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
st F is isomorphism holds card(G1.loops()) = card(G2.loops());
theorem :: GLIB_010:95
for G1 being _Graph, G2 being G1-isomorphic _Graph
holds G1 is G2-isomorphic;
theorem :: GLIB_010:96
for G1 being _Graph, G2 being G1-Disomorphic _Graph
holds G1 is G2-Disomorphic;
theorem :: GLIB_010:97
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being G2-isomorphic _Graph, 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;
theorem :: GLIB_010:98
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being G2-isomorphic _Graph, F being Isomorphism of G1, G2
st G1 == G3 holds F" is Isomorphism of G2, G3;
theorem :: GLIB_010:99
for G1 being _Graph, G2 being G1-Disomorphic _Graph
for G3 being G2-Disomorphic _Graph, F being DIsomorphism of G1, G2
st G1 == G3 holds F" is DIsomorphism of G2, G3;
:: define composition of graph mappings
definition
let G1, G2, G3 be _Graph;
let F1 be PGraphMapping of G1, G2, 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 ];
end;
theorem :: GLIB_010:100
:: this would otherwise need Proof outside of this article
for G1, G2, G3 being _Graph
for F1 being PGraphMapping of G1, G2, F2 being PGraphMapping of G2, G3
holds (F2*F1)_V = F2_V * F1_V & (F2*F1)_E = F2_E * F1_E;
theorem :: GLIB_010:101
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F2 * F1 is onto holds F2 is onto;
theorem :: GLIB_010:102
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F2 * F1 is total holds F1 is total;
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;
cluster F2 * F1 -> one-to-one;
end;
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;
cluster F2 * F1 -> semi-continuous;
end;
registration
let G1, G2, G3 be _Graph;
let F1 be continuous PGraphMapping of G1, G2;
let F2 be continuous PGraphMapping of G2, G3;
cluster F2 * F1 -> continuous;
end;
registration
let G1, G2, G3 be _Graph;
let F1 be directed PGraphMapping of G1, G2;
let F2 be directed PGraphMapping of G2, G3;
cluster F2 * F1 -> directed;
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;
cluster F2 * F1 -> semi-Dcontinuous;
end;
registration
let G1, G2, G3 be _Graph;
let F1 be Dcontinuous PGraphMapping of G1, G2;
let F2 be Dcontinuous PGraphMapping of G2, G3;
cluster F2 * F1 -> Dcontinuous;
end;
registration
let G1, G2, G3 be _Graph;
let F1 be empty PGraphMapping of G1, G2;
let F2 be PGraphMapping of G2, G3;
cluster F2 * F1 -> empty;
end;
registration
let G1, G2, G3 be _Graph;
let F1 be PGraphMapping of G1, G2;
let F2 be empty PGraphMapping of G2, G3;
cluster F2 * F1 -> empty;
end;
theorem :: GLIB_010:103
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is total & rng F1_V c= dom F2_V & rng F1_E c= dom F2_E
holds F2 * F1 is total;
theorem :: GLIB_010:104
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is total & F2 is total holds F2 * F1 is total;
theorem :: GLIB_010:105
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F2 is onto & dom F2_V c= rng F1_V & dom F2_E c= rng F1_E
holds F2 * F1 is onto;
theorem :: GLIB_010:106
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is onto & F2 is onto holds F2 * F1 is onto;
theorem :: GLIB_010:107
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is weak_SG-embedding & F2 is weak_SG-embedding
holds F2 * F1 is weak_SG-embedding;
theorem :: GLIB_010:108
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is strong_SG-embedding & F2 is strong_SG-embedding
holds F2 * F1 is strong_SG-embedding;
theorem :: GLIB_010:109
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3 st F1 is isomorphism & F2 is isomorphism
holds F2 * F1 is isomorphism;
theorem :: GLIB_010:110
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3 st F1 is Disomorphism & F2 is Disomorphism
holds F2 * F1 is Disomorphism;
theorem :: GLIB_010:111
for G1, G2, G3 being WGraph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is weight-preserving & F2 is weight-preserving
holds F2 * F1 is weight-preserving;
theorem :: GLIB_010:112
for G1, G2, G3 being EGraph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is elabel-preserving & F2 is elabel-preserving
holds F2 * F1 is elabel-preserving;
theorem :: GLIB_010:113
for G1, G2, G3 being VGraph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3
st F1 is vlabel-preserving & F2 is vlabel-preserving
holds F2 * F1 is vlabel-preserving;
theorem :: GLIB_010:114
for G1, G2, G3, G4 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3, F3 being PGraphMapping of G3, G4
holds F3 * (F2 * F1) = (F3 * F2) * F1;
theorem :: GLIB_010:115
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
st F is isomorphism holds F*(F") = id G2 & (F")*F = id G1;
theorem :: GLIB_010:116
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F * id G1 = F & (id G2) * F = F;
theorem :: GLIB_010:117
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3, H being Subgraph of G1
holds F2 * (F1|H) = (F2*F1) | H;
theorem :: GLIB_010:118
for G1, G2, G3 being _Graph, F1 being PGraphMapping of G1, G2,
F2 being PGraphMapping of G2, G3, H being Subgraph of G3
holds (H|`F2) * F1 = H |` (F2*F1);
registration
let G1 be _Graph, G2 be G1-isomorphic _Graph;
cluster G2-isomorphic -> G1-isomorphic for _Graph;
end;
registration
let G1 be _Graph, G2 be G1-Disomorphic _Graph;
cluster G2-Disomorphic -> G1-Disomorphic for _Graph;
end;
begin :: Walks induced by Graph Mappings
definition
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, W1 be Walk of G1;
attr W1 is F-defined means
:: GLIB_010:def 35
W1.vertices() c= dom F_V & W1.edges() c= dom F_E;
end;
definition
let G1, G2 be _Graph, F be PGraphMapping of G1, G2, W2 be Walk of G2;
attr W2 is F-valued means
:: GLIB_010:def 36
W2.vertices() c= rng F_V & W2.edges() c= rng F_E;
end;
registration
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
cluster F-defined trivial for Walk of G1;
cluster F-valued trivial for Walk of G2;
end;
theorem :: GLIB_010:119
for G1, G2 being _Graph, F being empty PGraphMapping of G1, G2,
W1 being Walk of G1 holds W1 is non F-defined;
theorem :: GLIB_010:120
for G1, G2 being _Graph, F being empty PGraphMapping of G1, G2,
W2 being Walk of G2 holds W2 is non F-valued;
theorem :: GLIB_010:121
for G1, G2 being _Graph, F be PGraphMapping of G1, G2, W1 being Walk of G1
st F is total holds W1 is F-defined;
theorem :: GLIB_010:122
for G1, G2 being _Graph, F be PGraphMapping of G1, G2, W2 being Walk of G2
st F is onto holds W2 is F-valued;
registration
let G1, G2 be _Graph, F be one-to-one PGraphMapping of G1, G2;
cluster F-defined -> F"-valued for Walk of G1;
cluster F-valued -> F"-defined for Walk of G2;
end;
definition
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let W1 be F-defined Walk of G1;
func F.:W1 -> Walk of G2 means
:: GLIB_010:def 37
F_V * W1.vertexSeq() = it.vertexSeq() & F_E * W1.edgeSeq() = it.edgeSeq();
end;
registration
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let W1 be F-defined Walk of G1;
cluster F.:W1 -> F-valued;
end;
definition
let G1, G2 be _Graph, F be non empty PGraphMapping of G1, G2;
let W1 be F-defined Walk of G1;
redefine func F.:W1 -> F-valued Walk of G2;
end;
definition
let G1, G2 be _Graph, F be non empty one-to-one PGraphMapping of G1, G2;
let W2 be F-valued Walk of G2;
func F"W2 -> F-defined Walk of G1 equals
:: GLIB_010:def 38
F".:W2;
end;
definition
let G1, G2 be _Graph, 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();
end;
theorem :: GLIB_010:123
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1, G2
for W1 being F-defined Walk of G1 holds F"(F.:W1) = W1;
theorem :: GLIB_010:124
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2 holds F.:(F"W2) = W2;
theorem :: GLIB_010:125
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1
holds W1.length() = (F.:W1).length() & len W1 = len (F.:W1);
theorem :: GLIB_010:126
for G1, G2 being _Graph,
F being non empty one-to-one PGraphMapping of G1, G2,
W2 being F-valued Walk of G2
holds W2.length() = (F"W2).length() & len W2 = len (F"W2);
theorem :: GLIB_010:127
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1
holds
F_V.(W1.first()) = (F.:W1).first() & F_V.(W1.last()) = (F.:W1).last();
theorem :: GLIB_010:128
for G1, G2 being _Graph,
F being non empty one-to-one PGraphMapping of G1, G2,
W2 being F-valued Walk of G2
holds
F_V".(W2.first()) = (F"W2).first() & F_V".(W2.last()) = (F"W2).last();
theorem :: GLIB_010:129
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1, n being odd Element of NAT
st n <= len W1 holds F_V.(W1.n) = (F.:W1).n;
theorem :: GLIB_010:130
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1, n being even Element of NAT
st 1 <= n & n <= len W1 holds F_E.(W1.n) = (F.:W1).n;
theorem :: GLIB_010:131
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1, v, w being object
holds W1 is_Walk_from v,w implies v in dom F_V & w in dom F_V;
theorem :: GLIB_010:132
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1, v, w being object
holds W1 is_Walk_from v,w implies F.:W1 is_Walk_from F_V.v, F_V.w;
theorem :: GLIB_010:133
for G1, G2 being _Graph,
F being non empty one-to-one PGraphMapping of G1, G2,
W1 being F-defined Walk of G1, 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;
theorem :: GLIB_010:134
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W1 being F-defined Walk of G1 st F_V.(W1.first()) = F_V.(W1.last())
holds W1.first() = W1.last();
theorem :: GLIB_010:135
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for W1 being F-defined Walk of G1
holds (F.:W1).vertices() = F_V.:W1.vertices();
theorem :: GLIB_010:136
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for W1 being F-defined Walk of G1
holds (F.:W1).edges() = F_E.:W1.edges();
theorem :: GLIB_010:137
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2,
W1 being F-defined Walk of G1
holds
(W1 is trivial implies F.:W1 is trivial) &
(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);
theorem :: GLIB_010:138
for G1, G2 being _Graph,
F being non empty one-to-one PGraphMapping of G1, G2,
W1 being F-defined Walk of G1
holds
(W1 is trivial iff F.:W1 is trivial) &
(W1 is closed iff F.:W1 is closed) &
(W1 is Trail-like iff F.:W1 is Trail-like) &
(W1 is Path-like iff F.:W1 is Path-like) &
(W1 is Circuit-like iff F.:W1 is Circuit-like) &
(W1 is Cycle-like iff F.:W1 is Cycle-like);
:: properties derived using walks
theorem :: GLIB_010:139
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is strong_SG-embedding
holds G2 is acyclic implies G1 is acyclic;
theorem :: GLIB_010:140
for G1, G2 being _Graph, F being PGraphMapping of G1, G2 st F is isomorphism
holds (G1 is acyclic iff G2 is acyclic) &
(G1 is chordal iff G2 is chordal) &
(G1 is connected iff G2 is connected);
begin :: Graph Mappings and Graph Modes
theorem :: GLIB_010:141
for G1, G2 being _Graph, 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 non empty implies F is non 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);
theorem :: GLIB_010:142
for G1, G2 being _Graph, 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);
theorem :: GLIB_010:143
for G1 being _Graph, G2 being G1-isomorphic _Graph, E1, E2 being set
for G3 being reverseEdgeDirections of G1, E1
for G4 being reverseEdgeDirections of G2, E2
holds G4 is G3-isomorphic;
theorem :: GLIB_010:144
for G3, G4 being _Graph, V1, V2 being set
for G1 being addVertices of G3,V1, G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4, f being one-to-one Function
st dom f = V1 \ the_Vertices_of G3 & rng f = V2 \ the_Vertices_of G4
ex F being PGraphMapping of G1, G2 st F = [F0_V +* f, F0_E] &
(F0 is non empty implies F is non 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);
theorem :: GLIB_010:145
for G3, G4 being _Graph, V1, V2 being set
for G1 being addVertices of G3,V1, G2 being addVertices of G4,V2
for F0 being PGraphMapping of G3,G4, f being one-to-one Function
st dom f = V1 \ the_Vertices_of G3 & rng f = V2 \ the_Vertices_of G4
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);
theorem :: GLIB_010:146
for G3 being _Graph, G4 being G3-isomorphic _Graph, V1, V2 being set
for G1 being addVertices of G3,V1, G2 being addVertices of G4,V2
st card(V1 \ the_Vertices_of G3) = card(V2 \ the_Vertices_of G4)
holds G2 is G1-isomorphic;
theorem :: GLIB_010:147
for G3 being _Graph, G4 being G3-Disomorphic _Graph, V1, V2 being set
for G1 being addVertices of G3, V1,G2 being addVertices of G4,V2
st card(V1 \ the_Vertices_of G3) = card(V2 \ the_Vertices_of G4)
holds G2 is G1-Disomorphic;
theorem :: GLIB_010:148
for G3, G4 being _Graph, v1, v2 being object
for G1 being addVertex of G3,v1, 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
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);
theorem :: GLIB_010:149
for G3, G4 being _Graph, v1, v2 being object
for G1 being addVertex of G3,v1, 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
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);
theorem :: GLIB_010:150
for G3 being _Graph, G4 being G3-isomorphic _Graph, v1, v2 being object
for G1 being addVertex of G3, v1, G2 being addVertex of G4, v2
st v1 in the_Vertices_of G3 iff v2 in the_Vertices_of G4
holds G2 is G1-isomorphic;
theorem :: GLIB_010:151
for G3 being _Graph, G4 being G3-Disomorphic _Graph, v1, v2 being object
for G1 being addVertex of G3, v1, G2 being addVertex of G4, v2
st v1 in the_Vertices_of G3 iff v2 in the_Vertices_of G4
holds G2 is G1-Disomorphic;
:: 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.
theorem :: GLIB_010:152
for G3, G4 being _Graph, v1, v3 being Vertex of G3, v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3, 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)
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);
theorem :: GLIB_010:153
for G3, G4 being _Graph, v1, v3 being Vertex of G3, v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3, 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)
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 (semi-)Dcontinuous, the same remarks as above apply.
theorem :: GLIB_010:154
for G3, G4 being _Graph, v1, v3 being Vertex of G3, v2, v4 being Vertex of G4
for e1, e2 being object
for G1 being addEdge of G3,v1,e1,v3, 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
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);
:: Similar to addEdge, the (semi-)(D)continuous properties are not
:: always carried over from F0 to F due to possible isolated vertices.
theorem :: GLIB_010:155
for G3, G4 being _Graph, v3 being Vertex of G3, 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
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);
theorem :: GLIB_010:156
for G3, G4 being _Graph, v3 being Vertex of G3, 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
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);
theorem :: GLIB_010:157
for G3, G4 being _Graph, v3 being Vertex of G3, 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
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);
theorem :: GLIB_010:158
for G3, G4 being _Graph, v3 being Vertex of G3, 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
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);
theorem :: GLIB_010:159
for G3, G4 being _Graph, v3 being Vertex of G3, 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
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);
theorem :: GLIB_010:160
for G3, G4 being _Graph, v3 being Vertex of G3, 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
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);
theorem :: GLIB_010:161
for G being _Graph, v being object, V being set
for G1, G2 being addAdjVertexAll of G,v,V
holds G2 is G1-isomorphic;
theorem :: GLIB_010:162
for G3, G4 being _Graph, v1,v2 being object, 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
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);
theorem :: GLIB_010:163
for G3 being _Graph, G4 being G3-isomorphic _Graph, v1, v2 being object
for G1 being addAdjVertexAll of G3,v1
for G2 being addAdjVertexAll of G4,v2
st v1 in the_Vertices_of G3 iff v2 in the_Vertices_of G4
holds G2 is G1-isomorphic;
theorem :: GLIB_010:164
for G1, G2 being _Graph
for G3 being removeLoops of G1, 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 and F are automatically semi-continuous
(F0 is semi-Dcontinuous implies F is semi-Dcontinuous);
theorem :: GLIB_010:165
for G1, G2 being _Graph
for G3 being removeLoops of G1, 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);
theorem :: GLIB_010:166
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being removeLoops of G1, G4 being removeLoops of G2
holds G4 is G3-isomorphic;
theorem :: GLIB_010:167
for G1 being _Graph, G2 being G1-Disomorphic _Graph
for G3 being removeLoops of G1, G4 being removeLoops of G2
holds G4 is G3-Disomorphic;
theorem :: GLIB_010:168
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being removeParallelEdges of G1
for G4 being removeParallelEdges of G2
holds G4 is G3-isomorphic;
theorem :: GLIB_010:169
for G1 being _Graph, G2, G3 being removeParallelEdges of G1
holds G3 is G2-isomorphic;
theorem :: GLIB_010:170
for G1 being _Graph, G2 being G1-Disomorphic _Graph
for G3 being removeDParallelEdges of G1
for G4 being removeDParallelEdges of G2
holds G4 is G3-Disomorphic;
theorem :: GLIB_010:171
for G1 being _Graph, G2, G3 being removeDParallelEdges of G1
holds G3 is G2-Disomorphic;
theorem :: GLIB_010:172
for G1 being _Graph, G2 being G1-isomorphic _Graph
for G3 being SimpleGraph of G1, G4 being SimpleGraph of G2
holds G4 is G3-isomorphic;
theorem :: GLIB_010:173
for G1 being _Graph, G2, G3 being SimpleGraph of G1
holds G3 is G2-isomorphic;
theorem :: GLIB_010:174
for G1 being _Graph, G2 being G1-Disomorphic _Graph
for G3 being DSimpleGraph of G1, G4 being DSimpleGraph of G2
holds G4 is G3-Disomorphic;
theorem :: GLIB_010:175
for G1 being _Graph, G2, G3 being DSimpleGraph of G1
holds G3 is G2-Disomorphic;
theorem :: GLIB_010:176
for G1, G2 being _trivial loopless _Graph
for F being non empty PGraphMapping of G1, G2
holds F is Disomorphism &
F = [ (the Vertex of G1) .--> the Vertex of G2, {} ];
theorem :: GLIB_010:177
for G1, G2 being _trivial _Graph st G1.size() = G2.size()
ex F being PGraphMapping of G1, G2 st F is Disomorphism;
:: 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.
theorem :: GLIB_010:178
for G1, G2 being _trivial loopless _Graph
holds G2 is G1-Disomorphic G1-isomorphic;