:: by Sebastian Koch

::

:: Received March 30, 2021

:: Copyright (c) 2021 Association of Mizar Users

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 )

( 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 ?

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

( 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

coherence

for b_{1} being Function st b_{1} is one-to-one & b_{1} is constant holds

b_{1} is trivial

end;
for b

b

proof 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} )

( ( not f is empty & f is constant ) iff ex y being object st rng f = {y} )

proof end;

:: into PBOOLE ?

registration
end;

:: into PBOOLE ?

registration

let X be set ;

existence

ex b_{1} being X -defined Function st

( b_{1} is total & b_{1} is one-to-one )

end;
existence

ex b

( b

proof end;

:: into PBOOLE ?

registration

let X be non empty set ;

existence

ex b_{1} being X -defined Function st

( b_{1} is total & b_{1} is one-to-one & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

:: this is a variant of FUNCT_2:sch 4 which can be used a little bit easier

:: into FUNCT_2 ?

:: into FUNCT_2 ?

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

for y being object st rng f = {y} holds

ex x being object st f = x .--> y

proof end;

:: into FUNCOP_1 ?

registration
end;

:: into FUNCT_3 or FUNCOP_1 ?

registration

let f be Function;

let g be one-to-one Function;

coherence

<:f,g:> is one-to-one

<:g,f:> is one-to-one

end;
let g be one-to-one Function;

coherence

<:f,g:> is one-to-one

proof end;

coherence <:g,f:> is one-to-one

proof end;

:: into FUNCT_3 or FUNCOP_1 ?

:: into FUNCT_3 ?

registration
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 }

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 ?

:: special case of FUNCT_7:10, compare FUNCT_7:9, FUNCT_7:11

:: into FUNCT_4 ?

:: into FUNCT_4 ?

:: into FUNCT_4 ?

:: into RELAT_2 or ORDERS_1 ?

registration

coherence

for b_{1} being Relation st b_{1} is reflexive & b_{1} is connected holds

b_{1} is strongly_connected

end;
for b

b

proof end;

:: into RELSET_1 or ORDERS_1 ?

:: into EQREL_1 or TAXONOM2 ?

:: into EQREL_1 or TAXONOM2 ?

registration

let X be set ;

coherence

for b_{1} being a_partition of X holds b_{1} is mutually-disjoint

end;
coherence

for b

proof end;

:: compare CARD_2:86, Proof mostly copied from there

:: into CARD_2 ?

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

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 ?

:: into CARD_3 or TAXONOM2 ?

:: compare CARD_2:87, Proof mostly copied from there

:: into CARD_2 ?

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

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

( 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;

existence

ex b_{1} being Subset of (the_Vertices_of G) st

( not b_{1} is empty & b_{1} is proper )

end;
existence

ex b

( not b

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

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

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

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

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

( 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
end;

registration

let X be non empty set ;

existence

ex b_{1} being ManySortedSet of X st

( not b_{1} is empty & b_{1} is Graph-yielding )

end;
existence

ex b

( not b

proof 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

end;
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;

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;

coherence

(P .vertexSeq()) | (P .length()) is one-to-one

end;
let P be Path of G;

coherence

(P .vertexSeq()) | (P .length()) is one-to-one

proof end;

:: compare GLIB_001:154

:: compare GLIB_001:144

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

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 )

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

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

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

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

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

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

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

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;

:: or into HELLY

registration

let G be _Graph;

coherence

for b_{1} being Element of G .componentSet() holds not b_{1} is empty

end;
coherence

for b

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 <> {}

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

coherence

not G .AdjacentSet S is empty

end;
let S be non empty proper Subset of (the_Vertices_of G);

coherence

not G .AdjacentSet S is empty

proof 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()

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}

for v being Vertex of G holds v .allNeighbors() = (the_Vertices_of G) \ {v}

proof end;

registration

let G be _Graph;

coherence

for b_{1} being Walk of G st b_{1} is V5() holds

b_{1} is minlength

ex b_{1} being Walk of G st

( b_{1} is minlength & b_{1} is Path-like )

end;
coherence

for b

b

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 b

( b

proof end;

registration
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

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 )

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

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 )

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

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

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

( 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} )

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

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

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}

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}

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

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

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

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

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

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

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

existence

ex b_{1} being Graph-yielding Function st

( not b_{1} is empty & not b_{1} is non-Dmulti & not b_{1} is non-multi )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being Graph-yielding Function st

( not b_{1} is empty & not b_{1} is acyclic & not b_{1} is connected )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being Graph-yielding Function st

( not b_{1} is empty & not b_{1} is edgeless )

end;
ex b

( not b

proof end;

registration

existence

ex b_{1} being Graph-yielding Function st

( not b_{1} is empty & not b_{1} is loopfull )

end;
ex b

( not b

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

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 )

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 )

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 )

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 )

for G2 being _Graph holds

( G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2 )

proof end;

registration

ex b_{1} being _Graph st

( b_{1} is loopless & not b_{1} is edgeless )
end;

cluster Relation-like NAT -defined Function-like V42() [Graph-like] loopless non edgeless countable non 0 -vertex for set ;

existence ex b

( b

proof end;

registration

let G be _Graph;

ex b_{1} being Subgraph of G st

( b_{1} is plain & b_{1} is spanning & b_{1} is acyclic )

ex b_{1} being Subgraph of G st

( b_{1} is plain & b_{1} is Tree-like )

ex b_{1} being Component of G st b_{1} is plain

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

existence ex b

( b

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 b

( b

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 b

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

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

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

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 )

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 )

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 )

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 )

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 )

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 )

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

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)

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

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

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 }

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

for F being PGraphMapping of G1,G2 st F is isomorphism holds

G1 .numComponents() = G2 .numComponents()

proof end;

registration

let G be loopless _Graph;

for b_{1} being _Graph st b_{1} is G -isomorphic holds

b_{1} is loopless

end;
cluster Relation-like NAT -defined Function-like V42() [Graph-like] G -isomorphic -> loopless for set ;

coherence for b

b

proof 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

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 )

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

for F being PGraphMapping of G1,G2 st F is total holds

(rng F) |` F is total

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

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)

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

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)

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_{3} -valued Walk of G2 holds (F " W2) .vertices() = (F _V) " (W2 .vertices())

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

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_{3} -valued Walk of G2 holds (F " W2) .edges() = (F _E) " (W2 .edges())

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

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_{3} -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;

for F being non empty one-to-one PGraphMapping of G1,G2

for W2 being b

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

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

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

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

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

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)

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 b_{3} -defined Walk of G1

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 b

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 b_{3} -defined Walk of G1 st W1 is Walk of H1 holds

F .: W1 is Walk of H2

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 b

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 b_{3} -valued Walk of G2

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

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_{3} -valued Walk of G2 st W2 is Walk of H2 holds

F " W2 is Walk of H1

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

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

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

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

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

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

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

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)

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

for v being Vertex of G holds

( v .inDegree() < G .order() & v .outDegree() < G .order() )

proof end;

registration
end;

registration

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

coherence

for b_{1} being Subset of S holds b_{1} is \/-tolerating

end;
coherence

for b

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

( 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

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

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

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

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

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

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

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;

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

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

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

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)

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

for E being Relation of V holds createGraph (V,(E \ (id V))) is removeLoops of (createGraph (V,E))

proof end;

:: into XREGULAR ?