:: Miscellaneous Graph Preliminaries, {I}
:: by Sebastian Koch
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


:: Proof mostly copied from XREGULAR:10
:: into XREGULAR ?
theorem :: GLIBPRE1:1
for X1, X2, X3, X4, X5, X6, X7 being set holds
( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X6 or not X6 in X7 or not X7 in X1 )
proof end;

:: Proof mostly copied from XREGULAR:10
:: into XREGULAR ?
theorem :: GLIBPRE1:2
for X1, X2, X3, X4, X5, X6, X7, X8 being set holds
( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X6 or not X6 in X7 or not X7 in X8 or not X8 in X1 )
proof end;

:: into FUNCT_1 ?
registration
cluster Relation-like Function-like one-to-one constant -> trivial for set ;
coherence
for b1 being Function st b1 is one-to-one & b1 is constant holds
b1 is trivial
proof end;
end;

:: into FUNCT_1 ?
theorem :: GLIBPRE1:3
for f being Function holds
( ( not f is empty & f is constant ) iff ex y being object st rng f = {y} )
proof end;

:: into PBOOLE ?
registration
let X be set ;
cluster Relation-like X -defined Function-like one-to-one total for set ;
existence
ex b1 being ManySortedSet of X st b1 is one-to-one
proof end;
end;

:: into PBOOLE ?
registration
let X be set ;
cluster Relation-like X -defined Function-like one-to-one total for set ;
existence
ex b1 being X -defined Function st
( b1 is total & b1 is one-to-one )
proof end;
end;

:: into PBOOLE ?
registration
let X be non empty set ;
cluster non empty Relation-like X -defined Function-like one-to-one total for set ;
existence
ex b1 being X -defined Function st
( b1 is total & b1 is one-to-one & not b1 is empty )
proof end;
end;

:: this is a variant of FUNCT_2:sch 4 which can be used a little bit easier
:: into FUNCT_2 ?
scheme :: GLIBPRE1:sch 1
LambdaDf{ F1() -> non empty set , F2() -> non empty set , F3( Element of F1()) -> object } :
ex f being Function of F1(),F2() st
for x being Element of F1() holds f . x = F3(x)
provided
A1: for x being Element of F1() holds F3(x) in F2()
proof end;

:: into FUNCOP_1 ?
theorem :: GLIBPRE1:4
for f being one-to-one Function
for y being object st rng f = {y} holds
ex x being object st f = x .--> y
proof end;

:: into FUNCOP_1 ?
registration
let f be one-to-one Function;
cluster f ~ -> one-to-one ;
coherence
f ~ is one-to-one
proof end;
end;

:: into FUNCT_3 or FUNCOP_1 ?
registration
let f be Function;
let g be one-to-one Function;
cluster <:f,g:> -> one-to-one ;
coherence
<:f,g:> is one-to-one
proof end;
cluster <:g,f:> -> one-to-one ;
coherence
<:g,f:> is one-to-one
proof end;
end;

:: into FUNCT_3 or FUNCOP_1 ?
theorem Th5: :: GLIBPRE1:5
for f being empty Function holds .: f = {} .--> {}
proof end;

:: into FUNCT_3 ?
registration
let f be one-to-one Function;
cluster .: f -> one-to-one ;
coherence
.: f is one-to-one
proof end;
end;

:: into FUNCT_3 ?
theorem Th6: :: GLIBPRE1:6
for f being non empty one-to-one Function
for X being non empty Subset of (bool (dom f)) holds rng ((.: f) | X) = { (f .: x) where x is Element of X : verum }
proof end;

