:: Underlying Simple Graphs
:: 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, ZFMISC_1, RELAT_2,
GLIB_002, FUNCOP_1, GLIB_001, ABIAN, GLIB_003, GLIB_009, INT_1, RCOMP_1,
EQREL_1, GLIB_006, GLIB_007, FUNCT_4, CHORD, SCMYCIEL, SGRAPH1, GRAPH_1,
ORDINAL4, XCMPLX_0, REWRITE1;
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, CARD_1, PBOOLE, 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, CHORD, GLIB_006,
GLIB_007, GLIB_008, 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;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
FINSEQ_1, GLIB_000, GLIB_003, INT_1, CARD_1, FUNCT_2, PARTFUN1, RELSET_1,
GLIB_001, ABIAN, FINSEQ_4, GLIB_006, GLIB_008, CHORD;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: Preliminaries
:: into XBOOLE_1 ?
theorem :: GLIB_009:1
for X, Y being set st Y c= X holds X \ (X \ Y) = Y;
:: into RELAT_1 ?
theorem :: GLIB_009:2
for R being Relation, X being set holds (R|X)~ = X|`(R~) & (X|`R)~ = (R~)|X;
::$CT
:: into FUNCT_1 ?
:: reformulation of FUNCT_1:113
theorem :: GLIB_009:4
for f being Function, Y being set holds Y|`f = f|dom(Y|`f);
:: into FUNCT_1 ?
theorem :: GLIB_009:5
for f being one-to-one Function, X being set
holds (f|X)" = X|`(f") & (X|`f)" = (f")|X;
:: BEGIN into GLIB_000 ?
theorem :: GLIB_009:6
for G being _Graph, e,x1,y1,x2,y2 being object
holds e DJoins x1,y1,G & e DJoins x2,y2,G implies x1 = x2 & y1 = y2;
registration
let G be _trivial _Graph;
cluster the_Vertices_of G -> trivial;
end;
registration
cluster _trivial non-Dmulti -> non-multi for _Graph;
let G be _trivial non-Dmulti _Graph;
cluster the_Edges_of G -> trivial;
end;
theorem :: GLIB_009:7
for G being _Graph, X,Y being set, e,x,y being object
holds e DJoins x,y,G & x in X & y in Y implies e DSJoins X,Y,G;
theorem :: GLIB_009:8
for G being _trivial _Graph, H being _Graph
st the_Vertices_of H c= the_Vertices_of G & the_Edges_of H c= the_Edges_of G
holds H is _trivial & H is Subgraph of G;
theorem :: GLIB_009:9
for G being _Graph holds G == G | _GraphSelectors;
theorem :: GLIB_009:10
for G being _Graph, X,Y being set, e being object
holds e SJoins X,Y,G iff e SJoins Y,X,G;
theorem :: GLIB_009:11
for G being _Graph, X,Y being set, e being object
holds e SJoins X,Y,G iff (e DSJoins X,Y,G or e DSJoins Y,X,G);
theorem :: GLIB_009:12
for G being _Graph, e,v,w being object
st e SJoins {v},{w},G holds e Joins v,w,G;
theorem :: GLIB_009:13
for G being _Graph, e,v,w being object
st e DSJoins {v},{w},G holds e DJoins v,w,G;
theorem :: GLIB_009:14
for G being _Graph, v,w being object st v <> w
holds G.edgesDBetween({v},{w}) misses G.edgesDBetween({w},{v}) &
G.edgesBetween({v},{w})
= G.edgesDBetween({v},{w}) \/ G.edgesDBetween({w},{v});
theorem :: GLIB_009:15
for G being _Graph, X being set
holds G.edgesBetween(X,X) = G.edgesDBetween(X,X);
theorem :: GLIB_009:16
for G being _Graph, X,Y being set
holds G.edgesBetween(X,Y) = G.edgesBetween(Y,X);
theorem :: GLIB_009:17
for G being _Graph holds G is loopless iff
for v being object holds not ex e being object st e DJoins v,v,G;
theorem :: GLIB_009:18
for G being _Graph holds G is loopless iff
for v being object holds not ex e being object st e SJoins {v},{v},G;
theorem :: GLIB_009:19
for G being _Graph holds G is loopless iff
for v being object holds not ex e being object st e DSJoins {v},{v},G;
theorem :: GLIB_009:20
for G being _Graph holds G is loopless iff
for v being object holds G.edgesBetween({v},{v}) = {};
theorem :: GLIB_009:21
for G being _Graph holds G is loopless iff
for v being object holds G.edgesDBetween({v},{v}) = {};
registration
let G be loopless _Graph, v be object;
cluster G.edgesBetween({v},{v}) -> empty;
cluster G.edgesDBetween({v},{v}) -> empty;
end;
theorem :: GLIB_009:22
for G being _Graph holds G is non-multi iff
for v,w being object holds G.edgesBetween({v},{w}) is trivial;
registration
let G be non-multi _Graph, v, w be object;
cluster G.edgesBetween({v},{w}) -> trivial;
end;
theorem :: GLIB_009:23
for G being _Graph holds G is non-Dmulti iff
for v,w being object holds G.edgesDBetween({v},{w}) is trivial;
registration
let G be non-Dmulti _Graph, v, w be object;
cluster G.edgesDBetween({v},{w}) -> trivial;
end;
registration
let G be non _trivial _Graph;
cluster spanning -> non _trivial for Subgraph of G;
end;
registration
let G be _Graph;
cluster isolated -> non endvertex for Vertex of G;
end;
:: END into GLIB_000 ?
:: into GLIB_001 ?
theorem :: GLIB_009:24
for G being _Graph, v being Vertex of G
holds G.walkOf(v).edgeSeq() = <*>the_Edges_of G;
:: into GLIB_001 ?
theorem :: GLIB_009:25
for G being _Graph, v being Vertex of G
holds G.walkOf(v).edges() = {};
:: into GLIB_001
registration
let G be _Graph, W be trivial Walk of G;
cluster W.edges() -> empty trivial;
end;
:: into GLIB_001 ?
registration
let G be _Graph, W be Walk of G;
cluster W.vertices() -> non empty;
end;
:: into GLIB_001 ?
theorem :: GLIB_009:26
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() & W1.edgeSeq() = W2.edgeSeq()
holds W1 = W2;
:: into GLIB_001 ?
theorem :: GLIB_009:27
for G being _Graph, p being FinSequence of the_Vertices_of G,
q being FinSequence of the_Edges_of G
st len p = 1 + len q & for n being Element of NAT
st 1 <= n & n+1 <= len p holds q.n Joins p.n, p.(n+1), G
holds ex W being Walk of G st W.vertexSeq() = p & W.edgeSeq() = q;
:: into GLIB_001 ?
theorem :: GLIB_009:28
for G being _Graph, W being Walk of G holds len W.vertexSeq() = W.length()+1;
:: into GLIB_001 ?
theorem :: GLIB_009:29
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
for n being odd Nat st W1.vertexSeq() = W2.vertexSeq() holds W1.n = W2.n;
:: into GLIB_001 ?
theorem :: GLIB_009:30
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() holds
len W1 = len W2 & W1.length() = W2.length() &
W1.first() = W2.first() & W1.last() = W2.last() &
W2 is_Walk_from W1.first(),W1.last();
:: into GLIB_001 ?
theorem :: GLIB_009:31
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() holds
(W1 is non trivial implies W2 is non trivial) &
(W1 is closed implies W2 is closed);
:: into GLIB_001 ?
:: in the case len W1 = 5, W1 could be the Path in a dipole visiting both
:: edges while W2 goes back on the same edge it came from
theorem :: GLIB_009:32
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st W1.vertexSeq() = W2.vertexSeq() & len W1 <> 5 holds
(W1 is Path-like implies W2 is Path-like) &
(W1 is Cycle-like implies W2 is Cycle-like);
:: into GLIB_001 ?
scheme :: GLIB_009:sch 1
IndWalk {G() -> _Graph, P[Walk of G()]} : for W being Walk of G() holds P[W]
provided
for W being trivial Walk of G() holds P[W] and
for W being Walk of G(), e being object st e in W.last().edgesInOut() &
P[W] holds P[W.addEdge(e)];
:: into GLIB_001 ?
scheme :: GLIB_009:sch 2
IndDWalk {G() -> _Graph, P[Walk of G()]} :
for W being DWalk of G() holds P[W]
provided
for W being trivial DWalk of G() holds P[W] and
for W being DWalk of G(), e being object
st e in W.last().edgesOut() & P[W] holds P[W.addEdge(e)];
:: into GLIB_002 ?
theorem :: GLIB_009:33
for G1 being _Graph, E being Subset of the_Edges_of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E
st G2 is connected holds G1 is connected;
:: into GLIB_002 ?
theorem :: GLIB_009:34
for G1 being _Graph, E being set, G2 being removeEdges of G1, E
st G2 is connected holds G1 is connected;
:: into GLIB_002 ?
registration
let G1 be non connected _Graph, E be set;
cluster -> non connected for removeEdges of G1, E;
end;
:: into GLIB_002 ?
theorem :: GLIB_009:35
for G1 being _Graph, G2 being Subgraph of G1
st (for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last())
holds
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
:: into GLIB_002 ?
theorem :: GLIB_009:36
for G1 being _Graph, G2 being Subgraph of G1
st (for W1 being Walk of G1 ex W2 being Walk of G2
st W2 is_Walk_from W1.first(),W1.last())
holds G1 is connected implies G2 is connected;
:: into GLIB_002 ?
theorem :: GLIB_009:37
for G1 being _Graph, G2 being spanning Subgraph of G1
st (for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2))
holds G1.componentSet() = G2.componentSet();
:: into GLIB_002 ?
theorem :: GLIB_009:38
for G1 being _Graph, G2 being spanning Subgraph of G1
st (for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2))
holds G1.numComponents() = G2.numComponents();
:: into CHORD ?
theorem :: GLIB_009:39
for G being _Graph holds G is loopless iff
for v being Vertex of G holds not v,v are_adjacent;
registration
let G be non complete _Graph;
cluster spanning -> non complete for Subgraph of G;
end;
:: into GLIB_006 ?
theorem :: GLIB_009:40
for G2, G3 being _Graph, G1 being Supergraph of G3
st G1 == G2 holds G2 is Supergraph of G3;
theorem :: GLIB_009:41
for G2 being _Graph, V being set, G1 being addVertices of G2, V
for x,y being set, e being object holds
(e Joins x,y,G1 iff e Joins x,y,G2) &
(e DJoins x,y,G1 iff e DJoins x,y,G2) &
(e SJoins x,y,G1 iff e SJoins x,y,G2) &
(e DSJoins x,y,G1 iff e DSJoins x,y,G2);
:: into GLIB_007 ?
theorem :: GLIB_009:42
for G1, G2 being _Graph st G1 == G2
holds G2 is reverseEdgeDirections of G1, {};
:: into GLIB_007 ?
theorem :: GLIB_009:43
for G being _Graph holds G is reverseEdgeDirections of G, {};
begin :: Plain Graphs
definition
let G be _Graph;
attr G is plain means
:: GLIB_009:def 1
dom G = _GraphSelectors;
end;
registration
let G be _Graph;
cluster G|(_GraphSelectors) -> plain;
end;
registration
let V be non empty set, E be set, S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> plain;
end;
registration
let G be _Graph, X be set;
cluster G.set(WeightSelector, X) -> non plain;
cluster G.set(ELabelSelector, X) -> non plain;
cluster G.set(VLabelSelector, X) -> non plain;
end;
registration
cluster plain for _Graph;
end;
theorem :: GLIB_009:44
for G1, G2 being plain _Graph st G1 == G2 holds G1 = G2;
:: existence clusters for plain graph modes
registration
let G be _Graph;
cluster plain for Subgraph of G;
let V be set;
cluster plain for removeVertices of G, V;
let E be set;
cluster plain for inducedSubgraph of G, V, E;
end;
registration
let G be _Graph, E be set;
cluster plain for removeEdges of G, E;
cluster plain for reverseEdgeDirections of G, E;
end;
registration
let G be _Graph, v be set;
cluster plain for removeVertex of G, v;
end;
registration
let G be _Graph, e be set;
cluster plain for removeEdge of G, e;
end;
registration
let G be _Graph;
cluster plain for Supergraph of G;
let V be set;
cluster plain for addVertices of G, V;
end;
registration
let G be _Graph, v, e, w be object;
cluster plain for addEdge of G, v, e, w;
cluster plain for addAdjVertex of G, v, e, w;
end;
registration
let G be _Graph, v be object, V be set;
cluster plain for addAdjVertexFromAll of G, v, V;
cluster plain for addAdjVertexToAll of G, v, V;
cluster plain for addAdjVertexAll of G, v, V;
end;
begin :: Graphs with Loops removed
definition
let G be _Graph;
func G.loops() -> Subset of the_Edges_of G means
:: GLIB_009:def 2
for e being object holds e in it iff ex v being object st e Joins v,v,G;
end;
theorem :: GLIB_009:45
for G being _Graph, e being object
holds e in G.loops() iff ex v being object st e DJoins v,v,G;
theorem :: GLIB_009:46
for G being _Graph, e,v,w being object st e Joins v,w,G & v <> w
holds not e in G.loops();
theorem :: GLIB_009:47
for G being _Graph holds G is loopless iff G.loops() = {};
registration
let G be loopless _Graph;
cluster G.loops() -> empty;
end;
registration
let G be non loopless _Graph;
cluster G.loops() -> non empty;
end;
theorem :: GLIB_009:48
for G1 being _Graph, G2 being Subgraph of G1 holds G2.loops() c= G1.loops();
theorem :: GLIB_009:49
for G2 being _Graph, G1 being Supergraph of G2 holds G2.loops() c= G1.loops()
;
theorem :: GLIB_009:50
for G1, G2 being _Graph st G1 == G2 holds G1.loops() = G2.loops();
theorem :: GLIB_009:51
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1.loops() = G2.loops();
theorem :: GLIB_009:52
for G2 being _Graph, V being set, G1 being addVertices of G2, V
holds G1.loops() = G2.loops();
theorem :: GLIB_009:53
for G2 being _Graph, v1,e,v2 being object, G1 being addEdge of G2,v1,e,v2
st v1 <> v2 holds G1.loops() = G2.loops();
theorem :: GLIB_009:54
for G2 being _Graph, v being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,v st not e in the_Edges_of G2
holds G1.loops() = G2.loops() \/ {e};
theorem :: GLIB_009:55
for G2 being _Graph, v1,e,v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1.loops() = G2.loops();
theorem :: GLIB_009:56
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2,v,V holds G1.loops() = G2.loops();
theorem :: GLIB_009:57
for G being _Graph, P being Path of G holds P.edges() misses G.loops() or
ex v,e being object st e Joins v,v,G & P = G.walkOf(v,e,v);
definition
let G be _Graph;
mode removeLoops of G is removeEdges of G, G.loops();
end;
theorem :: GLIB_009:58
for G1 being loopless _Graph, G2 being _Graph
holds G1 == G2 iff G2 is removeLoops of G1;
theorem :: GLIB_009:59
for G1, G2 being _Graph, G3 being removeLoops of G1
holds G2 == G3 iff G2 is removeLoops of G1;
theorem :: GLIB_009:60
for G1, G2 being _Graph, G3 being removeLoops of G1
st G1 == G2 holds G3 is removeLoops of G2;
registration
let G be _Graph;
cluster -> loopless for removeLoops of G;
cluster plain for removeLoops of G;
end;
registration
let G be non-multi _Graph;
cluster -> simple for removeLoops of G;
end;
registration
let G be non-Dmulti _Graph;
cluster -> Dsimple for removeLoops of G;
end;
registration
let G be complete _Graph;
cluster -> complete for removeLoops of G;
end;
theorem :: GLIB_009:61
for G1 being _Graph, G2 being removeLoops of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last();
theorem :: GLIB_009:62
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
registration
let G be connected _Graph;
cluster -> connected for removeLoops of G;
end;
registration
let G be non connected _Graph;
cluster -> non connected for removeLoops of G;
end;
theorem :: GLIB_009:63
for G1 being _Graph, G2 being removeLoops of G1
holds G1.componentSet() = G2.componentSet();
theorem :: GLIB_009:64
for G1 being _Graph, G2 being removeLoops of G1
holds G1.numComponents() = G2.numComponents();
theorem :: GLIB_009:65
for G1 being _Graph, G2 being removeLoops of G1
holds G1 is chordal iff G2 is chordal;
:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for removeLoops of G;
end;
:: More theorems of this kind can be produced with other
:: subgraph modes. This particular example was needed
:: to show that the cut-vertex property prevails in graphs
:: with removed loops
theorem :: GLIB_009:66
for G1 being _Graph, v being set, G2 being removeLoops of G1
for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v
holds G4 is removeLoops of G3;
theorem :: GLIB_009:67
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex;
theorem :: GLIB_009:68
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex;
begin :: Graphs with parallel Edges removed
definition
let G be _Graph;
func EdgeAdjEqRel(G) -> Equivalence_Relation of the_Edges_of G means
:: GLIB_009:def 3
for e1, e2 being object holds [e1,e2] in it iff
ex v1, v2 being object st e1 Joins v1,v2,G & e2 Joins v1,v2,G;
func DEdgeAdjEqRel(G) -> Equivalence_Relation of the_Edges_of G means
:: GLIB_009:def 4
for e1, e2 being object holds [e1,e2] in it iff
ex v1, v2 being object st e1 DJoins v1,v2,G & e2 DJoins v1,v2,G;
end;
theorem :: GLIB_009:69
for G being _Graph holds DEdgeAdjEqRel(G) c= EdgeAdjEqRel(G);
theorem :: GLIB_009:70
for G being _Graph
holds G is non-multi iff EdgeAdjEqRel(G) = id the_Edges_of G;
theorem :: GLIB_009:71
for G being _Graph
holds G is non-Dmulti iff DEdgeAdjEqRel(G) = id the_Edges_of G;
registration
let G be edgeless _Graph;
cluster EdgeAdjEqRel(G) -> empty;
cluster DEdgeAdjEqRel(G) -> empty;
end;
registration
let G be non edgeless _Graph;
cluster EdgeAdjEqRel(G) -> non empty;
cluster DEdgeAdjEqRel(G) -> non empty;
end;
definition
let G be _Graph; :: Rep is short for Representative
mode RepEdgeSelection of G -> Subset of the_Edges_of G means
:: GLIB_009:def 5
for v,w,e0 being object st e0 Joins v,w,G
ex e being object st e Joins v,w,G & e in it &
for e9 being object st e9 Joins v,w,G & e9 in it holds e9 = e;
mode RepDEdgeSelection of G -> Subset of the_Edges_of G means
:: GLIB_009:def 6
for v,w,e0 being object st e0 DJoins v,w,G
ex e being object st e DJoins v,w,G & e in it &
for e9 being object st e9 DJoins v,w,G & e9 in it holds e9 = e;
end;
registration
let G be edgeless _Graph;
cluster -> empty for RepEdgeSelection of G;
cluster -> empty for RepDEdgeSelection of G;
end;
registration
let G be non edgeless _Graph;
cluster -> non empty for RepEdgeSelection of G;
cluster -> non empty for RepDEdgeSelection of G;
end;
theorem :: GLIB_009:72
for G being _Graph, E1 being RepDEdgeSelection of G
ex E2 being RepEdgeSelection of G st E2 c= E1;
theorem :: GLIB_009:73
for G being _Graph, E2 being RepEdgeSelection of G
ex E1 being RepDEdgeSelection of G st E2 c= E1;
theorem :: GLIB_009:74
for G being non-multi _Graph, E being RepEdgeSelection of G
holds E = the_Edges_of G;
theorem :: GLIB_009:75
for G being _Graph st ex E being RepEdgeSelection of G st E = the_Edges_of G
holds G is non-multi;
theorem :: GLIB_009:76
for G being non-Dmulti _Graph, E being RepDEdgeSelection of G
holds E = the_Edges_of G;
theorem :: GLIB_009:77
for G being _Graph st ex E being RepDEdgeSelection of G st E = the_Edges_of G
holds G is non-Dmulti;
theorem :: GLIB_009:78
for G1 being _Graph, G2 being Subgraph of G1, E being RepEdgeSelection of G1
st E c= the_Edges_of G2 holds E is RepEdgeSelection of G2;
theorem :: GLIB_009:79
for G1 being _Graph, G2 being Subgraph of G1, E being RepDEdgeSelection of G1
st E c= the_Edges_of G2 holds E is RepDEdgeSelection of G2;
theorem :: GLIB_009:80
for G1 being _Graph, G2 being Subgraph of G1,E2 being RepEdgeSelection of G2
ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ the_Edges_of G2;
theorem :: GLIB_009:81
for G1 being _Graph, G2 being Subgraph of G1,E2 being RepDEdgeSelection of G2
ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ the_Edges_of G2;
theorem :: GLIB_009:82
for G1 being _Graph, E1 being RepEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E1
for E2 being RepEdgeSelection of G2 holds E1 = E2;
theorem :: GLIB_009:83
for G1 being _Graph, E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E1
for E2 being RepDEdgeSelection of G2 holds E1 = E2;
theorem :: GLIB_009:84
for G1 being _Graph, E1 being RepDEdgeSelection of G1
for G2 being inducedSubgraph of G1, the_Vertices_of G1, E1
for E2 being RepEdgeSelection of G2
holds E2 c= E1 & E2 is RepEdgeSelection of G1;
theorem :: GLIB_009:85
for G being _Graph, E1, E2 being RepEdgeSelection of G
ex f being one-to-one Function st dom f = E1 & rng f = E2 &
for e,v,w being object st e in E1 holds e Joins v,w,G iff f.e Joins v,w,G;
theorem :: GLIB_009:86
for G being _Graph, E1, E2 being RepEdgeSelection of G
holds card E1 = card E2;
theorem :: GLIB_009:87
for G being _Graph, E1, E2 being RepDEdgeSelection of G
ex f being one-to-one Function st dom f = E1 & rng f = E2 &
for e,v,w being object st e in E1 holds e DJoins v,w,G iff f.e DJoins v,w,G
;
theorem :: GLIB_009:88
for G being _Graph, E1, E2 being RepDEdgeSelection of G
holds card E1 = card E2;
definition
let G be _Graph;
mode removeParallelEdges of G -> Subgraph of G means
:: GLIB_009:def 7
ex E being RepEdgeSelection of G
st it is inducedSubgraph of G, the_Vertices_of G, E;
mode removeDParallelEdges of G -> Subgraph of G means
:: GLIB_009:def 8
ex E being RepDEdgeSelection of G
st it is inducedSubgraph of G, the_Vertices_of G, E;
end;
registration
let G be _Graph;
cluster -> spanning non-multi for removeParallelEdges of G;
cluster -> spanning non-Dmulti for removeDParallelEdges of G;
cluster plain for removeParallelEdges of G;
cluster plain for removeDParallelEdges of G;
end;
registration
let G be loopless _Graph;
cluster -> simple for removeParallelEdges of G;
cluster -> Dsimple for removeDParallelEdges of G;
end;
theorem :: GLIB_009:89
for G1 being non-multi _Graph, G2 being _Graph
holds G1 == G2 iff G2 is removeParallelEdges of G1;
theorem :: GLIB_009:90
for G1 being non-Dmulti _Graph, G2 being _Graph
holds G1 == G2 iff G2 is removeDParallelEdges of G1;
theorem :: GLIB_009:91
for G1, G2 being _Graph, G3 being removeParallelEdges of G1
st G1 == G2 holds G3 is removeParallelEdges of G2;
theorem :: GLIB_009:92
for G1, G2 being _Graph, G3 being removeDParallelEdges of G1
st G1 == G2 holds G3 is removeDParallelEdges of G2;
theorem :: GLIB_009:93
for G1, G2 being _Graph, G3 being removeParallelEdges of G1
st G2 == G3 holds G2 is removeParallelEdges of G1;
theorem :: GLIB_009:94
for G1, G2 being _Graph, G3 being removeDParallelEdges of G1
st G2 == G3 holds G2 is removeDParallelEdges of G1;
theorem :: GLIB_009:95
for G1 being _Graph, G2 being removeDParallelEdges of G1
for G3 being removeParallelEdges of G2
holds G3 is removeParallelEdges of G1;
theorem :: GLIB_009:96
for G1 being _Graph, G2 being removeDParallelEdges of G1
ex G3 being removeParallelEdges of G1
st G3 is removeParallelEdges of G2;
theorem :: GLIB_009:97
for G1 being _Graph, G3 being removeParallelEdges of G1
ex G2 being removeDParallelEdges of G1
st G3 is removeParallelEdges of G2;
registration
let G be complete _Graph;
cluster -> complete for removeParallelEdges of G;
cluster -> complete for removeDParallelEdges of G;
end;
theorem :: GLIB_009:98
for G1 being _Graph, G2 being removeParallelEdges of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W1.vertexSeq() = W2.vertexSeq();
theorem :: GLIB_009:99
for G1 being _Graph, G2 being removeDParallelEdges of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W1.vertexSeq() = W2.vertexSeq();
theorem :: GLIB_009:100
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
theorem :: GLIB_009:101
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
registration
let G be connected _Graph;
cluster -> connected for removeParallelEdges of G;
cluster -> connected for removeDParallelEdges of G;
end;
registration
let G be non connected _Graph;
cluster -> non connected for removeParallelEdges of G;
cluster -> non connected for removeDParallelEdges of G;
end;
theorem :: GLIB_009:102
for G1 being _Graph, G2 being removeParallelEdges of G1
holds G1.componentSet() = G2.componentSet();
theorem :: GLIB_009:103
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1.componentSet() = G2.componentSet();
theorem :: GLIB_009:104
for G1 being _Graph, G2 being removeParallelEdges of G1
holds G1.numComponents() = G2.numComponents();
theorem :: GLIB_009:105
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1.numComponents() = G2.numComponents();
theorem :: GLIB_009:106
for G1 being _Graph, G2 being removeParallelEdges of G1
holds G1 is chordal iff G2 is chordal;
theorem :: GLIB_009:107
for G1 being _Graph, G2 being removeDParallelEdges of G1
holds G1 is chordal iff G2 is chordal;
:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for removeParallelEdges of G;
cluster -> chordal for removeDParallelEdges of G;
end;
:: for cut-vertex property, same as with removeLoops above
theorem :: GLIB_009:108
for G1 being _Graph, v being set, G2 being removeParallelEdges of G1
for G3 being removeVertex of G1, v, G4 being removeVertex of G2, v
holds G4 is removeParallelEdges of G3;
theorem :: GLIB_009:109
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex;
theorem :: GLIB_009:110
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex;
theorem :: GLIB_009:111
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated;
theorem :: GLIB_009:112
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated;
theorem :: GLIB_009:113
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex;
theorem :: GLIB_009:114
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex;
:: Graphs with Loops and parallel Edges removed
definition
let G be _Graph;
mode SimpleGraph of G -> Subgraph of G means
:: GLIB_009:def 9
ex E being RepEdgeSelection of G st
it is inducedSubgraph of G, the_Vertices_of G, E \ G.loops();
mode DSimpleGraph of G -> Subgraph of G means
:: GLIB_009:def 10
ex E being RepDEdgeSelection of G st
it is inducedSubgraph of G, the_Vertices_of G, E \ G.loops();
end;
theorem :: GLIB_009:115
for G1 being _Graph, G2 being removeParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1;
theorem :: GLIB_009:116
for G1 being _Graph, G2 being removeDParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1;
theorem :: GLIB_009:117
for G1 being _Graph, G2 being removeLoops of G1
for G3 being removeParallelEdges of G2 holds G3 is SimpleGraph of G1;
theorem :: GLIB_009:118
for G1 being _Graph, G2 being removeLoops of G1
for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1;
theorem :: GLIB_009:119
for G1 being _Graph, G3 being SimpleGraph of G1
ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2;
theorem :: GLIB_009:120
for G1 being _Graph, G3 being DSimpleGraph of G1
ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2;
theorem :: GLIB_009:121
for G1 being _Graph, G2 being removeLoops of G1, G3 being SimpleGraph of G1
holds G3 is removeParallelEdges of G2;
theorem :: GLIB_009:122
for G1 being _Graph, G2 being removeLoops of G1, G3 being DSimpleGraph of G1
holds G3 is removeDParallelEdges of G2;
theorem :: GLIB_009:123
for G1 being loopless _Graph, G2 being _Graph
holds G2 is SimpleGraph of G1 iff G2 is removeParallelEdges of G1;
theorem :: GLIB_009:124
for G1 being loopless _Graph, G2 being _Graph
holds G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1;
theorem :: GLIB_009:125
for G1 being non-multi _Graph, G2 being _Graph
holds G2 is SimpleGraph of G1 iff G2 is removeLoops of G1;
theorem :: GLIB_009:126
for G1 being non-Dmulti _Graph, G2 being _Graph
holds G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1;
registration
let G be _Graph;
cluster -> spanning loopless non-multi simple for SimpleGraph of G;
cluster -> spanning loopless non-Dmulti Dsimple for DSimpleGraph of G;
cluster plain for SimpleGraph of G;
cluster plain for DSimpleGraph of G;
end;
theorem :: GLIB_009:127
for G1 being simple _Graph, G2 being _Graph
holds G1 == G2 iff G2 is SimpleGraph of G1;
theorem :: GLIB_009:128
for G1 being Dsimple _Graph, G2 being _Graph
holds G1 == G2 iff G2 is DSimpleGraph of G1;
theorem :: GLIB_009:129
for G1, G2 being _Graph, G3 being SimpleGraph of G1
st G1 == G2 holds G3 is SimpleGraph of G2;
theorem :: GLIB_009:130
for G1, G2 being _Graph, G3 being DSimpleGraph of G1
st G1 == G2 holds G3 is DSimpleGraph of G2;
theorem :: GLIB_009:131
for G1, G2 being _Graph, G3 being SimpleGraph of G1
st G2 == G3 holds G2 is SimpleGraph of G1;
theorem :: GLIB_009:132
for G1, G2 being _Graph, G3 being DSimpleGraph of G1
st G2 == G3 holds G2 is DSimpleGraph of G1;
theorem :: GLIB_009:133
for G1 being _Graph, G2 being DSimpleGraph of G1, G3 being SimpleGraph of G2
holds G3 is SimpleGraph of G1;
theorem :: GLIB_009:134
for G1 being _Graph, G2 being DSimpleGraph of G1
ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2;
theorem :: GLIB_009:135
for G1 being _Graph, G3 being SimpleGraph of G1
ex G2 being DSimpleGraph of G1 st G3 is SimpleGraph of G2;
registration
let G be complete _Graph;
cluster -> complete for SimpleGraph of G;
cluster -> complete for DSimpleGraph of G;
end;
theorem :: GLIB_009:136
for G1 being _Graph, G2 being SimpleGraph of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last();
theorem :: GLIB_009:137
for G1 being _Graph, G2 being DSimpleGraph of G1, W1 being Walk of G1
ex W2 being Walk of G2 st W2 is_Walk_from W1.first(),W1.last();
theorem :: GLIB_009:138
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
theorem :: GLIB_009:139
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds G1.reachableFrom(v1) = G2.reachableFrom(v2);
registration
let G be connected _Graph;
cluster -> connected for SimpleGraph of G;
cluster -> connected for DSimpleGraph of G;
end;
registration
let G be non connected _Graph;
cluster -> non connected for SimpleGraph of G;
cluster -> non connected for DSimpleGraph of G;
end;
theorem :: GLIB_009:140
for G1 being _Graph, G2 being SimpleGraph of G1
holds G1.componentSet() = G2.componentSet();
theorem :: GLIB_009:141
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1.componentSet() = G2.componentSet();
theorem :: GLIB_009:142
for G1 being _Graph, G2 being SimpleGraph of G1
holds G1.numComponents() = G2.numComponents();
theorem :: GLIB_009:143
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1.numComponents() = G2.numComponents();
theorem :: GLIB_009:144
for G1 being _Graph, G2 being SimpleGraph of G1
holds G1 is chordal iff G2 is chordal;
theorem :: GLIB_009:145
for G1 being _Graph, G2 being DSimpleGraph of G1
holds G1 is chordal iff G2 is chordal;
:: non chordal cluster after non chordal has been clustered with cycles
registration
let G be chordal _Graph;
cluster -> chordal for SimpleGraph of G;
cluster -> chordal for DSimpleGraph of G;
end;
theorem :: GLIB_009:146
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex;
theorem :: GLIB_009:147
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is cut-vertex iff v2 is cut-vertex;
theorem :: GLIB_009:148
for G1 being loopless _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated;
theorem :: GLIB_009:149
for G1 being loopless _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds v1 is isolated iff v2 is isolated;
theorem :: GLIB_009:150
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex;
theorem :: GLIB_009:151
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v1 is endvertex holds v2 is endvertex;