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