:: into FUNCT_4 ?
theorem :: GLIBPRE1:7
for f being Function
for g, h being one-to-one Function st h = f +* g holds
(h ") | (rng g) = g "
proof end;

:: special case of FUNCT_7:10, compare FUNCT_7:9, FUNCT_7:11
:: into FUNCT_4 ?
theorem Th8: :: GLIBPRE1:8
for f, g, h being Function st rng f c= dom h holds
(g +* h) * f = h * f
proof end;

:: into FUNCT_4 ?
theorem :: GLIBPRE1:9
for f being Function
for g being one-to-one Function holds (f +* g) * (g ") = id (rng g)
proof end;

:: into RELAT_2 or ORDERS_1 ?
registration
cluster Relation-like reflexive connected -> strongly_connected for set ;
coherence
for b1 being Relation st b1 is reflexive & b1 is connected holds
b1 is strongly_connected
proof end;
end;

:: into RELSET_1 or ORDERS_1 ?
theorem :: GLIBPRE1:10
for X being set
for R being Relation of X holds
( R is antisymmetric iff R \ (id X) is asymmetric )
proof end;

:: into EQREL_1 or TAXONOM2 ?
theorem Th11: :: GLIBPRE1:11
for X being set st X is mutually-disjoint holds
X \ {{}} is a_partition of union X
proof end;

:: into EQREL_1 or TAXONOM2 ?
registration
let X be set ;
cluster -> mutually-disjoint for a_partition of X;
coherence
for b1 being a_partition of X holds b1 is mutually-disjoint
proof end;
end;

:: compare CARD_2:86, Proof mostly copied from there
:: into CARD_2 ?
theorem Th12: :: GLIBPRE1:12
for M, N being Cardinal
for f being Function st M c= card (dom f) & ( for x being object st x in dom f holds
N c= card (f . x) ) holds
M *` N c= Sum (Card f)
proof end;

:: into CARD_3 ?
theorem Th13: :: GLIBPRE1:13
for X, x being set st x in X holds
(disjoin (Card (id X))) . x = [:(card x),{x}:]
proof end;

:: into CARD_3 or TAXONOM2 ?
theorem Th14: :: GLIBPRE1:14
for X being set st X is mutually-disjoint holds
Sum (Card (id X)) = card (union X)
proof end;

:: compare CARD_2:87, Proof mostly copied from there
:: into CARD_2 ?
theorem :: GLIBPRE1:15
for X being set
for M, N being Cardinal st X is mutually-disjoint & M c= card X & ( for Y being set st Y in X holds
N c= card Y ) holds
M *` N c= card (union X)
proof end;

:: into COMPUT_1 ?
theorem :: GLIBPRE1:16
for F being functional compatible set st ( for f1 being Function st f1 in F holds
( f1 is one-to-one & ( for f2 being Function st f2 in F & f1 <> f2 holds
rng f1 misses rng f2 ) ) ) holds
union F is one-to-one
proof end;

registration
let G be non _trivial _Graph;
cluster non empty proper for Element of bool (the_Vertices_of G);
existence
ex b1 being Subset of (the_Vertices_of G) st
( not b1 is empty & b1 is proper )
proof end;
end;

theorem :: GLIBPRE1:17
for G being _Graph
for X being set holds G .edgesBetween (X,X) = G .edgesBetween X
proof end;

theorem :: GLIBPRE1:18
for G being _Graph holds
( G is _trivial iff the_Vertices_of G is trivial )
proof end;

theorem :: GLIBPRE1:19
for G1 being _Graph
for G2 being Subgraph of G1 holds G2 is inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2
proof end;

theorem :: GLIBPRE1:20
for G1, G2 being _Graph
for G3 being spanning Subgraph of G1 st G2 == G3 holds
G2 is spanning Subgraph of G1
proof end;

theorem :: GLIBPRE1:21
for G being _Graph
for e being object st e in the_Edges_of G holds
e in G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)}
proof end;

theorem :: GLIBPRE1:22
for G being _Graph holds G == createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))
proof end;

:: generalization of GLIB_000:def 52
theorem :: GLIBPRE1:23
for G being _Graph
for v being Vertex of G holds
( v is endvertex iff v .degree() = 1 )
proof end;

theorem :: GLIBPRE1:24
for G being loopless _Graph
for v being Vertex of G holds
( v .inNeighbors() c= (the_Vertices_of G) \ {v} & v .outNeighbors() c= (the_Vertices_of G) \ {v} & v .allNeighbors() c= (the_Vertices_of G) \ {v} )
proof end;

theorem :: GLIBPRE1:25
for G being _Graph st ( for v being Vertex of G holds
( v .inNeighbors() c= (the_Vertices_of G) \ {v} or v .outNeighbors() c= (the_Vertices_of G) \ {v} or v .allNeighbors() c= (the_Vertices_of G) \ {v} ) ) holds
G is loopless
proof end;

:: basic Proof copied from NAT --> G -> Graph-yielding
registration
let X be set ;
let G be _Graph;
cluster X --> G -> Graph-yielding ;
coherence
X --> G is Graph-yielding
proof end;
end;

registration
let x be object ;
let G be _Graph;
cluster x .--> G -> Graph-yielding ;
coherence
x .--> G is Graph-yielding
proof end;
end;

registration
let X be set ;
cluster Relation-like X -defined Function-like total Graph-yielding for set ;
existence
ex b1 being ManySortedSet of X st b1 is Graph-yielding
proof end;
end;

