GLIBPRE1: Miscellaneous Graph Preliminaries, {I}

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

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

proof end;

end;

:: into PBOOLE ?

registration

let X be set ;

cluster Relation-like X -defined Function-like one-to-one total for set ;

existence

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

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{ F₁() -> non empty set , F₂() -> non empty set , F₃( Element of F₁()) -> object } :

ex f being Function of F₁(),F₂() st
for x being Element of F₁() holds f . x = F₃(x)

provided

A1: for x being Element of F₁() holds F₃(x) in F₂()

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

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

proof end;

cluster <:g,f:> -> one-to-one ;

coherence

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

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

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

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

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

proof end;

end;

registration

let x be object ;
let G be _Graph;

cluster x .--> G -> Graph-yielding ;

coherence

proof end;

end;

registration

let X be set ;

cluster Relation-like X -defined Function-like total Graph-yielding for set ;

existence

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

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

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

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

proof end;

end;

registration

let G be _Graph;

cluster G .componentSet() -> mutually-disjoint ;

coherence

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

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

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

proof end;

end;

registration

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

cluster W .reverse() -> minlength ;

coherence

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

proof end;

end;

registration

cluster non empty Relation-like Function-like Graph-yielding non connected non acyclic for set ;

existence

proof end;

end;

registration

cluster non empty Relation-like Function-like Graph-yielding non edgeless for set ;

existence

proof end;

end;

registration

cluster non empty Relation-like Function-like Graph-yielding non loopfull for set ;

existence

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

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

proof end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] Tree-like plain countable non 0 -vertex for Subgraph of G;

existence

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

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

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 b₃ -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 b₃ -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 b₃ -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

proof end;

theorem Th107: :: GLIBPRE1:104

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 b₃ -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 b₃ -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

proof end;

end;

registration

let S be Graph-membered \/-tolerating set ;

cluster -> \/-tolerating for Element of bool S;

coherence

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;