:: About Graph Sums
:: by Sebastian Koch
::
:: Received November 30, 2021
:: Copyright (c) 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, FINSET_1, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1,
FINSEQ_1, NAT_1, FUNCT_4, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, CARD_2,
ORDINAL2, XXREAL_0, PBOOLE, XCMPLX_0, RELAT_2, PARTFUN1, WELLORD1,
RING_3, FUNCT_2, MCART_1, TREES_1, WAYBEL_0, MOD_4, FUNCT_7, GLIB_015,
MSUALG_6, EQREL_1, ABIAN, TAXONOM2, GLIB_000, GLIB_001, GLIB_002, CHORD,
SCMYCIEL, SIMPLEX0, GLIB_009, GLIB_006, GLIB_007, GLIB_010, GLIB_012,
GLIB_013, GLIB_014;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, DOMAIN_1,
FUNCT_3, FUNCOP_1, FUNCT_4, ORDINAL2, FINSET_1, CARD_1, PBOOLE, CARD_3,
NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CARD_2, FINSEQ_1, EQREL_1, FINSEQ_4,
FUNCT_7, ABIAN, GLIB_000, TAXONOM2, COMPUT_1, GLIB_001, GLIB_002, CHORD,
AOFA_I00, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIBPRE0,
GLIB_012, GLIB_013, GLIB_014, GLIBPRE1;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, FUNCT_3,
FUNCT_7, GLIB_000, GLIB_001, GLIB_002, CHORD, GLIB_007, GLIB_008,
GLIB_009, GLIB_010, GLIB_012, GLIB_013, GLIB_014, GLIBPRE0, GLIB_006,
MCART_1, COMPUT_1, EQREL_1, ABIAN, CARD_3, TAXONOM2, AOFA_I00, PARTFUN2,
ORDINAL1, FINSET_1, QC_LANG1, CQC_LANG, GLIBPRE1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_4, FUNCT_2, PARTFUN1,
RELSET_1, FUNCT_3, FUNCT_7, XTUPLE_0, COMPUT_1, INT_1, PRE_POLY,
GLIB_000, GLIB_002, CHORD, GLIB_008, GLIB_009, GLIB_006, GLIBPRE0,
GLIB_010, GLIB_012, GLIB_013, GLIB_014, ABIAN, CARD_3, EQREL_1, GLIBPRE1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin
definition
let G be _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
func replaceVerticesEdges(V,E) -> plain _Graph means
:: GLIB_015:def 1
ex S,T being Function of rng E, rng V
st S = V*(the_Source_of G)*(E") & T = V*(the_Target_of G)*(E") &
it = createGraph(rng V,rng E,S,T);
end;
definition
let G be _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
func replaceVertices(V) -> plain _Graph equals
:: GLIB_015:def 2
replaceVerticesEdges(V,id the_Edges_of G);
end;
definition
let G be _Graph, E be one-to-one ManySortedSet of the_Edges_of G;
func replaceEdges(E) -> plain _Graph equals
:: GLIB_015:def 3
replaceVerticesEdges(id the_Vertices_of G, E);
end;
theorem :: GLIB_015:1
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
holds the_Vertices_of replaceVerticesEdges(V,E) = rng V &
the_Edges_of replaceVerticesEdges(V,E) = rng E &
the_Source_of replaceVerticesEdges(V,E) = V*(the_Source_of G)*(E") &
the_Target_of replaceVerticesEdges(V,E) = V*(the_Target_of G)*(E");
theorem :: GLIB_015:2
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
holds the_Vertices_of replaceVertices(V) = rng V &
the_Edges_of replaceVertices(V) = the_Edges_of G &
the_Source_of replaceVertices(V) = V*(the_Source_of G) &
the_Target_of replaceVertices(V) = V*(the_Target_of G);
theorem :: GLIB_015:3
for G being _Graph
for E being one-to-one ManySortedSet of the_Edges_of G
holds the_Vertices_of replaceEdges(E) = the_Vertices_of G &
the_Edges_of replaceEdges(E) = rng E &
the_Source_of replaceEdges(E) = (the_Source_of G)*(E") &
the_Target_of replaceEdges(E) = (the_Target_of G)*(E");
theorem :: GLIB_015:4
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e DJoins v,w,G
holds E.e DJoins V.v,V.w,replaceVerticesEdges(V,E);
theorem :: GLIB_015:5
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e,v,w being object st e DJoins v,w,G
holds e DJoins V.v,V.w,replaceVertices(V);
theorem :: GLIB_015:6
for G being _Graph, E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e DJoins v,w,G
holds E.e DJoins v,w,replaceEdges(E);
theorem :: GLIB_015:7
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e Joins v,w,G
holds E.e Joins V.v,V.w,replaceVerticesEdges(V,E);
theorem :: GLIB_015:8
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e,v,w being object st e Joins v,w,G
holds e Joins V.v,V.w,replaceVertices(V);
theorem :: GLIB_015:9
for G being _Graph, E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e Joins v,w,G
holds E.e Joins v,w,replaceEdges(E);
theorem :: GLIB_015:10
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e in dom E & v in dom V & w in dom V &
E.e DJoins V.v,V.w,replaceVerticesEdges(V,E)
holds e DJoins v,w,G;
theorem :: GLIB_015:11
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e,v,w being object
st v in dom V & w in dom V & e DJoins V.v,V.w,replaceVertices(V)
holds e DJoins v,w,G;
theorem :: GLIB_015:12
for G being _Graph, E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e in dom E & E.e DJoins v,w,replaceEdges(E)
holds e DJoins v,w,G;
theorem :: GLIB_015:13
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e in dom E & v in dom V & w in dom V &
E.e Joins V.v,V.w,replaceVerticesEdges(V,E)
holds e Joins v,w,G;
theorem :: GLIB_015:14
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e,v,w being object st v in dom V & w in dom V &
e Joins V.v,V.w,replaceVertices(V)
holds e Joins v,w,G;
theorem :: GLIB_015:15
for G being _Graph, E being one-to-one ManySortedSet of the_Edges_of G
for e,v,w being object st e in dom E & E.e Joins v,w,replaceEdges(E)
holds e Joins v,w,G;
theorem :: GLIB_015:16
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
ex F being PGraphMapping of G, replaceVerticesEdges(V,E)
st F_V = V & F_E = E & F is Disomorphism;
theorem :: GLIB_015:17
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
holds replaceVerticesEdges(V,E) is G-Disomorphic;
:: clusterings (from Disomorphic)
registration
let G be loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> loopless;
end;
registration
let G be loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> loopless;
end;
registration
let G be loopless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> loopless;
end;
registration
let G be non loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non loopless;
end;
registration
let G be non loopless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non loopless;
end;
registration
let G be non loopless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non loopless;
end;
registration
let G be non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non-multi;
end;
registration
let G be non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non-multi;
end;
registration
let G be non-multi _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non-multi;
end;
registration
let G be non non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non non-multi;
end;
registration
let G be non non-multi _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non non-multi;
end;
registration
let G be non non-multi _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non non-multi;
end;
registration
let G be non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non-Dmulti;
end;
registration
let G be non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non-Dmulti;
end;
registration
let G be non-Dmulti _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non-Dmulti;
end;
registration
let G be non non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non non-Dmulti;
end;
registration
let G be non non-Dmulti _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non non-Dmulti;
end;
registration
let G be non non-Dmulti _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non non-Dmulti;
end;
registration
let G be simple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> simple;
end;
registration
let G be simple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> simple;
end;
registration
let G be simple _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> simple;
end;
registration
let G be Dsimple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> Dsimple;
end;
registration
let G be Dsimple _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> Dsimple;
end;
registration
let G be Dsimple _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> Dsimple;
end;
registration
let G be _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> _trivial;
end;
registration
let G be _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> _trivial;
end;
registration
let G be _trivial _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> _trivial;
end;
registration
let G be non _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non _trivial;
end;
registration
let G be non _trivial _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non _trivial;
end;
registration
let G be non _trivial _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non _trivial;
end;
registration
let G be vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> vertex-finite;
end;
registration
let G be vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> vertex-finite;
end;
registration
let G be vertex-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> vertex-finite;
end;
registration
let G be non vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non vertex-finite;
end;
registration
let G be non vertex-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non vertex-finite;
end;
registration
let G be non vertex-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non vertex-finite;
end;
registration
let G be edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> edge-finite;
end;
registration
let G be edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> edge-finite;
end;
registration
let G be edge-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> edge-finite;
end;
registration
let G be non edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non edge-finite;
end;
registration
let G be non edge-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non edge-finite;
end;
registration
let G be non edge-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non edge-finite;
end;
registration
let G be finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> finite;
end;
registration
let G be finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> finite;
end;
registration
let G be finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> finite;
end;
registration
let G be acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> acyclic;
end;
registration
let G be acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> acyclic;
end;
registration
let G be acyclic _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> acyclic;
end;
registration
let G be non acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non acyclic;
end;
registration
let G be non acyclic _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non acyclic;
end;
registration
let G be non acyclic _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non acyclic;
end;
registration
let G be connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> connected;
end;
registration
let G be connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> connected;
end;
registration
let G be connected _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> connected;
end;
registration
let G be non connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non connected;
end;
registration
let G be non connected _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non connected;
end;
registration
let G be non connected _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non connected;
end;
registration
let G be Tree-like _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> Tree-like;
end;
registration
let G be Tree-like _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> Tree-like;
end;
registration
let G be Tree-like _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> Tree-like;
end;
registration
let G be chordal _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> chordal;
end;
registration
let G be chordal _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> chordal;
end;
registration
let G be chordal _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> chordal;
end;
:: clustering for non chordal graphs will be done after existence clustering
:: registration
:: let G be non chordal _Graph;
:: let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
:: let E be one-to-one ManySortedSet of the_Edges_of G;
:: cluster replaceVerticesEdges(V,E) -> non chordal;
:: coherence;
:: end;
::
:: registration
:: let G be non chordal _Graph;
:: let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
:: cluster replaceVertices(V) -> non chordal;
:: coherence;
:: end;
::
:: registration
:: let G be non chordal _Graph;
:: let E be one-to-one ManySortedSet of the_Edges_of G;
:: cluster replaceEdges(E) -> non chordal;
:: coherence;
:: end;
registration
let G be edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> edgeless;
end;
registration
let G be edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> edgeless;
end;
registration
let G be edgeless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> edgeless;
end;
registration
let G be non edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non edgeless;
end;
registration
let G be non edgeless _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non edgeless;
end;
registration
let G be non edgeless _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non edgeless;
end;
registration
let G be loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> loopfull;
end;
registration
let G be loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> loopfull;
end;
registration
let G be loopfull _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> loopfull;
end;
registration
let G be non loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non loopfull;
end;
registration
let G be non loopfull _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non loopfull;
end;
registration
let G be non loopfull _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non loopfull;
end;
registration
let G be locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> locally-finite;
end;
registration
let G be locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> locally-finite;
end;
registration
let G be locally-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> locally-finite;
end;
registration
let G be non locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> non locally-finite;
end;
registration
let G be non locally-finite _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> non locally-finite;
end;
registration
let G be non locally-finite _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> non locally-finite;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> c-vertex;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> c-vertex;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> c-vertex;
end;
registration
let c be Cardinal, G be c-edge _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceVerticesEdges(V,E) -> c-edge;
end;
registration
let c be Cardinal, G be c-edge _Graph;
let V be non empty one-to-one ManySortedSet of the_Vertices_of G;
cluster replaceVertices(V) -> c-edge;
end;
registration
let c be Cardinal, G be c-edge _Graph;
let E be one-to-one ManySortedSet of the_Edges_of G;
cluster replaceEdges(E) -> c-edge;
end;
theorem :: GLIB_015:18
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for W1 being Walk of G ex W2 being Walk of replaceVerticesEdges(V,E)
st V*(W1.vertexSeq()) = W2.vertexSeq() & E*(W1.edgeSeq()) = W2.edgeSeq();
theorem :: GLIB_015:19
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for W1 being Walk of G ex W2 being Walk of replaceVertices(V)
st V*(W1.vertexSeq()) = W2.vertexSeq() & W1.edgeSeq() = W2.edgeSeq();
theorem :: GLIB_015:20
for G being _Graph, E being one-to-one ManySortedSet of the_Edges_of G
for W1 being Walk of G ex W2 being Walk of replaceEdges(E)
st W1.vertexSeq() = W2.vertexSeq() & E*(W1.edgeSeq()) = W2.edgeSeq();
theorem :: GLIB_015:21
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for W2 being Walk of replaceVerticesEdges(V,E) ex W1 being Walk of G
st V*(W1.vertexSeq()) = W2.vertexSeq() & E*(W1.edgeSeq()) = W2.edgeSeq();
theorem :: GLIB_015:22
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for W2 being Walk of replaceVertices(V) ex W1 being Walk of G
st V*(W1.vertexSeq()) = W2.vertexSeq() & W1.edgeSeq() = W2.edgeSeq();
theorem :: GLIB_015:23
for G being _Graph, E being one-to-one ManySortedSet of the_Edges_of G
for W2 being Walk of replaceEdges(E) ex W1 being Walk of G
st W1.vertexSeq() = W2.vertexSeq() & E*(W1.edgeSeq()) = W2.edgeSeq();
begin :: Graph selectors of Graph-yielding Functions
definition
let F be Graph-yielding Function;
func the_Vertices_of F -> Function means
:: GLIB_015:def 4
dom it = dom F &
for x being object st x in dom F
ex G being _Graph st G = F.x & it.x = the_Vertices_of G;
func the_Edges_of F -> Function means
:: GLIB_015:def 5
dom it = dom F &
for x being object st x in dom F
ex G being _Graph st G = F.x & it.x = the_Edges_of G;
func the_Source_of F -> Function means
:: GLIB_015:def 6
dom it = dom F &
for x being object st x in dom F
ex G being _Graph st G = F.x & it.x = the_Source_of G;
func the_Target_of F -> Function means
:: GLIB_015:def 7
dom it = dom F &
for x being object st x in dom F
ex G being _Graph st G = F.x & it.x = the_Target_of G;
end;
registration
let F be Graph-yielding Function;
cluster the_Source_of F -> Function-yielding;
cluster the_Target_of F -> Function-yielding;
end;
registration
let F be empty Graph-yielding Function;
cluster the_Vertices_of F -> empty;
cluster the_Edges_of F -> empty;
cluster the_Source_of F -> empty;
cluster the_Target_of F -> empty;
end;
registration
let F be non empty Graph-yielding Function;
cluster the_Vertices_of F -> non empty;
cluster the_Edges_of F -> non empty;
cluster the_Source_of F -> non empty;
cluster the_Target_of F -> non empty;
end;
registration
let F be Graph-yielding Function;
cluster the_Vertices_of F -> non-empty;
end;
definition
let F be non empty Graph-yielding Function;
redefine func the_Vertices_of F means
:: GLIB_015:def 8
dom it = dom F &
for x being Element of dom F holds it.x = the_Vertices_of (F.x);
redefine func the_Edges_of F means
:: GLIB_015:def 9
dom it = dom F &
for x being Element of dom F holds it.x = the_Edges_of (F.x);
redefine func the_Source_of F means
:: GLIB_015:def 10
dom it = dom F &
for x being Element of dom F holds it.x = the_Source_of (F.x);
redefine func the_Target_of F means
:: GLIB_015:def 11
dom it = dom F &
for x being Element of dom F holds it.x = the_Target_of (F.x);
end;
theorem :: GLIB_015:24
for F being Graph-yielding Function
holds the_Vertices_of rng F = rng the_Vertices_of F;
theorem :: GLIB_015:25
for F being Graph-yielding Function
holds the_Edges_of rng F = rng the_Edges_of F;
theorem :: GLIB_015:26
for F being Graph-yielding Function
holds the_Source_of rng F = rng the_Source_of F;
theorem :: GLIB_015:27
for F being Graph-yielding Function
holds the_Target_of rng F = rng the_Target_of F;
begin :: Isomorphisms between Graph-membered Sets or Graph-yielding Functions
definition
let S1, S2 be Graph-membered set;
pred S1, S2 are_Disomorphic means
:: GLIB_015:def 12
ex f being one-to-one Function st dom f = S1 & rng f = S2 &
for G being _Graph st G in S1 holds f.G is G-Disomorphic _Graph;
reflexivity;
symmetry;
pred S1, S2 are_isomorphic means
:: GLIB_015:def 13
ex f being one-to-one Function st dom f = S1 & rng f = S2 &
for G being _Graph st G in S1 holds f.G is G-isomorphic _Graph;
reflexivity;
symmetry;
end;
theorem :: GLIB_015:28
for S1, S2, S3 being Graph-membered set
st S1, S2 are_Disomorphic & S2, S3 are_Disomorphic
holds S1, S3 are_Disomorphic;
theorem :: GLIB_015:29
for S1, S2, S3 being Graph-membered set
st S1, S2 are_isomorphic & S2, S3 are_isomorphic
holds S1, S3 are_isomorphic;
theorem :: GLIB_015:30
for S1, S2 being Graph-membered set st S1, S2 are_Disomorphic
holds S1, S2 are_isomorphic;
theorem :: GLIB_015:31
for S1, S2 being Graph-membered set st S1, S2 are_Disomorphic
holds card S1 = card S2;
theorem :: GLIB_015:32
for S1, S2 being Graph-membered set st S1, S2 are_isomorphic
holds card S1 = card S2;
theorem :: GLIB_015:33
for S1, S2 being empty Graph-membered set holds S1, S2 are_Disomorphic;
theorem :: GLIB_015:34
for G1, G2 being _Graph
holds {G1}, {G2} are_Disomorphic iff G2 is G1-Disomorphic;
theorem :: GLIB_015:35
for G1, G2 being _Graph
holds {G1}, {G2} are_isomorphic iff G2 is G1-isomorphic;
theorem :: GLIB_015:36
for S1, S2 being Graph-membered set st S1,S2 are_isomorphic holds
(S1 is empty implies S2 is empty) &
(S1 is loopless implies S2 is loopless) &
(S1 is non-multi implies S2 is non-multi) &
(S1 is simple implies S2 is simple) &
(S1 is acyclic implies S2 is acyclic) &
(S1 is connected implies S2 is connected) &
(S1 is Tree-like implies S2 is Tree-like) &
(S1 is chordal implies S2 is chordal) &
(S1 is edgeless implies S2 is edgeless) &
(S1 is loopfull implies S2 is loopfull);
theorem :: GLIB_015:37
for S1, S2 being Graph-membered set st S1,S2 are_Disomorphic holds
(S1 is non-Dmulti implies S2 is non-Dmulti) &
(S1 is Dsimple implies S2 is Dsimple);
definition
let F1, F2 being Graph-yielding Function;
pred F1, F2 are_Disomorphic means
:: GLIB_015:def 14
ex p being one-to-one Function st dom p = dom F1 & rng p = dom F2 &
for x being object st x in dom F1
ex G1, G2 being _Graph st G1 = F1.x & G2 = F2.(p.x) & G2 is G1-Disomorphic;
reflexivity;
symmetry;
pred F1, F2 are_isomorphic means
:: GLIB_015:def 15
ex p being one-to-one Function st dom p = dom F1 & rng p = dom F2 &
for x being object st x in dom F1
ex G1, G2 being _Graph st G1 = F1.x & G2 = F2.(p.x) & G2 is G1-isomorphic;
reflexivity;
symmetry;
end;
theorem :: GLIB_015:38
for F1, F2 being non empty Graph-yielding Function st dom F1 = dom F2 &
for x1 being Element of dom F1, x2 being Element of dom F2 st x1 = x2
holds F2.x2 is F1.x1-Disomorphic
holds F1, F2 are_Disomorphic;
theorem :: GLIB_015:39
for F1, F2 being non empty Graph-yielding Function st dom F1 = dom F2 &
for x1 being Element of dom F1, x2 being Element of dom F2 st x1 = x2
holds F2.x2 is F1.x1-isomorphic
holds F1, F2 are_isomorphic;
theorem :: GLIB_015:40
for F1, F2, F3 being Graph-yielding Function
st F1, F2 are_Disomorphic & F2, F3 are_Disomorphic
holds F1, F3 are_Disomorphic;
theorem :: GLIB_015:41
for F1, F2, F3 being Graph-yielding Function
st F1, F2 are_isomorphic & F2, F3 are_isomorphic
holds F1, F3 are_isomorphic;
theorem :: GLIB_015:42
for F1, F2 being Graph-yielding Function
st F1, F2 are_Disomorphic holds F1, F2 are_isomorphic;
:: might require Proof outside this article
theorem :: GLIB_015:43
for F1, F2 being empty Graph-yielding Function
holds F1, F2 are_Disomorphic & F1, F2 are_isomorphic;
theorem :: GLIB_015:44
for F1, F2 being Graph-yielding Function
st F1, F2 are_Disomorphic holds card F1 = card F2;
theorem :: GLIB_015:45
for F1, F2 being Graph-yielding Function
st F1, F2 are_isomorphic holds card F1 = card F2;
theorem :: GLIB_015:46
for G1, G2 being _Graph, x,y being object
holds x .--> G1, y .--> G2 are_Disomorphic iff G2 is G1-Disomorphic;
theorem :: GLIB_015:47
for G1, G2 being _Graph, x,y being object
holds x .--> G1, y .--> G2 are_isomorphic iff G2 is G1-isomorphic;
theorem :: GLIB_015:48
for F1, F2 being Graph-yielding Function st F1, F2 are_isomorphic holds
(F1 is empty implies F2 is empty) &
(F1 is loopless implies F2 is loopless) &
(F1 is non-multi implies F2 is non-multi) &
(F1 is simple implies F2 is simple) &
(F1 is acyclic implies F2 is acyclic) &
(F1 is connected implies F2 is connected) &
(F1 is Tree-like implies F2 is Tree-like) &
(F1 is chordal implies F2 is chordal) &
(F1 is edgeless implies F2 is edgeless) &
(F1 is loopfull implies F2 is loopfull);
theorem :: GLIB_015:49
for F1, F2 being Graph-yielding Function st F1, F2 are_Disomorphic holds
(F1 is non-Dmulti implies F2 is non-Dmulti) &
(F1 is Dsimple implies F2 is Dsimple);
definition
let I be set, F1, F2 being Graph-yielding ManySortedSet of I;
redefine pred F1, F2 are_Disomorphic means
:: GLIB_015:def 16
ex p being Permutation of I st
for x being object st x in I
ex G1, G2 being _Graph st G1 = F1.x & G2 = F2.(p.x) & G2 is G1-Disomorphic;
reflexivity;
symmetry;
redefine pred F1, F2 are_isomorphic means
:: GLIB_015:def 17
ex p being Permutation of I st
for x being object st x in I
ex G1, G2 being _Graph st G1 = F1.x & G2 = F2.(p.x) & G2 is G1-isomorphic;
reflexivity;
symmetry;
end;
begin :: Distinguishing the Vertex and Edge Sets of several Graphs from each other
definition
let S being Graph-membered set;
attr S is vertex-disjoint means
:: GLIB_015:def 18
for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2
holds the_Vertices_of G1 misses the_Vertices_of G2;
attr S is edge-disjoint means
:: GLIB_015:def 19
for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2
holds the_Edges_of G1 misses the_Edges_of G2;
end;
:: might require Proof outside this article
theorem :: GLIB_015:50
for S being Graph-membered set holds S is vertex-disjoint edge-disjoint iff
for G1, G2 being _Graph st G1 in S & G2 in S & G1 <> G2
holds the_Vertices_of G1 misses the_Vertices_of G2 &
the_Edges_of G1 misses the_Edges_of G2;
registration
cluster trivial -> vertex-disjoint edge-disjoint for Graph-membered set;
cluster edgeless -> edge-disjoint for Graph-membered set;
cluster edge-disjoint -> \/-tolerating for Graph-membered set;
cluster vertex-disjoint \/-tolerating -> edge-disjoint
for Graph-membered set;
end;
registration
let G be _Graph;
cluster {G} -> vertex-disjoint edge-disjoint;
end;
theorem :: GLIB_015:51
for G1, G2 being _Graph holds {G1, G2} is vertex-disjoint
iff G1 = G2 or the_Vertices_of G1 misses the_Vertices_of G2;
theorem :: GLIB_015:52
for G1, G2 being _Graph holds {G1, G2} is edge-disjoint
iff G1 = G2 or the_Edges_of G1 misses the_Edges_of G2;
registration
cluster non empty \/-tolerating vertex-disjoint edge-disjoint acyclic
simple Dsimple loopless non-multi non-Dmulti for Graph-membered set;
end;
:: note that the other direction does not work,
:: for example take S = {G,H} with G == H <> G
registration
let S be vertex-disjoint Graph-membered set;
cluster the_Vertices_of S -> mutually-disjoint;
end;
registration
let S be edge-disjoint Graph-membered set;
cluster the_Edges_of S -> mutually-disjoint;
end;
registration
let S be vertex-disjoint Graph-membered set;
cluster -> vertex-disjoint for Subset of S;
end;
registration
let S1 be vertex-disjoint Graph-membered set;
let S2 be set;
cluster S1 /\ S2 -> vertex-disjoint;
cluster S1 \ S2 -> vertex-disjoint;
end;
registration
let S be edge-disjoint Graph-membered set;
cluster -> edge-disjoint for Subset of S;
end;
registration
let S1 be edge-disjoint Graph-membered set;
let S2 be set;
cluster S1 /\ S2 -> edge-disjoint;
cluster S1 \ S2 -> edge-disjoint;
end;
theorem :: GLIB_015:53
for S1, S2 being Graph-membered set st S1 \/ S2 is vertex-disjoint
holds S1 is vertex-disjoint & S2 is vertex-disjoint;
theorem :: GLIB_015:54
for S1, S2 being Graph-membered set st S1 \/ S2 is edge-disjoint
holds S1 is edge-disjoint & S2 is edge-disjoint;
theorem :: GLIB_015:55
for S1, S2 being vertex-disjoint GraphUnionSet
for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
st S1,S2 are_Disomorphic holds G2 is G1-Disomorphic;
theorem :: GLIB_015:56
for S1, S2 being vertex-disjoint GraphUnionSet
for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
st S1,S2 are_isomorphic
ex S3 being vertex-disjoint GraphUnionSet, E being Subset of the_Edges_of G2,
G3 being GraphUnion of S3
st S1,S3 are_Disomorphic & G3 is reverseEdgeDirections of G2, E;
theorem :: GLIB_015:57
for S1, S2 being vertex-disjoint GraphUnionSet
for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
st S1,S2 are_isomorphic holds G2 is G1-isomorphic;
theorem :: GLIB_015:58
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
for W being Walk of G ex H being Element of S st W is Walk of H;
theorem :: GLIB_015:59
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
st G is connected ex H being _Graph st S = {H};
theorem :: GLIB_015:60
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S holds
(S is non-multi iff G is non-multi) &
(S is non-Dmulti iff G is non-Dmulti) &
(S is acyclic iff G is acyclic);
theorem :: GLIB_015:61
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S holds
(S is simple iff G is simple) &
(S is Dsimple iff G is Dsimple);
registration
let S be vertex-disjoint non-multi GraphUnionSet;
cluster -> non-multi for GraphUnion of S;
end;
registration
let S be vertex-disjoint non-Dmulti GraphUnionSet;
cluster -> non-Dmulti for GraphUnion of S;
end;
registration
let S be vertex-disjoint simple GraphUnionSet;
cluster -> simple for GraphUnion of S;
end;
registration
let S be vertex-disjoint Dsimple GraphUnionSet;
cluster -> Dsimple for GraphUnion of S;
end;
registration
let S be vertex-disjoint acyclic GraphUnionSet;
cluster -> acyclic for GraphUnion of S;
end;
theorem :: GLIB_015:62
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
for H being Element of S holds H is inducedSubgraph of G, the_Vertices_of H;
theorem :: GLIB_015:63
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S holds
(S is chordal iff G is chordal) &
(S is loopfull iff G is loopfull);
theorem :: GLIB_015:64
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
for H being Element of S, v being Vertex of G, w being Vertex of H
st v = w holds G.reachableFrom(v) = H.reachableFrom(w);
theorem :: GLIB_015:65
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
holds G.componentSet()
= union the set of all H.componentSet() where H is Element of S;
theorem :: GLIB_015:66
for S being vertex-disjoint non empty Graph-membered set
holds the set of all H.componentSet() where H is Element of S
is mutually-disjoint;
theorem :: GLIB_015:67
for S being non empty connected Graph-membered set
holds the set of all H.componentSet() where H is Element of S
= SmallestPartition the_Vertices_of S;
theorem :: GLIB_015:68
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
holds card S c= G.numComponents();
theorem :: GLIB_015:69
for S being vertex-disjoint GraphUnionSet, G being GraphUnion of S
st S is connected holds card S = G.numComponents();
definition
let F be Graph-yielding Function;
attr F is vertex-disjoint means
:: GLIB_015:def 20
for x1,x2 being object st x1 in dom F & x2 in dom F & x1 <> x2
ex G1, G2 being _Graph st G1 = F.x1 & G2 = F.x2 &
the_Vertices_of G1 misses the_Vertices_of G2;
attr F is edge-disjoint means
:: GLIB_015:def 21
for x1,x2 being object st x1 in dom F & x2 in dom F & x1 <> x2
ex G1, G2 being _Graph st G1 = F.x1 & G2 = F.x2 &
the_Edges_of G1 misses the_Edges_of G2;
end;
:: note that edge-disjoint -> one-to-one doesn't hold because of edgeless graphs
registration
cluster trivial -> vertex-disjoint edge-disjoint for Graph-yielding Function;
cluster vertex-disjoint -> one-to-one for Graph-yielding Function;
end;
definition
let F be non empty Graph-yielding Function;
redefine attr F is vertex-disjoint means
:: GLIB_015:def 22
for x1,x2 being Element of dom F st x1 <> x2
holds the_Vertices_of (F.x1) misses the_Vertices_of (F.x2);
redefine attr F is edge-disjoint means
:: GLIB_015:def 23
for x1,x2 being Element of dom F st x1 <> x2
holds the_Edges_of (F.x1) misses the_Edges_of (F.x2);
end;
theorem :: GLIB_015:70
for F being non empty Graph-yielding Function holds F is vertex-disjoint iff
for x1,x2 being Element of dom F st x1 <> x2
holds (the_Vertices_of F).x1 misses (the_Vertices_of F).x2;
theorem :: GLIB_015:71
for F being non empty Graph-yielding Function holds F is edge-disjoint iff
for x1,x2 being Element of dom F st x1 <> x2
holds (the_Edges_of F).x1 misses (the_Edges_of F).x2;
:: might need Proof outside this article
theorem :: GLIB_015:72
for F being non empty Graph-yielding Function
holds F is vertex-disjoint edge-disjoint iff
for x1,x2 being Element of dom F st x1 <> x2
holds the_Vertices_of(F.x1) misses the_Vertices_of(F.x2) &
the_Edges_of(F.x1) misses the_Edges_of(F.x2);
theorem :: GLIB_015:73
for F being non empty Graph-yielding Function
holds F is vertex-disjoint edge-disjoint iff
for x1,x2 being Element of dom F st x1 <> x2
holds (the_Vertices_of F).x1 misses (the_Vertices_of F).x2 &
(the_Edges_of F).x1 misses (the_Edges_of F).x2;
registration
let x be object, G be _Graph;
cluster x .--> G -> vertex-disjoint edge-disjoint;
end;
registration
let G be _Graph;
cluster <* G *> -> vertex-disjoint edge-disjoint;
end;
registration
cluster non empty vertex-disjoint edge-disjoint for Graph-yielding Function;
end;
registration
let F be vertex-disjoint Graph-yielding Function;
cluster rng F -> vertex-disjoint;
end;
registration
let F be edge-disjoint Graph-yielding Function;
cluster rng F -> edge-disjoint;
end;
theorem :: GLIB_015:74
for F1, F2 being non empty one-to-one Graph-yielding Function
st F1, F2 are_Disomorphic holds rng F1, rng F2 are_Disomorphic;
theorem :: GLIB_015:75
for F1, F2 being non empty one-to-one Graph-yielding Function
st F1, F2 are_isomorphic holds rng F1, rng F2 are_isomorphic;
theorem :: GLIB_015:76
for G1, G2 being _Graph holds <* G1, G2 *> is vertex-disjoint iff
the_Vertices_of G1 misses the_Vertices_of G2;
theorem :: GLIB_015:77
for G1, G2 being _Graph holds <* G1, G2 *> is edge-disjoint iff
the_Edges_of G1 misses the_Edges_of G2;
begin :: Distinguishing the Range of a Graph-yielding Function
definition
let f be Function, x be object;
func renameElementsDistinctlyFunc(f,x) -> ManySortedSet of f.x equals
:: GLIB_015:def 24
<: f.x --> [f,x], id(f.x) :>;
end;
theorem :: GLIB_015:78
for f being Function, x, y being object st x in dom f & y in f.x
holds renameElementsDistinctlyFunc(f,x).y = [f,x,y];
theorem :: GLIB_015:79
for f being Function, x, z being object
st x in dom f & z in rng renameElementsDistinctlyFunc(f,x)
ex y being object st y in f.x & z = [f,x,y];
theorem :: GLIB_015:80
for f being Function, x being object
holds rng renameElementsDistinctlyFunc(f,x) = [: {[f,x]}, f.x :];
theorem :: GLIB_015:81
for f being Function, x1, x2 being object
holds rng renameElementsDistinctlyFunc(f,x1) misses f.x2;
theorem :: GLIB_015:82
for f being Function, x1, x2 being object st x1 <> x2
holds rng renameElementsDistinctlyFunc(f,x1) misses
rng renameElementsDistinctlyFunc(f,x2);
registration
let f be Function, x be object;
cluster renameElementsDistinctlyFunc(f,x) -> one-to-one;
end;
registration
let f be empty Function, x be object;
cluster renameElementsDistinctlyFunc(f,x) -> empty;
end;
registration
let f be non empty non-empty Function, x be Element of dom f;
cluster renameElementsDistinctlyFunc(f,x) -> non empty;
end;
registration
let F be non empty Graph-yielding Function, x be Element of dom F;
cluster renameElementsDistinctlyFunc(the_Vertices_of F,x)
-> non empty (the_Vertices_of (F.x))-defined;
cluster renameElementsDistinctlyFunc(the_Edges_of F,x)
-> (the_Edges_of (F.x))-defined;
end;
registration
let F be non empty Graph-yielding Function, x be Element of dom F;
cluster renameElementsDistinctlyFunc(the_Vertices_of F,x)
-> total for (the_Vertices_of (F.x))-defined Function;
cluster renameElementsDistinctlyFunc(the_Edges_of F,x)
-> total for (the_Edges_of (F.x))-defined Function;
end;
definition
let F be non empty Graph-yielding Function;
:: canonical distinction of the graph yielding function
func canGFDistinction(F) -> Graph-yielding Function means
:: GLIB_015:def 25
dom it = dom F & for x being Element of dom F holds
it.x = replaceVerticesEdges(
renameElementsDistinctlyFunc(the_Vertices_of F,x),
renameElementsDistinctlyFunc(the_Edges_of F,x));
end;
registration
let F be non empty Graph-yielding Function;
cluster canGFDistinction(F) -> non empty;
end;
registration
let F be non empty Graph-yielding Function;
cluster canGFDistinction(F) -> plain;
end;
theorem :: GLIB_015:83
for F being non empty Graph-yielding Function, x being Element of dom F
holds (the_Vertices_of canGFDistinction F).x
= [: {[the_Vertices_of F,x]}, (the_Vertices_of F).x :];
theorem :: GLIB_015:84
for F being non empty Graph-yielding Function, x being Element of dom F
holds (the_Edges_of canGFDistinction F).x
= [: {[the_Edges_of F,x]}, (the_Edges_of F).x :];
registration
let F be non empty Graph-yielding Function;
cluster canGFDistinction(F) -> vertex-disjoint edge-disjoint;
end;
theorem :: GLIB_015:85
for F being non empty Graph-yielding Function, x being Element of dom F
for x9 being Element of dom canGFDistinction F st x = x9
ex G being PGraphMapping of F.x,(canGFDistinction F).x9
st G_V = renameElementsDistinctlyFunc(the_Vertices_of F,x) &
G_E = renameElementsDistinctlyFunc(the_Edges_of F,x) &
G is Disomorphism;
theorem :: GLIB_015:86
for F being non empty Graph-yielding Function, x being Element of dom F
for x9 being Element of dom canGFDistinction F st x = x9
holds (canGFDistinction F).x9 is F.x-Disomorphic;
theorem :: GLIB_015:87
for F being non empty Graph-yielding Function
holds F,canGFDistinction(F) are_Disomorphic;
theorem :: GLIB_015:88
for F1, F2 being non empty Graph-yielding Function st F1, F2 are_Disomorphic
holds canGFDistinction(F1),canGFDistinction(F2) are_Disomorphic;
theorem :: GLIB_015:89
for F1, F2 being non empty Graph-yielding Function st F1, F2 are_isomorphic
holds canGFDistinction(F1),canGFDistinction(F2) are_isomorphic;
theorem :: GLIB_015:90
for F being non empty Graph-yielding Function, x being Element of dom F
for x9 being Element of dom canGFDistinction(F)
for v,e,w being object st x = x9
holds e DJoins v,w,F.x implies [the_Edges_of F,x,e] DJoins
[the_Vertices_of F,x,v],[the_Vertices_of F,x,w],(canGFDistinction F).x9;
theorem :: GLIB_015:91
for F being non empty Graph-yielding Function, x being Element of dom F
for x9 being Element of dom canGFDistinction(F)
for v,e,w being object st x = x9
holds e Joins v,w,F.x implies [the_Edges_of F,x,e] Joins
[the_Vertices_of F,x,v],[the_Vertices_of F,x,w],(canGFDistinction F).x9;
theorem :: GLIB_015:92
for F being non empty Graph-yielding Function, x being Element of dom F
for x9 being Element of dom canGFDistinction(F)
for v9,e9,w9 being object st x = x9 & e9 DJoins v9,w9,(canGFDistinction F).x9
ex v,e,w being object st e DJoins v,w,F.x &
e9 = [the_Edges_of F,x,e] & v9 = [the_Vertices_of F,x,v] &
w9 = [the_Vertices_of F,x,w];
theorem :: GLIB_015:93
for F being non empty Graph-yielding Function, x being Element of dom F
for x9 being Element of dom canGFDistinction(F)
for v9,e9,w9 being object st x = x9 & e9 Joins v9,w9,(canGFDistinction F).x9
ex v,e,w being object st e Joins v,w,F.x &
e9 = [the_Edges_of F,x,e] & v9 = [the_Vertices_of F,x,v] &
w9 = [the_Vertices_of F,x,w];
registration
let F be non empty loopless Graph-yielding Function;
cluster canGFDistinction(F) -> loopless;
end;
registration
let F be non empty non loopless Graph-yielding Function;
cluster canGFDistinction(F) -> non loopless;
end;
registration
let F be non empty non-multi Graph-yielding Function;
cluster canGFDistinction(F) -> non-multi;
end;
registration
let F be non empty non non-multi Graph-yielding Function;
cluster canGFDistinction(F) -> non non-multi;
end;
registration
let F be non empty non-Dmulti Graph-yielding Function;
cluster canGFDistinction(F) -> non-Dmulti;
end;
registration
let F be non empty non non-Dmulti Graph-yielding Function;
cluster canGFDistinction(F) -> non non-Dmulti;
end;
registration
let F be non empty simple Graph-yielding Function;
cluster canGFDistinction(F) -> simple;
end;
registration
let F be non empty Dsimple Graph-yielding Function;
cluster canGFDistinction(F) -> Dsimple;
end;
registration
let F be non empty acyclic Graph-yielding Function;
cluster canGFDistinction(F) -> acyclic;
end;
registration
let F be non empty non acyclic Graph-yielding Function;
cluster canGFDistinction(F) -> non acyclic;
end;
registration
let F be non empty connected Graph-yielding Function;
cluster canGFDistinction(F) -> connected;
end;
registration
let F be non empty non connected Graph-yielding Function;
cluster canGFDistinction(F) -> non connected;
end;
registration
let F be non empty Tree-like Graph-yielding Function;
cluster canGFDistinction(F) -> Tree-like;
end;
registration
let F be non empty edgeless Graph-yielding Function;
cluster canGFDistinction(F) -> edgeless;
end;
registration
let F be non empty non edgeless Graph-yielding Function;
cluster canGFDistinction(F) -> non edgeless;
end;
definition
let F be non empty Graph-yielding Function, z be Element of dom F;
func canGFDistinction(F,z) -> Graph-yielding Function equals
:: GLIB_015:def 26
canGFDistinction(F) +* (z,F.z | _GraphSelectors);
end;
registration
let F be non empty Graph-yielding Function, z be Element of dom F;
cluster canGFDistinction(F,z) -> non empty;
end;
theorem :: GLIB_015:94
for F being non empty Graph-yielding Function, z being Element of dom F
holds dom F = dom canGFDistinction(F,z);
theorem :: GLIB_015:95
for F being non empty Graph-yielding Function, z being Element of dom F
for G being Graph-yielding Function
holds G = canGFDistinction(F,z) iff dom G = dom F &
G.z = F.z | _GraphSelectors &
for x being Element of dom F st x <> z
holds G.x = replaceVerticesEdges(
renameElementsDistinctlyFunc(the_Vertices_of F,x),
renameElementsDistinctlyFunc(the_Edges_of F,x));
theorem :: GLIB_015:96
for F being non empty Graph-yielding Function, z being Element of dom F
holds canGFDistinction(F,z).z = F.z | _GraphSelectors;
registration
let F being non empty Graph-yielding Function, z being Element of dom F;
cluster canGFDistinction(F,z) -> plain;
end;
theorem :: GLIB_015:97
for F being non empty Graph-yielding Function, z being Element of dom F
holds (the_Vertices_of canGFDistinction(F,z)).z = (the_Vertices_of F).z;
theorem :: GLIB_015:98
for F being non empty Graph-yielding Function, x,z being Element of dom F
st x <> z holds (the_Vertices_of canGFDistinction(F,z)).x
= (the_Vertices_of canGFDistinction F).x;
theorem :: GLIB_015:99
for F being non empty Graph-yielding Function, z being Element of dom F
holds the_Vertices_of canGFDistinction(F,z)
= (the_Vertices_of canGFDistinction F) +* (z, the_Vertices_of (F.z));
theorem :: GLIB_015:100
for F being non empty Graph-yielding Function, z being Element of dom F
holds (the_Edges_of canGFDistinction(F,z)).z = (the_Edges_of F).z;
theorem :: GLIB_015:101
for F being non empty Graph-yielding Function, x,z being Element of dom F
st x <> z holds (the_Edges_of canGFDistinction(F,z)).x
= (the_Edges_of canGFDistinction F).x;
theorem :: GLIB_015:102
for F being non empty Graph-yielding Function, z being Element of dom F
holds (the_Edges_of canGFDistinction(F,z))
= (the_Edges_of canGFDistinction F) +* (z, the_Edges_of (F.z));
registration
let F be non empty Graph-yielding Function, z being Element of dom F;
cluster canGFDistinction(F,z) -> vertex-disjoint edge-disjoint;
end;
theorem :: GLIB_015:103
for F being non empty Graph-yielding Function, x,z being Element of dom F
for x9 being Element of dom canGFDistinction(F,z) st x <> z & x = x9
ex G being PGraphMapping of F.x,(canGFDistinction(F,z)).x9
st G_V = renameElementsDistinctlyFunc(the_Vertices_of F,x) &
G_E = renameElementsDistinctlyFunc(the_Edges_of F,x) &
G is Disomorphism;
theorem :: GLIB_015:104
for F being non empty Graph-yielding Function, x,z being Element of dom F
for x9 being Element of dom canGFDistinction(F,z) st x = x9
holds (canGFDistinction(F,z)).x9 is F.x-Disomorphic;
theorem :: GLIB_015:105
for F being non empty Graph-yielding Function, z being Element of dom F
holds F,canGFDistinction(F,z) are_Disomorphic;
theorem :: GLIB_015:106
for F being non empty Graph-yielding Function, z being Element of dom F
holds canGFDistinction(F),canGFDistinction(F,z) are_Disomorphic;
theorem :: GLIB_015:107
for F1, F2 being non empty Graph-yielding Function
for z1 being Element of dom F1, z2 being Element of dom F2
st F1, F2 are_Disomorphic
holds canGFDistinction(F1,z1),canGFDistinction(F2,z2) are_Disomorphic;
theorem :: GLIB_015:108
for F being non empty Graph-yielding Function, z being Element of dom F
for z9 being Element of dom canGFDistinction(F,z)
for v,e,w being object st z = z9
holds e DJoins v,w,F.z iff e DJoins v,w,canGFDistinction(F,z).z9;
theorem :: GLIB_015:109
for F being non empty Graph-yielding Function, z being Element of dom F
for z9 being Element of dom canGFDistinction(F,z)
for v,e,w being object st z = z9
holds e Joins v,w,F.z iff e Joins v,w,canGFDistinction(F,z).z9;
theorem :: GLIB_015:110
for F being non empty Graph-yielding Function, x,z being Element of dom F
for x9 being Element of dom canGFDistinction(F,z)
for v,e,w being object st x <> z & x = x9
holds e DJoins v,w,F.x implies [the_Edges_of F,x,e] DJoins
[the_Vertices_of F,x,v],[the_Vertices_of F,x,w],(canGFDistinction(F,z)).x9;
theorem :: GLIB_015:111
for F being non empty Graph-yielding Function, x,z being Element of dom F
for x9 being Element of dom canGFDistinction(F,z)
for v,e,w being object st x <> z & x = x9
holds e Joins v,w,F.x implies [the_Edges_of F,x,e] Joins
[the_Vertices_of F,x,v],[the_Vertices_of F,x,w],(canGFDistinction(F,z)).x9;
theorem :: GLIB_015:112
for F being non empty Graph-yielding Function, x,z being Element of dom F
for x9 being Element of dom canGFDistinction(F,z)
for v9,e9,w9 being object
st x <> z & x = x9 & e9 DJoins v9,w9,(canGFDistinction(F,z)).x9
ex v,e,w being object st e DJoins v,w,F.x &
e9 = [the_Edges_of F,x,e] & v9 = [the_Vertices_of F,x,v] &
w9 = [the_Vertices_of F,x,w];
theorem :: GLIB_015:113
for F being non empty Graph-yielding Function, x,z being Element of dom F
for x9 being Element of dom canGFDistinction(F,z)
for v9,e9,w9 being object
st x <> z & x = x9 & e9 Joins v9,w9,(canGFDistinction(F,z)).x9
ex v,e,w being object st e Joins v,w,F.x &
e9 = [the_Edges_of F,x,e] & v9 = [the_Vertices_of F,x,v] &
w9 = [the_Vertices_of F,x,w];
registration
let F be non empty loopless Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> loopless;
end;
registration
let F be non empty non loopless Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non loopless;
end;
registration
let F be non empty non-multi Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non-multi;
end;
registration
let F be non empty non non-multi Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non non-multi;
end;
registration
let F be non empty non-Dmulti Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non-Dmulti;
end;
registration
let F be non empty non non-Dmulti Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non non-Dmulti;
end;
registration
let F be non empty simple Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> simple;
end;
registration
let F be non empty Dsimple Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> Dsimple;
end;
registration
let F be non empty acyclic Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> acyclic;
end;
registration
let F be non empty non acyclic Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non acyclic;
end;
registration
let F be non empty connected Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> connected;
end;
registration
let F be non empty non connected Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non connected;
end;
registration
let F be non empty Tree-like Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> Tree-like;
end;
registration
let F be non empty edgeless Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> edgeless;
end;
registration
let F be non empty non edgeless Graph-yielding Function;
let z be Element of dom F;
cluster canGFDistinction(F,z) -> non edgeless;
end;
theorem :: GLIB_015:114
for G2, H being _Graph, F being PGraphMapping of G2, H
st F is directed weak_SG-embedding
ex G1 being Supergraph of G2 st G1 is H-Disomorphic;
theorem :: GLIB_015:115
for G2, H being _Graph, F being PGraphMapping of G2, H
st F is weak_SG-embedding ex G1 being Supergraph of G2 st G1 is H-isomorphic;
begin :: The Sum of Graphs
definition
let F be non empty Graph-yielding Function;
mode GraphSum of F -> _Graph means
:: GLIB_015:def 27
ex G9 being GraphUnion of rng canGFDistinction(F) st it is G9-Disomorphic;
end;
theorem :: GLIB_015:116
for F being non empty Graph-yielding Function, S being GraphSum of F
for G9 being GraphUnion of rng canGFDistinction(F)
holds S is G9-Disomorphic;
theorem :: GLIB_015:117
for F1, F2 being non empty Graph-yielding Function
for S1 being GraphSum of F1, S2 being GraphSum of F2
st F1, F2 are_Disomorphic holds S2 is S1-Disomorphic;
theorem :: GLIB_015:118
for F1, F2 being non empty Graph-yielding Function
for S1 being GraphSum of F1, S2 being GraphSum of F2
st F1, F2 are_isomorphic holds S2 is S1-isomorphic;
theorem :: GLIB_015:119
for F being non empty Graph-yielding Function, S1, S2 being GraphSum of F
holds S2 is S1-Disomorphic;
:: theorem
:: for F, G being non empty Graph-yielding Function, R being GraphUnionSet
:: for S being GraphUnion of R
:: st R = rng G & G,canGFDistinction(F) are_Disomorphic
:: holds S is GraphSum of F;
theorem :: GLIB_015:120
for x being object, G being _Graph, S being GraphSum of x .--> G
holds S is G-Disomorphic;
theorem :: GLIB_015:121
for F being non empty Graph-yielding Function, S being GraphSum of F
st S is connected
ex x being object, G being connected _Graph st F = x .--> G;
registration
let X be non empty set;
cluster non empty vertex-disjoint edge-disjoint
for Graph-yielding ManySortedSet of X;
end;
theorem :: GLIB_015:122
for F being non empty Graph-yielding Function, x being Element of dom F
for S being GraphSum of F
ex M being PGraphMapping of F.x,S st M is strong_SG-embedding;
:: This is a possible generalization of the preceeding theorem.
:: :: A graph sum can be divided into its (direct, not isomorphic) parts.
:: theorem
:: for F1 being non empty Graph-yielding Function, S being GraphSum of F1
:: ex F2 being non empty vertex-disjoint edge-disjoint
:: Graph-yielding ManySortedSet of dom F1
:: st S is GraphUnion of rng F2 &
:: for x being Element of dom F1 holds F2.x is F1.x-Disomorphic
:: proof
:: let F1 be non empty Graph-yielding Function, S be GraphSum of F1;
:: :: construct function from dom F1 to a Disomorphism from F1.x to GFD(F1).x |H1
:: :: construct function from dom F1 to injection from GFD(F1).x into G9 |H2
:: :: the Disomorphism from G9 to S |F
:: :: set F2.x = rng (F*(H2.x)*(H1.x))
:: :: show F2.x is Disomorphism from F1.x to F2.x
:: :: show F2 is vertex-disjoint
:: :: show F2 is edge-disjoint
:: :: show S is GraphUnion
:: thus thesis;
:: end;
theorem :: GLIB_015:123
for F being non empty Graph-yielding Function, z being Element of dom F
ex S being GraphSum of F st S is Supergraph of F.z &
S is GraphUnion of rng canGFDistinction(F,z);
theorem :: GLIB_015:124
for F being non empty Graph-yielding Function, S being GraphSum of F holds
(F is loopless iff S is loopless) &
(F is non-multi iff S is non-multi) &
(F is non-Dmulti iff S is non-Dmulti) &
(F is simple iff S is simple) &
(F is Dsimple iff S is Dsimple) &
(F is chordal iff S is chordal) &
(F is edgeless iff S is edgeless) &
(F is loopfull iff S is loopfull);
registration
let F be non empty loopless Graph-yielding Function;
cluster -> loopless for GraphSum of F;
end;
registration
let F be non empty non loopless Graph-yielding Function;
cluster -> non loopless for GraphSum of F;
end;
registration
let F be non empty non-Dmulti Graph-yielding Function;
cluster -> non-Dmulti for GraphSum of F;
end;
registration
let F be non empty non non-Dmulti Graph-yielding Function;
cluster -> non non-Dmulti for GraphSum of F;
end;
registration
let F be non empty non-multi Graph-yielding Function;
cluster -> non-multi for GraphSum of F;
end;
registration
let F be non empty non non-multi Graph-yielding Function;
cluster -> non non-multi for GraphSum of F;
end;
registration
let F be non empty simple Graph-yielding Function;
cluster -> simple for GraphSum of F;
end;
registration
let F be non empty Dsimple Graph-yielding Function;
cluster -> Dsimple for GraphSum of F;
end;
registration
let F be non empty edgeless Graph-yielding Function;
cluster -> edgeless for GraphSum of F;
end;
registration
let F be non empty non edgeless Graph-yielding Function;
cluster -> non edgeless for GraphSum of F;
end;
registration
let F be non empty loopfull Graph-yielding Function;
cluster -> loopfull for GraphSum of F;
end;
registration
let F be non empty non loopfull Graph-yielding Function;
cluster -> non loopfull for GraphSum of F;
end;
theorem :: GLIB_015:125
for F being non empty Graph-yielding Function, S being GraphSum of F holds
(F is acyclic iff S is acyclic) &
(F is chordal iff S is chordal);
registration
let F be non empty acyclic Graph-yielding Function;
cluster -> acyclic for GraphSum of F;
end;
registration
let F be non empty non acyclic Graph-yielding Function;
cluster -> non acyclic for GraphSum of F;
end;
theorem :: GLIB_015:126
for F being non empty Graph-yielding Function, S being GraphSum of F
holds card F c= S.numComponents();
theorem :: GLIB_015:127
for F being non empty connected Graph-yielding Function,S being GraphSum of F
holds card F = S.numComponents();
begin :: The Sum of two Graphs
definition
let G1, G2 be _Graph;
mode GraphSum of G1, G2 -> Supergraph of G1 means
:: GLIB_015:def 28
it is GraphSum of <* G1, G2 *>;
end;
theorem :: GLIB_015:128
for G1, G2 being _Graph, S being GraphSum of G1, G2 holds
(G1 is loopless & G2 is loopless iff S is loopless) &
(G1 is non-multi & G2 is non-multi iff S is non-multi) &
(G1 is non-Dmulti & G2 is non-Dmulti iff S is non-Dmulti) &
(G1 is simple & G2 is simple iff S is simple) &
(G1 is Dsimple & G2 is Dsimple iff S is Dsimple) &
(G1 is acyclic & G2 is acyclic iff S is acyclic) &
(G1 is chordal & G2 is chordal iff S is chordal) &
(G1 is edgeless & G2 is edgeless iff S is edgeless) &
(G1 is loopfull & G2 is loopfull iff S is loopfull);
registration
let G1, G2 be loopless _Graph;
cluster -> loopless for GraphSum of G1, G2;
end;
registration
let G1, G2 be non loopless _Graph;
cluster -> non loopless for GraphSum of G1, G2;
end;
registration
let G1, G2 be non-Dmulti _Graph;
cluster -> non-Dmulti for GraphSum of G1, G2;
end;
registration
let G1, G2 be non non-Dmulti _Graph;
cluster -> non non-Dmulti for GraphSum of G1, G2;
end;
registration
let G1, G2 be non-multi _Graph;
cluster -> non-multi for GraphSum of G1, G2;
end;
registration
let G1, G2 be non non-multi _Graph;
cluster -> non non-multi for GraphSum of G1, G2;
end;
registration
let G1, G2 be simple _Graph;
cluster -> simple for GraphSum of G1, G2;
end;
registration
let G1, G2 be Dsimple _Graph;
cluster -> Dsimple for GraphSum of G1, G2;
end;
registration
let G1, G2 be acyclic _Graph;
cluster -> acyclic for GraphSum of G1, G2;
end;
registration
let G1, G2 be non acyclic _Graph;
cluster -> non acyclic for GraphSum of G1, G2;
end;
registration
let G1, G2 be edgeless _Graph;
cluster -> edgeless for GraphSum of G1, G2;
end;
registration
let G1, G2 be non edgeless _Graph;
cluster -> non edgeless for GraphSum of G1, G2;
end;
registration
let G1, G2 be loopfull _Graph;
cluster -> loopfull for GraphSum of G1, G2;
end;
registration
let G1, G2 be non loopfull _Graph;
cluster -> non loopfull for GraphSum of G1, G2;
end;
theorem :: GLIB_015:129
for G1, G2 being _Graph, S being GraphSum of G1, G2
holds S.order() = G1.order() +` G2.order();
theorem :: GLIB_015:130
for G1, G2 being _Graph, S being GraphSum of G1, G2
holds S.size() = G1.size() +` G2.size();
theorem :: GLIB_015:131
for G1, G2 being _Graph, S being GraphSum of G1, G2
holds S.numComponents() = G1.numComponents() +` G2.numComponents();