registration
let X be non empty set ;
cluster non empty Relation-like X -defined Function-like total Graph-yielding for set ;
existence
ex b1 being ManySortedSet of X st
( not b1 is empty & b1 is Graph-yielding )
proof end;
end;

definition
let X be non empty set ;
let f be Graph-yielding ManySortedSet of X;
let x be Element of X;
:: original: .
redefine func f . x -> _Graph;
coherence
f . x is _Graph
proof end;
end;

Lm1: for G being _Graph
for P being Path of G holds dom ((P .vertexSeq()) | (P .length())) = Seg (P .length())
proof end;

registration
let G be _Graph;
let P be Path of G;
cluster (P .vertexSeq()) | (P .length()) -> one-to-one ;
coherence
(P .vertexSeq()) | (P .length()) is one-to-one
proof end;
end;

:: compare GLIB_001:154
theorem :: GLIBPRE1:26
for G being _Graph
for P being Path of G holds P .length() c= G .order()
proof end;

:: compare GLIB_001:144
theorem :: GLIBPRE1:27
for G being _Graph
for T being Trail of G holds T .length() c= G .size()
proof end;

Lm2: for G being _Graph
for W being Walk of G st len W = 3 holds
ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )
proof end;

theorem Th28: :: GLIBPRE1:28
for G being _Graph
for W being Walk of G st ( len W = 3 or W .length() = 1 ) holds
ex e being object st
( e Joins W .first() ,W .last() ,G & W = G .walkOf ((W .first()),e,(W .last())) )
proof end;

theorem :: GLIBPRE1:29
for G being _Graph
for W being Walk of G
for e being object st e in W .edges() & not e in G .loops() & W is Circuit-like holds
ex e0 being object st
( e0 in W .edges() & e0 <> e )
proof end;

:: compare GLIB_001:149 and CHORD:93
theorem Th30: :: GLIBPRE1:30
for G being _Graph
for P being Path of G
for n, m being odd Element of NAT st n < m & m <= len P & ( n <> 1 or m <> len P ) holds
P .cut (n,m) is open
proof end;

