:: Underlying Simple Graphs
:: by Sebastian Koch
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

:: into XBOOLE_1 ?

theorem Th1: :: GLIB_009:1

for X, Y being set st Y c= X holds
X \ (X \ Y) = Y

proof end;

Lm1: for R being Relation
for X being set holds (R | X) ~ = X |` (R ~)

proof end;

:: into RELAT_1 ?

theorem Th2: :: GLIB_009:2

for R being Relation
for X being set holds
( (R | X) ~ = X |` (R ~) & (X |` R) ~ = (R ~) | X )

proof end;

theorem :: GLIB_009:3

canceled;

::$CT
:: into FUNCT_1 ?
:: reformulation of FUNCT_1:113

theorem :: GLIB_009:4

for f being Function
for Y being set holds Y |` f = f | (dom (Y |` f))

proof end;

:: into FUNCT_1 ?

theorem :: GLIB_009:5

for f being one-to-one Function
for X being set holds
( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )

proof end;

:: BEGIN into GLIB_000 ?

theorem Th6: :: GLIB_009:6

for G being _Graph
for e, x1, y1, x2, y2 being object st e DJoins x1,y1,G & e DJoins x2,y2,G holds
( x1 = x2 & y1 = y2 )

proof end;

registration

let G be _trivial _Graph;

cluster the_Vertices_of G -> trivial ;

coherence
the_Vertices_of G is trivial

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like V42() [Graph-like] _trivial non-Dmulti -> non-multi for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is non-Dmulti holds
b₁ is non-multi

proof end;

let G be _trivial non-Dmulti _Graph;

cluster the_Edges_of G -> trivial ;

coherence
the_Edges_of G is trivial

proof end;

end;

theorem Th7: :: GLIB_009:7

for G being _Graph
for X, Y being set
for e, x, y being object st e DJoins x,y,G & x in X & y in Y holds
e DSJoins X,Y,G

proof end;

theorem :: GLIB_009:8

for G being _trivial _Graph
for 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 )

proof end;

theorem Th9: :: GLIB_009:9

for G being _Graph holds G == G | _GraphSelectors

proof end;

theorem Th10: :: GLIB_009:10

for G being _Graph
for X, Y being set
for e being object holds
( e SJoins X,Y,G iff e SJoins Y,X,G )

proof end;

theorem Th11: :: GLIB_009:11

for G being _Graph
for X, Y being set
for e being object holds
( e SJoins X,Y,G iff ( e DSJoins X,Y,G or e DSJoins Y,X,G ) )

proof end;

theorem Th12: :: GLIB_009:12

for G being _Graph
for e, v, w being object st e SJoins {v},{w},G holds
e Joins v,w,G

proof end;

theorem Th13: :: GLIB_009:13

for G being _Graph
for e, v, w being object st e DSJoins {v},{w},G holds
e DJoins v,w,G

proof end;

theorem :: GLIB_009:14

for G being _Graph
for 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})) )

proof end;

theorem :: GLIB_009:15

for G being _Graph
for X being set holds G .edgesBetween (X,X) = G .edgesDBetween (X,X)

proof end;

theorem :: GLIB_009:16

for G being _Graph
for X, Y being set holds G .edgesBetween (X,Y) = G .edgesBetween (Y,X)

proof end;

theorem :: GLIB_009:17

for G being _Graph holds
( G is loopless iff for v, e being object holds not e DJoins v,v,G )

proof end;

theorem Th18: :: GLIB_009:18

for G being _Graph holds
( G is loopless iff for v, e being object holds not e SJoins {v},{v},G )

proof end;

theorem Th19: :: GLIB_009:19

for G being _Graph holds
( G is loopless iff for v, e being object holds not e DSJoins {v},{v},G )

proof end;

theorem Th20: :: GLIB_009:20

for G being _Graph holds
( G is loopless iff for v being object holds G .edgesBetween ({v},{v}) = {} )

proof end;

theorem Th21: :: GLIB_009:21

for G being _Graph holds
( G is loopless iff for v being object holds G .edgesDBetween ({v},{v}) = {} )

proof end;

registration

let G be loopless _Graph;
let v be object ;

cluster G .edgesBetween ({v},{v}) -> empty ;

coherence
G .edgesBetween ({v},{v}) is empty by Th20;

cluster G .edgesDBetween ({v},{v}) -> empty ;

coherence
G .edgesDBetween ({v},{v}) is empty by Th21;

end;

theorem Th22: :: 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 )

proof end;

registration

let G be non-multi _Graph;
let v, w be object ;

cluster G .edgesBetween ({v},{w}) -> trivial ;

coherence
G .edgesBetween ({v},{w}) is trivial by Th22;

end;

theorem Th23: :: 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 )

proof end;

registration

let G be non-Dmulti _Graph;
let v, w be object ;

cluster G .edgesDBetween ({v},{w}) -> trivial ;

coherence
G .edgesDBetween ({v},{w}) is trivial by Th23;

end;

registration

let G be non _trivial _Graph;

cluster spanning -> non _trivial for Subgraph of G;

coherence
for b₁ being Subgraph of G st b₁ is spanning holds
not b₁ is _trivial

proof end;

end;

registration

let G be _Graph;

cluster isolated -> non endvertex for Element of the_Vertices_of G;

coherence
for b₁ being Vertex of G st b₁ is isolated holds
not b₁ is endvertex

proof end;

end;

:: END into GLIB_000 ?
:: into GLIB_001 ?

theorem Th24: :: GLIB_009:24

for G being _Graph
for v being Vertex of G holds (G .walkOf v) .edgeSeq() = <*> (the_Edges_of G)

proof end;

:: into GLIB_001 ?

theorem Th25: :: GLIB_009:25

for G being _Graph
for v being Vertex of G holds (G .walkOf v) .edges() = {}

proof end;

:: into GLIB_001

registration

let G be _Graph;
let W be V5() Walk of G;

cluster W .edges() -> empty trivial ;

coherence
( W .edges() is empty & W .edges() is trivial )

proof end;

end;

:: into GLIB_001 ?

registration

let G be _Graph;
let W be Walk of G;

cluster W .vertices() -> non empty ;

coherence
not W .vertices() is empty

proof end;

end;

:: into GLIB_001 ?

theorem :: GLIB_009:26

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds
W1 = W2

proof end;

:: into GLIB_001 ?

theorem :: GLIB_009:27

for G being _Graph
for p being FinSequence of the_Vertices_of G
for 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 )

proof end;

Lm2: for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 holds
( len W1 = len W2 iff W1 .length() = W2 .length() )

proof end;

:: into GLIB_001 ?

theorem :: GLIB_009:28

for G being _Graph
for W being Walk of G holds len (W .vertexSeq()) = (W .length()) + 1

proof end;

Lm3: for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
len W1 = len W2

proof end;

:: into GLIB_001 ?

theorem Th29: :: GLIB_009:29

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for n being odd Nat st W1 .vertexSeq() = W2 .vertexSeq() holds
W1 . n = W2 . n

proof end;

:: into GLIB_001 ?

theorem Th30: :: GLIB_009:30

for G1, G2 being _Graph
for W1 being Walk of G1
for 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() )

proof end;

:: into GLIB_001 ?

theorem Th31: :: GLIB_009:31

for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( ( W1 is V5() implies not W2 is V5() ) & ( W1 is closed implies W2 is closed ) )

proof end;

:: 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 Th32: :: GLIB_009:32

for G1, G2 being _Graph
for W1 being Walk of G1
for 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 ) )

proof end;

:: into GLIB_001 ?

scheme :: GLIB_009:sch 1
IndWalk{ F₁() -> _Graph, P₁[ Walk of F₁()] } :

for W being Walk of F₁() holds P₁[W]

provided

A1: for W being V5() Walk of F₁() holds P₁[W] and
A2: for W being Walk of F₁()
for e being object st e in (W .last()) .edgesInOut() & P₁[W] holds
P₁[W .addEdge e]

proof end;

:: into GLIB_001 ?

scheme :: GLIB_009:sch 2
IndDWalk{ F₁() -> _Graph, P₁[ Walk of F₁()] } :

for W being DWalk of F₁() holds P₁[W]

provided

A1: for W being V5() DWalk of F₁() holds P₁[W] and
A2: for W being DWalk of F₁()
for e being object st e in (W .last()) .edgesOut() & P₁[W] holds
P₁[W .addEdge e]

proof end;

:: into GLIB_002 ?

theorem Th33: :: GLIB_009:33

for G1 being _Graph
for 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

proof end;

:: into GLIB_002 ?

theorem :: GLIB_009:34

for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E st G2 is connected holds
G1 is connected by Th33;

:: into GLIB_002 ?

registration

let G1 be non connected _Graph;
let E be set ;

cluster -> non connected for inducedSubgraph of G1, the_Vertices_of G1,(the_Edges_of G1) \ E;

coherence
for b₁ being removeEdges of G1,E holds not b₁ is connected by Th33;

end;

:: into GLIB_002 ?

theorem Th35: :: GLIB_009:35

for G1 being _Graph
for 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
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

:: into GLIB_002 ?

theorem Th36: :: GLIB_009:36

for G1 being _Graph
for 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() ) & G1 is connected holds
G2 is connected

proof end;

:: into GLIB_002 ?

theorem Th37: :: GLIB_009:37

for G1 being _Graph
for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds
G1 .componentSet() = G2 .componentSet()

proof end;

:: into GLIB_002 ?

theorem Th38: :: GLIB_009:38

for G1 being _Graph
for G2 being spanning Subgraph of G1 st ( for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2 ) holds
G1 .numComponents() = G2 .numComponents()

proof end;

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

proof end;

registration

let G be non complete _Graph;

cluster spanning -> non complete for Subgraph of G;

coherence
for b₁ being Subgraph of G st b₁ is spanning holds
not b₁ is complete

proof end;

end;

:: into GLIB_006 ?

theorem Th40: :: GLIB_009:40

for G2, G3 being _Graph
for G1 being Supergraph of G3 st G1 == G2 holds
G2 is Supergraph of G3

proof end;

theorem Th41: :: GLIB_009:41

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V
for x, y being set
for e being object holds
( ( e Joins x,y,G1 implies e Joins x,y,G2 ) & ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G1 implies e DJoins x,y,G2 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G1 implies e SJoins x,y,G2 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G1 implies e DSJoins x,y,G2 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )

proof end;

:: into GLIB_007 ?

theorem Th42: :: GLIB_009:42

for G1, G2 being _Graph st G1 == G2 holds
G2 is reverseEdgeDirections of G1, {}

proof end;

:: into GLIB_007 ?

theorem :: GLIB_009:43

for G being _Graph holds G is reverseEdgeDirections of G, {} by Th42;

definition

let G be _Graph;

attr G is plain means :Def1: :: GLIB_009:def 1
dom G = _GraphSelectors ;

end;

:: deftheorem Def1 defines plain GLIB_009:def 1 :
for G being _Graph holds
( G is plain iff dom G = _GraphSelectors );

registration

let G be _Graph;

cluster G | _GraphSelectors -> plain ;

coherence
G | _GraphSelectors is plain

proof end;

end;

registration

let V be non empty set ;
let E be set ;
let S, T be Function of E,V;

cluster createGraph (V,E,S,T) -> plain ;

coherence
createGraph (V,E,S,T) is plain

proof end;

end;

registration

let G be _Graph;
let X be set ;

cluster G .set (WeightSelector,X) -> non plain ;

coherence
not G .set (WeightSelector,X) is plain

proof end;

cluster G .set (ELabelSelector,X) -> non plain ;

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

proof end;

cluster G .set (VLabelSelector,X) -> non plain ;

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

proof end;

end;

registration

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for set ;

existence
ex b₁ being _Graph st b₁ is plain

proof end;

end;

theorem :: GLIB_009:44

for G1, G2 being plain _Graph st G1 == G2 holds
G1 = G2

proof end;

:: existence clusters for plain graph modes

registration

let G be _Graph;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for Subgraph of G;

existence
ex b₁ being Subgraph of G st b₁ is plain

proof end;

let V be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,(the_Vertices_of G) \ V,G .edgesBetween ((the_Vertices_of G) \ V);

existence
ex b₁ being removeVertices of G,V st b₁ is plain

proof end;

let E be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,V,E;

existence
ex b₁ being inducedSubgraph of G,V,E st b₁ is plain

proof end;

end;

registration

let G be _Graph;
let E be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;

existence
ex b₁ being removeEdges of G,E st b₁ is plain

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for reverseEdgeDirections of G,E;

existence
ex b₁ being reverseEdgeDirections of G,E st b₁ is plain

proof end;

end;

registration

let G be _Graph;
let v be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for inducedSubgraph of G,(the_Vertices_of G) \ {v},G .edgesBetween ((the_Vertices_of G) \ {v});

existence
ex b₁ being removeVertex of G,v st b₁ is plain

proof end;

end;

registration

let G be _Graph;
let e be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};

existence
ex b₁ being removeEdge of G,e st b₁ is plain

proof end;

end;

registration

let G be _Graph;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for Supergraph of G;

existence
ex b₁ being Supergraph of G st b₁ is plain

proof end;

let V be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addVertices of G,V;

existence
ex b₁ being addVertices of G,V st b₁ is plain

proof end;

end;

registration

let G be _Graph;
let v, e, w be object ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addEdge of G,v,e,w;

existence
ex b₁ being addEdge of G,v,e,w st b₁ is plain

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertex of G,v,e,w;

existence
ex b₁ being addAdjVertex of G,v,e,w st b₁ is plain

proof end;

end;

registration

let G be _Graph;
let v be object ;
let V be set ;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexFromAll of G,v,V;

existence
ex b₁ being addAdjVertexFromAll of G,v,V st b₁ is plain

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexToAll of G,v,V;

existence
ex b₁ being addAdjVertexToAll of G,v,V st b₁ is plain

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for addAdjVertexAll of G,v,V;

existence
ex b₁ being addAdjVertexAll of G,v,V st b₁ is plain

proof end;

end;

definition

let G be _Graph;

func G .loops() -> Subset of (the_Edges_of G) means :Def2: :: GLIB_009:def 2
for e being object holds
( e in it iff ex v being object st e Joins v,v,G );

existence
ex b₁ being Subset of (the_Edges_of G) st
for e being object holds
( e in b₁ iff ex v being object st e Joins v,v,G )

proof end;

uniqueness
for b₁, b₂ being Subset of (the_Edges_of G) st ( for e being object holds
( e in b₁ iff ex v being object st e Joins v,v,G ) ) & ( for e being object holds
( e in b₂ iff ex v being object st e Joins v,v,G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines .loops() GLIB_009:def 2 :
for G being _Graph
for b₂ being Subset of (the_Edges_of G) holds
( b₂ = G .loops() iff for e being object holds
( e in b₂ iff ex v being object st e Joins v,v,G ) );

theorem Th45: :: GLIB_009:45

for G being _Graph
for e being object holds
( e in G .loops() iff ex v being object st e DJoins v,v,G )

proof end;

theorem Th46: :: GLIB_009:46

for G being _Graph
for e, v, w being object st e Joins v,w,G & v <> w holds
not e in G .loops()

proof end;

theorem Th47: :: GLIB_009:47

for G being _Graph holds
( G is loopless iff G .loops() = {} )

proof end;

registration

let G be loopless _Graph;

cluster G .loops() -> empty ;

coherence
G .loops() is empty by Th47;

end;

registration

let G be non loopless _Graph;

cluster G .loops() -> non empty ;

coherence
not G .loops() is empty by Th47;

end;

theorem Th48: :: GLIB_009:48

for G1 being _Graph
for G2 being Subgraph of G1 holds G2 .loops() c= G1 .loops()

proof end;

theorem Th49: :: GLIB_009:49

for G2 being _Graph
for G1 being Supergraph of G2 holds G2 .loops() c= G1 .loops()

proof end;

theorem Th50: :: GLIB_009:50

for G1, G2 being _Graph st G1 == G2 holds
G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:51

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:52

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:53

for G2 being _Graph
for v1, e, v2 being object
for G1 being addEdge of G2,v1,e,v2 st v1 <> v2 holds
G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:54

for G2 being _Graph
for v being Vertex of G2
for 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}

proof end;

theorem :: GLIB_009:55

for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 holds G1 .loops() = G2 .loops()

proof end;

theorem :: GLIB_009:56

for G2 being _Graph
for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V holds G1 .loops() = G2 .loops()

proof end;

theorem Th57: :: GLIB_009:57

for G being _Graph
for 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) ) )

proof end;

definition

let G be _Graph;
mode removeLoops of G is removeEdges of G,(G .loops());

end;

theorem Th58: :: GLIB_009:58

for G1 being loopless _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is removeLoops of G1 )

proof end;

theorem Th59: :: GLIB_009:59

for G1, G2 being _Graph
for G3 being removeLoops of G1 holds
( G2 == G3 iff G2 is removeLoops of G1 ) by GLIB_006:16, GLIB_000:93;

theorem Th60: :: GLIB_009:60

for G1, G2 being _Graph
for G3 being removeLoops of G1 st G1 == G2 holds
G3 is removeLoops of G2

proof end;

registration

let G be _Graph;

cluster -> loopless for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is loopless

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning plain for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

existence
ex b₁ being removeLoops of G st b₁ is plain

proof end;

end;

registration

let G be non-multi _Graph;

cluster -> simple for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is simple ;

end;

registration

let G be non-Dmulti _Graph;

cluster -> Dsimple for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is Dsimple ;

end;

registration

let G be complete _Graph;

cluster -> complete for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is complete

proof end;

end;

theorem Th61: :: GLIB_009:61

for G1 being _Graph
for G2 being removeLoops of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th62: :: GLIB_009:62

for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

registration

let G be connected _Graph;

cluster -> connected for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is connected

proof end;

end;

registration

let G be non connected _Graph;

cluster -> non connected for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds not b₁ is connected ;

end;

theorem :: GLIB_009:63

for G1 being _Graph
for G2 being removeLoops of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem Th64: :: GLIB_009:64

for G1 being _Graph
for G2 being removeLoops of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem Th65: :: GLIB_009:65

for G1 being _Graph
for G2 being removeLoops of G1 holds
( G1 is chordal iff G2 is chordal )

proof end;

:: non chordal cluster after non chordal has been clustered with cycles

registration

let G be chordal _Graph;

cluster -> chordal for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is chordal by Th65;

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 Th66: :: GLIB_009:66

for G1 being _Graph
for v being set
for G2 being removeLoops of G1
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeLoops of G3

proof end;

theorem Th67: :: GLIB_009:67

for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem Th68: :: GLIB_009:68

for G1 being _Graph
for G2 being removeLoops of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex

proof end;

definition

let G be _Graph;

func EdgeAdjEqRel G -> Equivalence_Relation of (the_Edges_of G) means :Def3: :: 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 ) );

existence
ex b₁ being Equivalence_Relation of (the_Edges_of G) st
for e1, e2 being object holds
( [e1,e2] in b₁ iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of (the_Edges_of G) st ( for e1, e2 being object holds
( [e1,e2] in b₁ iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) & ( for e1, e2 being object holds
( [e1,e2] in b₂ iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) holds
b₁ = b₂

proof end;

func DEdgeAdjEqRel G -> Equivalence_Relation of (the_Edges_of G) means :Def4: :: 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 ) );

existence
ex b₁ being Equivalence_Relation of (the_Edges_of G) st
for e1, e2 being object holds
( [e1,e2] in b₁ iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of (the_Edges_of G) st ( for e1, e2 being object holds
( [e1,e2] in b₁ iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) & ( for e1, e2 being object holds
( [e1,e2] in b₂ iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines EdgeAdjEqRel GLIB_009:def 3 :
for G being _Graph
for b₂ being Equivalence_Relation of (the_Edges_of G) holds
( b₂ = EdgeAdjEqRel G iff for e1, e2 being object holds
( [e1,e2] in b₂ iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) );

:: deftheorem Def4 defines DEdgeAdjEqRel GLIB_009:def 4 :
for G being _Graph
for b₂ being Equivalence_Relation of (the_Edges_of G) holds
( b₂ = DEdgeAdjEqRel G iff for e1, e2 being object holds
( [e1,e2] in b₂ iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) );

theorem :: GLIB_009:69

for G being _Graph holds DEdgeAdjEqRel G c= EdgeAdjEqRel G

proof end;

theorem :: GLIB_009:70

for G being _Graph holds
( G is non-multi iff EdgeAdjEqRel G = id (the_Edges_of G) )

proof end;

theorem :: GLIB_009:71

for G being _Graph holds
( G is non-Dmulti iff DEdgeAdjEqRel G = id (the_Edges_of G) )

proof end;

registration

let G be edgeless _Graph;

cluster EdgeAdjEqRel G -> empty ;

coherence
EdgeAdjEqRel G is empty ;

cluster DEdgeAdjEqRel G -> empty ;

coherence
DEdgeAdjEqRel G is empty ;

end;

registration

let G be non edgeless _Graph;

cluster EdgeAdjEqRel G -> non empty ;

coherence
not EdgeAdjEqRel G is empty ;

cluster DEdgeAdjEqRel G -> non empty ;

coherence
not DEdgeAdjEqRel G is empty ;

end;

definition

let G be _Graph;

mode RepEdgeSelection of G -> Subset of (the_Edges_of G) means :Def5: :: GLIB_009:def 5
for v, w, e0 being object st e0 Joins v,w,G holds
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 ) );

existence
ex b₁ being Subset of (the_Edges_of G) st
for v, w, e0 being object st e0 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in b₁ & ( for e9 being object st e9 Joins v,w,G & e9 in b₁ holds
e9 = e ) )

proof end;

mode RepDEdgeSelection of G -> Subset of (the_Edges_of G) means :Def6: :: GLIB_009:def 6
for v, w, e0 being object st e0 DJoins v,w,G holds
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 ) );

existence
ex b₁ being Subset of (the_Edges_of G) st
for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in b₁ & ( for e9 being object st e9 DJoins v,w,G & e9 in b₁ holds
e9 = e ) )

proof end;

end;

:: deftheorem Def5 defines RepEdgeSelection GLIB_009:def 5 :
for G being _Graph
for b₂ being Subset of (the_Edges_of G) holds
( b₂ is RepEdgeSelection of G iff for v, w, e0 being object st e0 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in b₂ & ( for e9 being object st e9 Joins v,w,G & e9 in b₂ holds
e9 = e ) ) );

:: deftheorem Def6 defines RepDEdgeSelection GLIB_009:def 6 :
for G being _Graph
for b₂ being Subset of (the_Edges_of G) holds
( b₂ is RepDEdgeSelection of G iff for v, w, e0 being object st e0 DJoins v,w,G holds
ex e being object st
( e DJoins v,w,G & e in b₂ & ( for e9 being object st e9 DJoins v,w,G & e9 in b₂ holds
e9 = e ) ) );

registration

let G be edgeless _Graph;

cluster -> empty for RepEdgeSelection of G;

coherence
for b₁ being RepEdgeSelection of G holds b₁ is empty

proof end;

cluster -> empty for RepDEdgeSelection of G;

coherence
for b₁ being RepDEdgeSelection of G holds b₁ is empty

proof end;

end;

registration

let G be non edgeless _Graph;

cluster -> non empty for RepEdgeSelection of G;

coherence
for b₁ being RepEdgeSelection of G holds not b₁ is empty

proof end;

cluster -> non empty for RepDEdgeSelection of G;

coherence
for b₁ being RepDEdgeSelection of G holds not b₁ is empty

proof end;

end;

theorem Th72: :: GLIB_009:72

for G being _Graph
for E1 being RepDEdgeSelection of G ex E2 being RepEdgeSelection of G st E2 c= E1

proof end;

theorem Th73: :: GLIB_009:73

for G being _Graph
for E2 being RepEdgeSelection of G ex E1 being RepDEdgeSelection of G st E2 c= E1

proof end;

theorem Th74: :: GLIB_009:74

for G being non-multi _Graph
for E being RepEdgeSelection of G holds E = the_Edges_of G

proof end;

theorem Th75: :: 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

proof end;

theorem Th76: :: GLIB_009:76

for G being non-Dmulti _Graph
for E being RepDEdgeSelection of G holds E = the_Edges_of G

proof end;

theorem Th77: :: 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

proof end;

theorem Th78: :: GLIB_009:78

for G1 being _Graph
for G2 being Subgraph of G1
for E being RepEdgeSelection of G1 st E c= the_Edges_of G2 holds
E is RepEdgeSelection of G2

proof end;

theorem Th79: :: GLIB_009:79

for G1 being _Graph
for G2 being Subgraph of G1
for E being RepDEdgeSelection of G1 st E c= the_Edges_of G2 holds
E is RepDEdgeSelection of G2

proof end;

theorem Th80: :: GLIB_009:80

for G1 being _Graph
for G2 being Subgraph of G1
for E2 being RepEdgeSelection of G2 ex E1 being RepEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

proof end;

theorem Th81: :: GLIB_009:81

for G1 being _Graph
for G2 being Subgraph of G1
for E2 being RepDEdgeSelection of G2 ex E1 being RepDEdgeSelection of G1 st E2 = E1 /\ (the_Edges_of G2)

proof end;

theorem Th82: :: GLIB_009:82

for G1 being _Graph
for 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

proof end;

theorem Th83: :: GLIB_009:83

for G1 being _Graph
for 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

proof end;

theorem Th84: :: GLIB_009:84

for G1 being _Graph
for 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 )

proof end;

theorem Th85: :: GLIB_009:85

for G being _Graph
for 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 ) ) )

proof end;

theorem :: GLIB_009:86

for G being _Graph
for E1, E2 being RepEdgeSelection of G holds card E1 = card E2

proof end;

theorem Th87: :: GLIB_009:87

for G being _Graph
for 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 ) ) )

proof end;

theorem :: GLIB_009:88

for G being _Graph
for E1, E2 being RepDEdgeSelection of G holds card E1 = card E2

proof end;

definition

let G be _Graph;

mode removeParallelEdges of G -> Subgraph of G means :Def7: :: GLIB_009:def 7
ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;

existence
ex b₁ being Subgraph of G ex E being RepEdgeSelection of G st b₁ is inducedSubgraph of G, the_Vertices_of G,E

proof end;

mode removeDParallelEdges of G -> Subgraph of G means :Def8: :: GLIB_009:def 8
ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E;

existence
ex b₁ being Subgraph of G ex E being RepDEdgeSelection of G st b₁ is inducedSubgraph of G, the_Vertices_of G,E

proof end;

end;

:: deftheorem Def7 defines removeParallelEdges GLIB_009:def 7 :
for G being _Graph
for b₂ being Subgraph of G holds
( b₂ is removeParallelEdges of G iff ex E being RepEdgeSelection of G st b₂ is inducedSubgraph of G, the_Vertices_of G,E );

:: deftheorem Def8 defines removeDParallelEdges GLIB_009:def 8 :
for G being _Graph
for b₂ being Subgraph of G holds
( b₂ is removeDParallelEdges of G iff ex E being RepDEdgeSelection of G st b₂ is inducedSubgraph of G, the_Vertices_of G,E );

registration

let G be _Graph;

cluster -> non-multi spanning for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds
( b₁ is spanning & b₁ is non-multi )

proof end;

cluster -> non-Dmulti spanning for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds
( b₁ is spanning & b₁ is non-Dmulti )

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for removeParallelEdges of G;

existence
ex b₁ being removeParallelEdges of G st b₁ is plain

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for removeDParallelEdges of G;

existence
ex b₁ being removeDParallelEdges of G st b₁ is plain

proof end;

end;

registration

let G be loopless _Graph;

cluster -> simple for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds b₁ is simple ;

cluster -> Dsimple for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds b₁ is Dsimple ;

end;

theorem :: GLIB_009:89

for G1 being non-multi _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is removeParallelEdges of G1 )

proof end;

theorem :: GLIB_009:90

for G1 being non-Dmulti _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is removeDParallelEdges of G1 )

proof end;

theorem Th91: :: GLIB_009:91

for G1, G2 being _Graph
for G3 being removeParallelEdges of G1 st G1 == G2 holds
G3 is removeParallelEdges of G2

proof end;

theorem :: GLIB_009:92

for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1 st G1 == G2 holds
G3 is removeDParallelEdges of G2

proof end;

theorem Th93: :: GLIB_009:93

for G1, G2 being _Graph
for G3 being removeParallelEdges of G1 st G2 == G3 holds
G2 is removeParallelEdges of G1

proof end;

theorem :: GLIB_009:94

for G1, G2 being _Graph
for G3 being removeDParallelEdges of G1 st G2 == G3 holds
G2 is removeDParallelEdges of G1

proof end;

theorem Th95: :: GLIB_009:95

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for G3 being removeParallelEdges of G2 holds G3 is removeParallelEdges of G1

proof end;

theorem Th96: :: GLIB_009:96

for G1 being _Graph
for G2 being removeDParallelEdges of G1 ex G3 being removeParallelEdges of G1 st G3 is removeParallelEdges of G2

proof end;

theorem Th97: :: GLIB_009:97

for G1 being _Graph
for G3 being removeParallelEdges of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeParallelEdges of G2

proof end;

registration

let G be complete _Graph;

cluster -> complete for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds b₁ is complete

proof end;

cluster -> complete for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds b₁ is complete

proof end;

end;

theorem Th98: :: GLIB_009:98

for G1 being _Graph
for G2 being removeParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()

proof end;

Lm4: for G1 being _Graph
for G2 being removeParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th99: :: GLIB_009:99

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq()

proof end;

Lm5: for G1 being _Graph
for G2 being removeDParallelEdges of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th100: :: GLIB_009:100

for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

theorem Th101: :: GLIB_009:101

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

registration

let G be connected _Graph;

cluster -> connected for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds b₁ is connected

proof end;

cluster -> connected for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds b₁ is connected

proof end;

end;

registration

let G be non connected _Graph;

cluster -> non connected for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds not b₁ is connected

proof end;

cluster -> non connected for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds not b₁ is connected

proof end;

end;

theorem :: GLIB_009:102

for G1 being _Graph
for G2 being removeParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem :: GLIB_009:103

for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem Th104: :: GLIB_009:104

for G1 being _Graph
for G2 being removeParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem :: GLIB_009:105

for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem Th106: :: GLIB_009:106

for G1 being _Graph
for G2 being removeParallelEdges of G1 holds
( G1 is chordal iff G2 is chordal )

proof end;

theorem Th107: :: GLIB_009:107

for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds
( G1 is chordal iff G2 is chordal )

proof end;

:: non chordal cluster after non chordal has been clustered with cycles

registration

let G be chordal _Graph;

cluster -> chordal for removeParallelEdges of G;

coherence
for b₁ being removeParallelEdges of G holds b₁ is chordal by Th106;

cluster -> chordal for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds b₁ is chordal by Th107;

end;

:: for cut-vertex property, same as with removeLoops above

theorem Th108: :: GLIB_009:108

for G1 being _Graph
for v being set
for G2 being removeParallelEdges of G1
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is removeParallelEdges of G3

proof end;

theorem Th109: :: GLIB_009:109

for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem Th110: :: GLIB_009:110

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem Th111: :: GLIB_009:111

for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

proof end;

theorem Th112: :: GLIB_009:112

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

proof end;

theorem Th113: :: GLIB_009:113

for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex

proof end;

theorem Th114: :: GLIB_009:114

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex

proof end;

:: Graphs with Loops and parallel Edges removed

definition

let G be _Graph;

mode SimpleGraph of G -> Subgraph of G means :Def9: :: GLIB_009:def 9
ex E being RepEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());

existence
ex b₁ being Subgraph of G ex E being RepEdgeSelection of G st b₁ is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())

proof end;

mode DSimpleGraph of G -> Subgraph of G means :Def10: :: GLIB_009:def 10
ex E being RepDEdgeSelection of G st it is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops());

existence
ex b₁ being Subgraph of G ex E being RepDEdgeSelection of G st b₁ is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops())

proof end;

end;

:: deftheorem Def9 defines SimpleGraph GLIB_009:def 9 :
for G being _Graph
for b₂ being Subgraph of G holds
( b₂ is SimpleGraph of G iff ex E being RepEdgeSelection of G st b₂ is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );

:: deftheorem Def10 defines DSimpleGraph GLIB_009:def 10 :
for G being _Graph
for b₂ being Subgraph of G holds
( b₂ is DSimpleGraph of G iff ex E being RepDEdgeSelection of G st b₂ is inducedSubgraph of G, the_Vertices_of G,E \ (G .loops()) );

theorem :: GLIB_009:115

for G1 being _Graph
for G2 being removeParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is SimpleGraph of G1

proof end;

theorem :: GLIB_009:116

for G1 being _Graph
for G2 being removeDParallelEdges of G1
for G3 being removeLoops of G2 holds G3 is DSimpleGraph of G1

proof end;

theorem Th117: :: GLIB_009:117

for G1 being _Graph
for G2 being removeLoops of G1
for G3 being removeParallelEdges of G2 holds G3 is SimpleGraph of G1

proof end;

theorem Th118: :: GLIB_009:118

for G1 being _Graph
for G2 being removeLoops of G1
for G3 being removeDParallelEdges of G2 holds G3 is DSimpleGraph of G1

proof end;

theorem Th119: :: GLIB_009:119

for G1 being _Graph
for G3 being SimpleGraph of G1 ex G2 being removeParallelEdges of G1 st G3 is removeLoops of G2

proof end;

theorem Th120: :: GLIB_009:120

for G1 being _Graph
for G3 being DSimpleGraph of G1 ex G2 being removeDParallelEdges of G1 st G3 is removeLoops of G2

proof end;

theorem Th121: :: GLIB_009:121

for G1 being _Graph
for G2 being removeLoops of G1
for G3 being SimpleGraph of G1 holds G3 is removeParallelEdges of G2

proof end;

theorem Th122: :: GLIB_009:122

for G1 being _Graph
for G2 being removeLoops of G1
for G3 being DSimpleGraph of G1 holds G3 is removeDParallelEdges of G2

proof end;

theorem Th123: :: GLIB_009:123

for G1 being loopless _Graph
for G2 being _Graph holds
( G2 is SimpleGraph of G1 iff G2 is removeParallelEdges of G1 )

proof end;

theorem :: GLIB_009:124

for G1 being loopless _Graph
for G2 being _Graph holds
( G2 is DSimpleGraph of G1 iff G2 is removeDParallelEdges of G1 )

proof end;

theorem :: GLIB_009:125

for G1 being non-multi _Graph
for G2 being _Graph holds
( G2 is SimpleGraph of G1 iff G2 is removeLoops of G1 )

proof end;

theorem :: GLIB_009:126

for G1 being non-Dmulti _Graph
for G2 being _Graph holds
( G2 is DSimpleGraph of G1 iff G2 is removeLoops of G1 )

proof end;

registration

let G be _Graph;

cluster -> loopless non-multi simple spanning for SimpleGraph of G;

coherence
for b₁ being SimpleGraph of G holds
( b₁ is spanning & b₁ is loopless & b₁ is non-multi & b₁ is simple )

proof end;

cluster -> loopless non-Dmulti Dsimple spanning for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds
( b₁ is spanning & b₁ is loopless & b₁ is non-Dmulti & b₁ is Dsimple )

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for SimpleGraph of G;

existence
ex b₁ being SimpleGraph of G st b₁ is plain

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] plain for DSimpleGraph of G;

existence
ex b₁ being DSimpleGraph of G st b₁ is plain

proof end;

end;

theorem :: GLIB_009:127

for G1 being simple _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is SimpleGraph of G1 )

proof end;

theorem :: GLIB_009:128

for G1 being Dsimple _Graph
for G2 being _Graph holds
( G1 == G2 iff G2 is DSimpleGraph of G1 )

proof end;

theorem :: GLIB_009:129

for G1, G2 being _Graph
for G3 being SimpleGraph of G1 st G1 == G2 holds
G3 is SimpleGraph of G2

proof end;

theorem :: GLIB_009:130

for G1, G2 being _Graph
for G3 being DSimpleGraph of G1 st G1 == G2 holds
G3 is DSimpleGraph of G2

proof end;

theorem :: GLIB_009:131

for G1, G2 being _Graph
for G3 being SimpleGraph of G1 st G2 == G3 holds
G2 is SimpleGraph of G1

proof end;

theorem :: GLIB_009:132

for G1, G2 being _Graph
for G3 being DSimpleGraph of G1 st G2 == G3 holds
G2 is DSimpleGraph of G1

proof end;

theorem Th133: :: GLIB_009:133

for G1 being _Graph
for G2 being DSimpleGraph of G1
for G3 being SimpleGraph of G2 holds G3 is SimpleGraph of G1

proof end;

theorem :: GLIB_009:134

for G1 being _Graph
for G2 being DSimpleGraph of G1 ex G3 being SimpleGraph of G1 st G3 is SimpleGraph of G2

proof end;

theorem :: GLIB_009:135

for G1 being _Graph
for G3 being SimpleGraph of G1 ex G2 being DSimpleGraph of G1 st G3 is SimpleGraph of G2

proof end;

registration

let G be complete _Graph;

cluster -> complete for SimpleGraph of G;

coherence
for b₁ being SimpleGraph of G holds b₁ is complete

proof end;

cluster -> complete for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds b₁ is complete

proof end;

end;

theorem Th136: :: GLIB_009:136

for G1 being _Graph
for G2 being SimpleGraph of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th137: :: GLIB_009:137

for G1 being _Graph
for G2 being DSimpleGraph of G1
for W1 being Walk of G1 ex W2 being Walk of G2 st W2 is_Walk_from W1 .first() ,W1 .last()

proof end;

theorem Th138: :: GLIB_009:138

for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

theorem Th139: :: GLIB_009:139

for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2

proof end;

registration

let G be connected _Graph;

cluster -> connected for SimpleGraph of G;

coherence
for b₁ being SimpleGraph of G holds b₁ is connected

proof end;

cluster -> connected for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds b₁ is connected

proof end;

end;

registration

let G be non connected _Graph;

cluster -> non connected for SimpleGraph of G;

coherence
for b₁ being SimpleGraph of G holds not b₁ is connected

proof end;

cluster -> non connected for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds not b₁ is connected

proof end;

end;

theorem :: GLIB_009:140

for G1 being _Graph
for G2 being SimpleGraph of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem :: GLIB_009:141

for G1 being _Graph
for G2 being DSimpleGraph of G1 holds G1 .componentSet() = G2 .componentSet()

proof end;

theorem :: GLIB_009:142

for G1 being _Graph
for G2 being SimpleGraph of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem :: GLIB_009:143

for G1 being _Graph
for G2 being DSimpleGraph of G1 holds G1 .numComponents() = G2 .numComponents()

proof end;

theorem Th144: :: GLIB_009:144

for G1 being _Graph
for G2 being SimpleGraph of G1 holds
( G1 is chordal iff G2 is chordal )

proof end;

theorem Th145: :: GLIB_009:145

for G1 being _Graph
for G2 being DSimpleGraph of G1 holds
( G1 is chordal iff G2 is chordal )

proof end;

:: non chordal cluster after non chordal has been clustered with cycles

registration

let G be chordal _Graph;

cluster -> chordal for SimpleGraph of G;

coherence
for b₁ being SimpleGraph of G holds b₁ is chordal by Th144;

cluster -> chordal for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds b₁ is chordal by Th145;

end;

theorem :: GLIB_009:146

for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem :: GLIB_009:147

for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is cut-vertex iff v2 is cut-vertex )

proof end;

theorem :: GLIB_009:148

for G1 being loopless _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

proof end;

theorem :: GLIB_009:149

for G1 being loopless _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v1 is isolated iff v2 is isolated )

proof end;

theorem :: GLIB_009:150

for G1 being _Graph
for G2 being SimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex

proof end;

theorem :: GLIB_009:151

for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is endvertex holds
v2 is endvertex

proof end;