:: cutting a closed walk at an edge
theorem Th31: :: GLIBPRE1:31
for G being _Graph
for W being closed Walk of G
for n being odd Element of NAT st n < len W holds
( (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is_Walk_from W . (n + 2),W . n & ( W is Trail-like implies ( (W .cut ((n + 2),(len W))) .edges() misses (W .cut (1,n)) .edges() & ((W .cut ((n + 2),(len W))) .append (W .cut (1,n))) .edges() = (W .edges()) \ {(W . (n + 1))} ) ) & ( W is Path-like implies ( ((W .cut ((n + 2),(len W))) .vertices()) /\ ((W .cut (1,n)) .vertices()) = {(W .first())} & ( not W . (n + 1) in G .loops() implies (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is open ) & (W .cut ((n + 2),(len W))) .append (W .cut (1,n)) is Path-like ) ) )
proof end;

:: extension of GLIB_001:157
theorem Th32: :: GLIBPRE1:32
for G being _Graph
for W1 being Walk of G
for e, x, y being object st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Path of G st
( W2 is_Walk_from x,y & W2 .edges() = (W1 .edges()) \ {e} & ( not e in G .loops() implies W2 is open ) )
proof end;

theorem :: GLIBPRE1:33
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;

theorem :: GLIBPRE1:34
for G being _Graph
for W being Walk of G holds W .length() = (W .reverse()) .length()
proof end;

theorem Th36: :: GLIBPRE1:35
for G being _Graph
for W being Walk of G
for e being object st not e in (W .last()) .edgesInOut() holds
W .addEdge e = W
proof end;

theorem :: GLIBPRE1:36
for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
(W .addEdge e) .length() = (W .length()) + 1
proof end;

theorem Th38: :: GLIBPRE1:37
for G1 being _Graph
for E being set
for G2 being removeEdges of G1,E
for W1 being Walk of G1 st W1 .edges() misses E holds
W1 is Walk of G2
proof end;

theorem Th39: :: GLIBPRE1:38
for G1, G2 being _Graph
for G3 being Component of G1 st G2 == G3 holds
G2 is Component of G1
proof end;

theorem :: GLIBPRE1:39
for G1, G2 being _Graph
for G3 being Component of G1 st G1 == G2 holds
G3 is Component of G2
proof end;

:: or into HELLY
theorem :: GLIBPRE1:40
for G being Tree-like _Graph
for H being spanning Subgraph of G st H is connected holds
G == H
proof end;

registration
let G be _Graph;
cluster -> non empty for Element of G .componentSet() ;
coherence
for b1 being Element of G .componentSet() holds not b1 is empty
proof end;
end;

registration
let G be _Graph;
cluster G .componentSet() -> mutually-disjoint ;
coherence
G .componentSet() is mutually-disjoint
proof end;
end;

theorem Th42: :: GLIBPRE1:41
for G being _Graph
for v, w being Vertex of G holds
( v,w are_adjacent iff w in v .allNeighbors() )
proof end;

:: the necessary existence clustering is from _008, but should be in _002
theorem Th43: :: GLIBPRE1:42
for G being _Graph
for S being set
for v being Vertex of G st not v in S & S meets G .reachableFrom v holds
G .AdjacentSet S <> {}
proof end;

:: the necessary existence clustering is from _008, but should be in _002
registration
let G be non _trivial connected _Graph;
let S be non empty proper Subset of (the_Vertices_of G);
cluster G .AdjacentSet S -> non empty ;
coherence
not G .AdjacentSet S is empty
proof end;
end;

theorem Th44: :: GLIBPRE1:43
for G being complete _Graph
for v being Vertex of G holds (the_Vertices_of G) \ {v} c= v .allNeighbors()
proof end;

theorem Th45: :: GLIBPRE1:44
for G being loopless complete _Graph
for v being Vertex of G holds v .allNeighbors() = (the_Vertices_of G) \ {v}
proof end;

theorem :: GLIBPRE1:45
for G being simple complete _Graph
for v being Vertex of G holds (v .degree()) +` 1 = G .order()
proof end;

registration
let G be _Graph;
cluster V5() -> minlength for Walk of G;
coherence
for b1 being Walk of G st b1 is V5() holds
b1 is minlength
proof end;
cluster Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like V42() FinSequence-like FinSubsequence-like Path-like minlength countable for Walk of G;
existence
ex b1 being Walk of G st
( b1 is minlength & b1 is Path-like )
proof end;
end;

registration
let G be _Graph;
let W be minlength Walk of G;
cluster W .reverse() -> minlength ;
coherence
W .reverse() is minlength
proof end;
end;

theorem Th47: :: GLIBPRE1:46
for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is minlength holds
W2 is minlength
proof end;

theorem Th48: :: GLIBPRE1:47
for G being _Graph
for v being Vertex of G
for W being Walk of G st W is_Walk_from v,v holds
( W is minlength iff W = G .walkOf v )
proof end;

theorem Th49: :: GLIBPRE1:48
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st G1 == G2 & W1 = W2 & W1 is minlength holds
W2 is minlength
proof end;

:: other direction of first part of GLIB_000:72 and GLIB_006:70
theorem Th50: :: GLIBPRE1:49
for G1, G2 being _Graph st the_Vertices_of G2 c= the_Vertices_of G1 & ( for e, x, y being object st e DJoins x,y,G2 holds
e DJoins x,y,G1 ) holds
( G2 is Subgraph of G1 & G1 is Supergraph of G2 )
proof end;

theorem :: GLIBPRE1:50
for G1 being _Graph
for G3 being Subgraph of G1
for v, e, w being object
for G2 being addEdge of G3,v,e,w st e DJoins v,w,G1 holds
G2 is Subgraph of G1
proof end;

:: adding an edge to a tree makes it unicyclic
theorem :: GLIBPRE1:51
for G being Tree-like _Graph
for v1, v2 being Vertex of G
for e being object
for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
( not H is acyclic & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) )
proof end;

:: if adding an edge to a graph makes it unicyclic, it has been a tree before
theorem :: GLIBPRE1:52
for G being connected _Graph st ex v1, v2 being Vertex of G ex e being object ex H being addEdge of G,v1,e,v2 st
( not e in the_Edges_of G & ( for W1, W2 being Walk of H st W1 is Cycle-like & W2 is Cycle-like holds
W1 .edges() = W2 .edges() ) ) holds
G is Tree-like
proof end;

theorem Th54: :: GLIBPRE1:53
for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( the_Vertices_of G1 c= (the_Vertices_of G2) \/ {v,w} & the_Edges_of G1 c= (the_Edges_of G2) \/ {e} )
proof end;

theorem Th55: :: GLIBPRE1:54
for G2 being _Graph
for v, v2 being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = v2 & not v in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

theorem Th56: :: GLIBPRE1:55
for G2 being _Graph
for w, v2 being Vertex of G2
for v, e being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = v2 & not w in G2 .reachableFrom v2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .reachableFrom v1 = G2 .reachableFrom v2
proof end;

theorem Th57: :: GLIBPRE1:56
for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = v & not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
G1 .reachableFrom v1 = (G2 .reachableFrom v) \/ {w}
proof end;

theorem Th58: :: GLIBPRE1:57
for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 = w & not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .reachableFrom v1 = (G2 .reachableFrom w) \/ {v}
proof end;

theorem :: GLIBPRE1:58
for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom v)}) \/ {((G2 .reachableFrom v) \/ {w})}
proof end;

theorem :: GLIBPRE1:59
for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
G1 .componentSet() = ((G2 .componentSet()) \ {(G2 .reachableFrom w)}) \/ {((G2 .reachableFrom w) \/ {v})}
proof end;

theorem Th61: :: GLIBPRE1:60
for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength holds
W1 is minlength
proof end;

:: the necessary existence clustering is from _008, but should be in _002
theorem :: GLIBPRE1:61
for G1 being non _trivial connected _Graph
for G2 being non spanning Subgraph of G1 ex v, e, w being object st
( v <> w & e DJoins v,w,G1 & not e in the_Edges_of G2 & ( for G3 being addAdjVertex of G2,v,e,w holds G3 is Subgraph of G1 ) & ( ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 ) or ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ) )
proof end;

theorem :: GLIBPRE1:62
for G2 being _Graph
for v being Vertex of G2
for e, w, x being object
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,v & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
proof end;

theorem :: GLIBPRE1:63
for G2 being _Graph
for v, e, x being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W2 is minlength & W2 is_Walk_from x,w & not e in the_Edges_of G2 holds
W1 .addEdge e is minlength
proof end;

registration
cluster non empty Relation-like Function-like Graph-yielding non non-multi non non-Dmulti for set ;
existence
ex b1 being Graph-yielding Function st
( not b1 is empty & not b1 is non-Dmulti & not b1 is non-multi )
proof end;
end;

registration
cluster non empty Relation-like Function-like Graph-yielding non connected non acyclic for set ;
existence
ex b1 being Graph-yielding Function st
( not b1 is empty & not b1 is acyclic & not b1 is connected )
proof end;
end;

registration
cluster non empty Relation-like Function-like Graph-yielding non edgeless for set ;
existence
ex b1 being Graph-yielding Function st
( not b1 is empty & not b1 is edgeless )
proof end;
end;

registration
cluster non empty Relation-like Function-like Graph-yielding non loopfull for set ;
existence
ex b1 being Graph-yielding Function st
( not b1 is empty & not b1 is loopfull )
proof end;
end;

theorem :: GLIBPRE1:64
for G2, G3 being _Graph
for V, E being set
for G1 being addVertices of G3,V
for G4 being reverseEdgeDirections of G3,E holds
( G2 is reverseEdgeDirections of G1,E iff G2 is addVertices of G4,V )
proof end;

theorem Th66: :: GLIBPRE1:65
for G2, G3 being _Graph
for v, e, w being object
for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )
proof end;

theorem :: GLIBPRE1:66
for G2, G3 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addAdjVertex of G3,w,e,v )
proof end;

Lm3: for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is minlength holds
W2 is minlength
proof end;

theorem :: GLIBPRE1:67
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
proof end;

theorem :: GLIBPRE1:68
for G1 being edgeless _Graph
for G2 being _Graph holds
( G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2 )
proof end;

registration
cluster Relation-like NAT -defined Function-like V42() [Graph-like] loopless non edgeless countable non 0 -vertex for set ;
existence
ex b1 being _Graph st
( b1 is loopless & not b1 is edgeless )
proof end;
end;

registration
let G be _Graph;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] spanning acyclic plain countable non 0 -vertex for Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is plain & b1 is spanning & b1 is acyclic )
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] Tree-like plain countable non 0 -vertex for Subgraph of G;
existence
ex b1 being Subgraph of G st
( b1 is plain & b1 is Tree-like )
proof end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] connected Component-like plain countable non 0 -vertex for Subgraph of G;
existence
ex b1 being Component of G st b1 is plain
proof end;
end;

theorem :: GLIBPRE1:69
for G being plain _Graph holds G = createGraph ((the_Vertices_of G),(the_Edges_of G),(the_Source_of G),(the_Target_of G))
proof end;

theorem :: GLIBPRE1:70
for G being _Graph
for H being removeLoops of G holds
( the_Edges_of G = G .loops() iff H is edgeless )
proof end;

theorem :: GLIBPRE1:71
for G being _Graph
for H being removeLoops of G
for H9 being loopless Subgraph of G holds H9 is Subgraph of H
proof end;

theorem :: GLIBPRE1:72
for G1 being _Graph
for G2 being removeLoops of G1
for W1 being minlength Walk of G1 holds W1 is Walk of G2
proof end;

theorem :: GLIBPRE1:73
for G1 being _Graph
for G2 being removeLoops of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
proof end;

theorem Th75: :: GLIBPRE1:74
for G1 being _Graph
for G2 being removeLoops of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
proof end;

theorem Th76: :: GLIBPRE1:75
for G1 being _Graph
for G2 being removeParallelEdges of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
proof end;

theorem Th77: :: GLIBPRE1:76
for G1 being _Graph
for G2 being removeDParallelEdges of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
proof end;

theorem :: GLIBPRE1:77
for G1 being _Graph
for G2 being SimpleGraph of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
proof end;

theorem :: GLIBPRE1:78
for G1 being _Graph
for G2 being DSimpleGraph of G1
for v1, w1 being Vertex of G1
for v2, w2 being Vertex of G2 st v1 = v2 & w1 = w2 & v1 <> w1 holds
( v1,w1 are_adjacent iff v2,w2 are_adjacent )
proof end;

theorem Th80: :: GLIBPRE1:79
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is total holds
(F _V) .: (G1 .reachableFrom v1) c= G2 .reachableFrom v2
proof end;

:: onto would be enough, but there are no theorems for that
:: (there could be multiple walks of G1 mapping to a specific one of G2)
theorem Th81: :: GLIBPRE1:80
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 in dom (F _V) & v2 = (F _V) . v1 & F is one-to-one & F is onto holds
G2 .reachableFrom v2 c= (F _V) .: (G1 .reachableFrom v1)
proof end;

theorem Th82: :: GLIBPRE1:81
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) .: (G1 .reachableFrom v1) = G2 .reachableFrom v2
proof end;

theorem Th83: :: GLIBPRE1:82
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G2 .componentSet() = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum }
proof end;

theorem :: GLIBPRE1:83
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .numComponents() = G2 .numComponents()
proof end;

registration
let G be loopless _Graph;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] G -isomorphic -> loopless for set ;
coherence
for b1 being _Graph st b1 is G -isomorphic holds
b1 is loopless
proof end;
end;

theorem Th85: :: GLIBPRE1:84
for G1, G2, G3, G4 being _Graph
for F1 being empty PGraphMapping of G1,G2
for F2 being empty PGraphMapping of G3,G4 holds F1 = F2
proof end;

theorem Th86: :: GLIBPRE1:85
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds
( F | (dom F) = F & (rng F) |` F = F )
proof end;

theorem Th87: :: GLIBPRE1:86
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is total holds
(rng F) |` F is total
proof end;

theorem :: GLIBPRE1:87
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto holds
F | (dom F) is onto
proof end;

theorem :: GLIBPRE1:88
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds F is PGraphMapping of G1, rng F
proof end;

theorem :: GLIBPRE1:89
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 holds F is PGraphMapping of dom F,G2
proof end;

:: Proof mostly taken from GLIB_010:46, generalization of the same
theorem Th91: :: GLIBPRE1:90
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is total holds
(F _E) .: (G1 .edgesBetween (X,Y)) c= G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
proof end;

:: generalization of GLIB_010:7 and GLIB_010:46
theorem Th103: :: GLIBPRE1:91
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for V being set holds (F _E) .: (G1 .edgesBetween V) c= G2 .edgesBetween ((F _V) .: V)
proof end;

:: generalization of GLIB_010:86
theorem :: GLIBPRE1:92
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for X, Y being Subset of (the_Vertices_of G1) st F is weak_SG-embedding & F is onto holds
(F _E) .: (G1 .edgesBetween (X,Y)) = G2 .edgesBetween (((F _V) .: X),((F _V) .: Y))
proof end;

:: generalization of GLIB_010:87
theorem Th104: :: GLIBPRE1:93
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for V being set st F is continuous holds
(F _E) .: (G1 .edgesBetween V) = G2 .edgesBetween ((F _V) .: V)
proof end;

theorem Th95: :: GLIBPRE1:94
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds (F " W2) .vertices() = (F _V) " (W2 .vertices())
proof end;

theorem Th96: :: GLIBPRE1:95
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2 holds (F " W2) .edges() = (F _E) " (W2 .edges())
proof end;

theorem Th97: :: GLIBPRE1:96
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for W2 being b3 -valued Walk of G2
for v, w being object st W2 is_Walk_from v,w holds
F " W2 is_Walk_from ((F ") _V) . v,((F ") _V) . w by GLIB_010:132;

theorem :: GLIBPRE1:97
for G1, G2 being _Graph
for F being one-to-one PGraphMapping of G1,G2
for v1 being Vertex of G1
for v2 being Vertex of G2 st v2 = (F _V) . v1 & F is isomorphism holds
(F _V) " (G2 .reachableFrom v2) = G1 .reachableFrom v1
proof end;

theorem Th99: :: GLIBPRE1:98
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H being Subgraph of G2 holds (F _E) " (the_Edges_of H) c= G1 .edgesBetween ((F _V) " (the_Vertices_of H))
proof end;

theorem :: GLIBPRE1:99
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds rng (F | H1) == H2
proof end;

theorem Th101: :: GLIBPRE1:100
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for V2 being non empty Subset of (the_Vertices_of (rng F))
for H being inducedSubgraph of (rng F),V2 st G1 .edgesBetween ((F _V) " (the_Vertices_of H)) c= dom (F _E) holds
(F _E) " (the_Edges_of H) = G1 .edgesBetween ((F _V) " (the_Vertices_of H))
proof end;

theorem :: GLIBPRE1:101
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for V2 being non empty Subset of (the_Vertices_of (rng F))
for H2 being inducedSubgraph of (rng F),V2
for H1 being inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)) st G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E) holds
rng (F | H1) == H2
proof end;

theorem :: GLIBPRE1:102
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for V being non empty Subset of (the_Vertices_of (dom F))
for H being inducedSubgraph of G1,V st F is continuous holds
rng (F | H) is inducedSubgraph of G2,((F _V) .: V)
proof end;

theorem Th106: :: GLIBPRE1:103
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)
for W1 being Walk of H1 holds W1 is b3 -defined Walk of G1
proof end;

theorem Th107: :: GLIBPRE1:104
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)
for W1 being b3 -defined Walk of G1 st W1 is Walk of H1 holds
F .: W1 is Walk of H2
proof end;

theorem Th108: :: GLIBPRE1:105
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1,G2
for H being Subgraph of rng F
for W being Walk of H holds W is b3 -valued Walk of G2
proof end;

theorem Th109: :: GLIBPRE1:106
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for H2 being Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)
for W2 being b3 -valued Walk of G2 st W2 is Walk of H2 holds
F " W2 is Walk of H1
proof end;

theorem :: GLIBPRE1:107
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for H2 being acyclic Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is acyclic
proof end;

theorem :: GLIBPRE1:108
for G1, G2 being _Graph
for F being non empty one-to-one PGraphMapping of G1,G2
for H2 being connected Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is connected
proof end;

:: To see why F_E being one-to-one is necessary for (D)continuity
:: consider the surjective mapping from K_4 to K_2. It is (D)continuous,
:: but if you take H = 2K_2, then the induced map isn't (D)continuous anymore
:: (but it still is semi-(D)continuous).
theorem Th112: :: GLIBPRE1:109
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H being Subgraph of G1
for F9 being PGraphMapping of H, rng (F | H) st F9 = F | H holds
( ( not F9 is empty implies F9 is onto ) & ( F is total implies F9 is total ) & ( F is one-to-one implies F9 is one-to-one ) & ( F is directed implies F9 is directed ) & ( F is semi-continuous implies F9 is semi-continuous ) & ( F is continuous & F _E is one-to-one implies F9 is continuous ) & ( F is semi-Dcontinuous implies F9 is semi-Dcontinuous ) & ( F is Dcontinuous & F _E is one-to-one implies F9 is Dcontinuous ) )
proof end;

theorem :: GLIBPRE1:110
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for H being Subgraph of G1
for F9 being PGraphMapping of H, rng (F | H) st F9 = F | H holds
( ( F is weak_SG-embedding implies F9 is weak_SG-embedding ) & ( F is strong_SG-embedding implies F9 is isomorphism ) & ( F is directed & F is strong_SG-embedding implies F9 is Disomorphism ) )
proof end;

:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem :: GLIBPRE1:111
for G1 being Dsimple vertex-finite _Graph
for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() = (G1 .order()) - ((v1 .inDegree()) + 1) & v2 .outDegree() = (G1 .order()) - ((v1 .outDegree()) + 1) & v2 .degree() = (2 * (G1 .order())) - ((v1 .degree()) + 2) )
proof end;

:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem :: GLIBPRE1:112
for G1 being simple vertex-finite _Graph
for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
v2 .degree() = (G1 .order()) - ((v1 .degree()) + 1)
proof end;

theorem :: GLIBPRE1:113
for G being Dsimple vertex-finite _Graph
for v being Vertex of G holds
( v .inDegree() < G .order() & v .outDegree() < G .order() )
proof end;

theorem :: GLIBPRE1:114
for G being simple vertex-finite _Graph
for v being Vertex of G holds v .degree() < G .order()
proof end;

registration
cluster Relation-like NAT -defined Function-like V42() [Graph-like] 1 -edge -> non-multi for set ;
coherence
for b1 being _Graph st b1 is 1 -edge holds
b1 is non-multi
proof end;
end;

registration
let S be Graph-membered \/-tolerating set ;
cluster -> \/-tolerating for Element of bool S;
coherence
for b1 being Subset of S holds b1 is \/-tolerating
proof end;
end;

theorem :: GLIBPRE1:115
for S1, S2 being Graph-membered set st S1 c= S2 holds
( the_Vertices_of S1 c= the_Vertices_of S2 & the_Edges_of S1 c= the_Edges_of S2 & the_Source_of S1 c= the_Source_of S2 & the_Target_of S1 c= the_Target_of S2 )
proof end;

theorem Th119: :: GLIBPRE1:116
for S being GraphUnionSet
for G being GraphUnion of S
for e, v, w being object st e DJoins v,w,G holds
ex H being Element of S st e DJoins v,w,H
proof end;

theorem :: GLIBPRE1:117
for S being GraphUnionSet
for G being GraphUnion of S
for e, v, w being object st e Joins v,w,G holds
ex H being Element of S st e Joins v,w,H
proof end;

theorem Th121: :: GLIBPRE1:118
for S1, S2 being GraphUnionSet
for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st ( for H2 being Element of S2 ex H1 being Element of S1 st H2 is Subgraph of H1 ) holds
G2 is Subgraph of G1
proof end;

theorem :: GLIBPRE1:119
for S1, S2 being GraphUnionSet
for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st S2 c= S1 holds
G2 is Subgraph of G1
proof end;

theorem :: GLIBPRE1:120
for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 holds
G .order() = (G1 .order()) +` (G2 .order())
proof end;

theorem :: GLIBPRE1:121
for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Edges_of G1 misses the_Edges_of G2 holds
G .size() = (G1 .size()) +` (G2 .size())
proof end;

theorem :: GLIBPRE1:122
for G1, G2 being connected _Graph
for G being GraphUnion of G1,G2 st the_Vertices_of G1 meets the_Vertices_of G2 holds
G is connected
proof end;

Lm4: for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 holds
for W being Walk of G holds
( W is Walk of G1 or W is Walk of G2 )
proof end;

theorem Th126: :: GLIBPRE1:123
for G1, G2 being _Graph
for G being GraphUnion of G1,G2
for W being Walk of G st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & W is not Walk of G1 holds
W is Walk of G2 by Lm4;

theorem Th127: :: GLIBPRE1:124
for G1, G2 being _Graph
for G being GraphUnion of G1,G2
for v1 being Vertex of G1
for v being Vertex of G st the_Vertices_of G1 misses the_Vertices_of G2 & v = v1 holds
G .reachableFrom v = G1 .reachableFrom v1
proof end;

theorem Th128: :: GLIBPRE1:125
for G1, G2 being _Graph
for G being GraphUnion of G1,G2
for v2 being Vertex of G2
for v being Vertex of G st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 & v = v2 holds
G .reachableFrom v = G2 .reachableFrom v2
proof end;

Lm5: for G1, G2 being _Graph st the_Vertices_of G1 misses the_Vertices_of G2 holds
G1 .componentSet() misses G2 .componentSet()
proof end;

theorem :: GLIBPRE1:126
for G1, G2 being _Graph
for G being GraphUnion of G1,G2 st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2 holds
( G .componentSet() = (G1 .componentSet()) \/ (G2 .componentSet()) & G .numComponents() = (G1 .numComponents()) +` (G2 .numComponents()) )
proof end;

theorem Th130: :: GLIBPRE1:127
for V being non empty set
for E being Relation of V holds (createGraph (V,E)) .loops() = E /\ (id V)
proof end;

theorem :: GLIBPRE1:128
for V being non empty set
for E being Relation of V holds createGraph (V,(E \ (id V))) is removeLoops of (createGraph (V,E))
proof end;