:: Miscellaneous Graph Preliminaries, {I}
:: by Sebastian Koch
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RELAT_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, FINSEQ_1,
NAT_1, FUNCT_4, FUNCOP_1, ZFMISC_1, CARD_1, ARYTM_3, CARD_2, ORDINAL2,
XXREAL_0, PBOOLE, GLIB_000, RING_3, GLIB_002, PARTFUN1, FUNCT_2, CHORD,
SCMYCIEL, REWRITE1, ARYTM_1, GLIB_006, GLIB_007, GLIB_009, GLIB_010,
GLIB_012, WAYBEL_0, MOD_4, RELAT_2, GRAPH_1, GLIB_001, ABIAN, SGRAPH1,
TREES_1, MSUALG_6, EQREL_1, GLIB_013, GLIB_014, RCOMP_1, MSAFREE2,
FUNCT_7, HELLY, INT_1, TAXONOM2, CARD_3, AOFA_I00;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1,
RELAT_1, FUNCT_1, RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, CARD_1, PBOOLE, ORDERS_1,
CARD_3, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, INT_1, VALUED_0,
NAT_D, CARD_2, FINSEQ_1, EQREL_1, NEWTON, ABIAN, FINSEQ_6, GLIB_000,
FINSEQ_8, GRAPH_2, TAXONOM2, COMPUT_1, GLIB_001, GLIB_002, CHORD, HELLY,
AOFA_I00, GLIB_006, GLIB_007, GLIB_008, GLIB_009, GLIB_010, GLIB_011,
GLIBPRE0, GLIB_012, GLIB_013, GLIB_014, GLUNIR00;
constructors DOMAIN_1, FUNCT_4, NAT_1, NAT_D, BINOP_2, CARD_2, FINSEQ_4,
PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, SQUARE_1, GLIB_000,
NEWTON, XTUPLE_0, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_008,
GLIB_009, GLIB_010, GLIB_011, GLIB_001, ABIAN, BINOP_1, FINSOP_1,
RVSUM_1, FINSEQ_5, GRAPH_5, FUNCT_2, FIB_NUM2, FINSEQ_8, HELLY, FUNCT_3,
GRAPH_2, FINSEQ_6, FUNCT_7, FINSEQ_1, SUBSET_1, RELAT_1, ENUMSET1,
ORDINAL1, INT_1, XXREAL_0, XREAL_0, XCMPLX_0, GLIB_012, PARTFUN2,
ORDERS_1, TOLER_1, TAXONOM2, SETFAM_1, COMPUT_1, EQREL_1, GLIBPRE0,
GLIB_013, GLIB_014, GLUNIR00, WELLORD1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSET_1, XREAL_0, NAT_1, CARD_1, FINSEQ_1, FINSEQ_4, FUNCT_2, PARTFUN1,
RELSET_1, GLIB_000, CHORD, GLIB_002, GLIB_006, GLIB_007, GLIB_009,
GLIB_008, GLIB_010, GLIB_011, SQUARE_1, NEWTON, XTUPLE_0, ABIAN,
GLIB_001, NUMBERS, MEMBERED, INT_1, CARD_3, RFINSEQ, GRAPH_2, GLIB_012,
SETFAM_1, COMPUT_1, ZFMISC_1, OPOSET_1, RELAT_2, GLIBPRE0, GLIB_013,
GLIB_014, ORDERS_1, ORDINAL5, EQREL_1, MSAFREE5, PRE_POLY;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: Preliminaries not directly related to graphs
:: 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 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X7 &
X7 in X1);
:: 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 & X2 in X3 & X3 in X4 & X4 in X5 & X5 in X6 & X6 in X7 &
X7 in X8 & X8 in X1);
:: into FUNCT_1 ?
registration
cluster one-to-one constant -> trivial for Function;
end;
:: into FUNCT_1 ?
theorem :: GLIBPRE1:3
for f being Function
holds f is non empty constant iff ex y being object st rng f = {y};
:: into PBOOLE ?
registration
let X be set;
cluster one-to-one for ManySortedSet of X;
end;
:: into PBOOLE ?
registration
let X be set;
cluster total one-to-one for X-defined Function;
end;
:: into PBOOLE ?
registration
let X be non empty set;
cluster total one-to-one non empty for X-defined Function;
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 {C, D() -> non empty set, F(Element of C()) -> object} :
ex f being Function of C(),D() st
for x being Element of C() holds f.x=F(x)
provided
for x being Element of C() holds F(x) in D();
:: into FUNCOP_1 ?
theorem :: GLIBPRE1:4
for f being one-to-one Function, y being object st rng f = {y}
ex x being object st f = x .--> y;
:: into FUNCOP_1 ?
registration
let f be one-to-one Function;
cluster f~ -> one-to-one;
end;
:: into FUNCT_3 or FUNCOP_1 ?
registration
let f be Function, g be one-to-one Function;
cluster <: f,g :> -> one-to-one;
cluster <: g,f :> -> one-to-one;
end;
:: into FUNCT_3 or FUNCOP_1 ?
theorem :: GLIBPRE1:5
for f being empty Function holds .:f = {} .--> {};
:: into FUNCT_3 ?
registration
let f be one-to-one Function;
cluster .:f -> one-to-one;
end;
:: into FUNCT_3 ?
theorem :: 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) = the set of all f.:x where x is Element of X;
:: into FUNCT_4 ?
theorem :: GLIBPRE1:7
for f being Function, g, h being one-to-one Function
st h = f +* g holds h"|rng g = g";
:: special case of FUNCT_7:10, compare FUNCT_7:9, FUNCT_7:11
:: into FUNCT_4 ?
theorem :: GLIBPRE1:8
for f, g, h being Function st rng f c= dom h holds (g +* h)*f = h*f;
:: into FUNCT_4 ?
theorem :: GLIBPRE1:9
for f being Function, g being one-to-one Function
holds (f +* g)*(g") = id rng g;
:: into RELAT_2 or ORDERS_1 ?
registration
cluster reflexive connected -> strongly_connected for Relation;
end;
:: into RELSET_1 or ORDERS_1 ?
theorem :: GLIBPRE1:10
for X being set, R being Relation of X
holds R is antisymmetric iff R \ id X is asymmetric;
:: into EQREL_1 or TAXONOM2 ?
theorem :: GLIBPRE1:11
for X being set st X is mutually-disjoint
holds X \ {{}} is a_partition of union X;
:: into EQREL_1 or TAXONOM2 ?
registration
let X be set;
cluster -> mutually-disjoint for a_partition of X;
end;
:: compare CARD_2:86, Proof mostly copied from there
:: into CARD_2 ?
theorem :: GLIBPRE1:12
for M,N being Cardinal, f being Function holds
(M c= card dom f & for x being object st x in dom f
holds N c= card (f.x)) implies M*`N c= Sum Card f;
:: into CARD_3 ?
theorem :: GLIBPRE1:13
for X, x being set st x in X holds (disjoin Card id X).x = [: card x, {x} :];
:: into CARD_3 or TAXONOM2 ?
theorem :: GLIBPRE1:14
for X being set st X is mutually-disjoint holds Sum Card id X = card union X;
:: compare CARD_2:87, Proof mostly copied from there
:: into CARD_2 ?
theorem :: GLIBPRE1:15
for X being set, 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;
:: into COMPUT_1 ?
theorem :: GLIBPRE1:16
for F being compatible functional 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;
begin :: into GLIB_000
registration
let G be non _trivial _Graph;
cluster non empty proper for Subset of the_Vertices_of G;
end;
theorem :: GLIBPRE1:17
for G being _Graph, X being set holds G.edgesBetween(X,X) = G.edgesBetween(X)
;
theorem :: GLIBPRE1:18
for G being _Graph holds G is _trivial iff the_Vertices_of G is trivial;
theorem :: GLIBPRE1:19
for G1 being _Graph, G2 being Subgraph of G1
holds G2 is inducedSubgraph of G1, the_Vertices_of G2, the_Edges_of G2;
theorem :: GLIBPRE1:20
for G1, G2 being _Graph, G3 being spanning Subgraph of G1
st G2 == G3 holds G2 is spanning Subgraph of G1;
theorem :: GLIBPRE1:21
for G being _Graph, 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});
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);
:: generalization of GLIB_000:def 52
theorem :: GLIBPRE1:23
for G being _Graph, v being Vertex of G
holds v is endvertex iff v.degree() = 1;
theorem :: GLIBPRE1:24
for G being loopless _Graph, 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};
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;
:: basic Proof copied from NAT --> G -> Graph-yielding
registration
let X be set, G be _Graph;
cluster X --> G -> Graph-yielding;
end;
registration
let x be object, G be _Graph;
cluster x .--> G -> Graph-yielding;
end;
registration
let X be set;
cluster Graph-yielding for ManySortedSet of X;
end;
registration
let X be non empty set;
cluster non empty Graph-yielding for ManySortedSet of X;
end;
definition
let X be non empty set, f be Graph-yielding ManySortedSet of X;
let x be Element of X;
redefine func f.x -> _Graph;
end;
begin
registration
let G being _Graph, P being Path of G;
cluster P.vertexSeq() | P.length() -> one-to-one;
end;
:: compare GLIB_001:154
theorem :: GLIBPRE1:26
for G being _Graph, P being Path of G holds P.length() c= G.order();
:: compare GLIB_001:144
theorem :: GLIBPRE1:27
for G being _Graph, T being Trail of G holds T.length() c= G.size();
theorem :: GLIBPRE1:28
for G being _Graph, W being Walk of G st len W = 3 or W.length() = 1
ex e being object st e Joins W.first(),W.last(),G &
W = G.walkOf(W.first(),e,W.last());
theorem :: GLIBPRE1:29
for G being _Graph, W being Walk of G, e being object
st e in W.edges() & not e in G.loops() & W is Circuit-like
ex e0 being object st e0 in W.edges() & e0 <> e;
:: compare GLIB_001:149 and CHORD:93
theorem :: GLIBPRE1:30
for G being _Graph, P being Path of G, 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;
:: cutting a closed walk at an edge
theorem :: GLIBPRE1:31
for G being _Graph, W being closed Walk of G, 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);
:: extension of GLIB_001:157
theorem :: GLIBPRE1:32
for G being _Graph, W1 being Walk of G, e,x,y being object
st e Joins x,y,G & e in W1.edges() & W1 is Cycle-like
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);
theorem :: GLIBPRE1:33
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
holds len W1 <= len W2 iff W1.length() <= W2.length();
theorem :: GLIBPRE1:34
for G being _Graph, W being Walk of G
holds W.length() = W.reverse().length();
theorem :: GLIBPRE1:35
for G being _Graph, W being Walk of G, e being object
st not e in W.last().edgesInOut() holds W.addEdge(e) = W;
theorem :: GLIBPRE1:36
for G being _Graph, W being Walk of G, e,x being object
st e Joins W.last(),x,G holds W.addEdge(e).length() = W.length() + 1;
theorem :: GLIBPRE1:37
for G1 being _Graph, E being set, G2 being removeEdges of G1, E
for W1 being Walk of G1 st W1.edges() misses E holds W1 is Walk of G2;
begin :: into GLIB_002
theorem :: GLIBPRE1:38
for G1, G2 being _Graph, G3 being Component of G1 st G2 == G3
holds G2 is Component of G1;
theorem :: GLIBPRE1:39
for G1, G2 being _Graph, G3 being Component of G1 st G1 == G2
holds G3 is Component of G2;
:: or into HELLY
theorem :: GLIBPRE1:40
for G being Tree-like _Graph, H being spanning Subgraph of G
st H is connected holds G == H;
registration
let G be _Graph;
cluster -> non empty for Element of G.componentSet();
end;
registration
let G be _Graph;
cluster G.componentSet() -> mutually-disjoint;
end;
begin :: into CHORD
theorem :: GLIBPRE1:41
for G being _Graph, v,w being Vertex of G
holds v,w are_adjacent iff w in v.allNeighbors();
:: the necessary existence clustering is from _008, but should be in _002
theorem :: GLIBPRE1:42
for G being _Graph, S being set, v being Vertex of G
st not v in S & S meets G.reachableFrom(v) holds G.AdjacentSet(S) <> {};
:: 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;
end;
theorem :: GLIBPRE1:43
for G being complete _Graph, v being Vertex of G
holds the_Vertices_of G \ {v} c= v.allNeighbors();
theorem :: GLIBPRE1:44
for G being loopless complete _Graph, v being Vertex of G
holds v.allNeighbors() = the_Vertices_of G \ {v};
theorem :: GLIBPRE1:45
for G being simple complete _Graph, v being Vertex of G
holds v.degree()+`1 = G.order();
registration
let G be _Graph;
cluster trivial -> minlength for Walk of G;
cluster minlength Path-like for Walk of G;
end;
registration
let G be _Graph, W be minlength Walk of G;
cluster W.reverse() -> minlength;
end;
theorem :: GLIBPRE1:46
for G1 being _Graph, G2 being Subgraph of G1
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 & W1 is minlength holds W2 is minlength;
theorem :: GLIBPRE1:47
for G being _Graph, v being Vertex of G, W being Walk of G
st W is_Walk_from v,v holds W is minlength iff W = G.walkOf(v);
theorem :: GLIBPRE1:48
for G1, G2 being _Graph, W1 being Walk of G1, W2 being Walk of G2
st G1 == G2 & W1 = W2 & W1 is minlength holds W2 is minlength;
begin :: into GLIB_006
:: other direction of first part of GLIB_000:72 and GLIB_006:70
theorem :: 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;
theorem :: GLIBPRE1:50
for G1 being _Graph, G3 being Subgraph of G1, 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;
:: adding an edge to a tree makes it unicyclic
theorem :: GLIBPRE1:51
for G being Tree-like _Graph, v1,v2 being Vertex of G, e being object
for H being addEdge of G,v1,e,v2 st not e in the_Edges_of G holds
H is non acyclic & for W1, W2 being Walk of H
st W1 is Cycle-like & W2 is Cycle-like holds W1.edges() = W2.edges();
:: 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, e being object, 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;
theorem :: GLIBPRE1:53
for G2 being _Graph, v,e,w being object, 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};
theorem :: GLIBPRE1:54
for G2 being _Graph, v,v2 being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w, 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);
theorem :: GLIBPRE1:55
for G2 being _Graph, w,v2 being Vertex of G2, v,e being object
for G1 being addAdjVertex of G2,v,e,w, 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);
theorem :: GLIBPRE1:56
for G2 being _Graph, v being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w, 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};
theorem :: GLIBPRE1:57
for G2 being _Graph, v,e being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w, 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};
theorem :: GLIBPRE1:58
for G2 being _Graph, v being Vertex of G2, 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}};
theorem :: GLIBPRE1:59
for G2 being _Graph, v,e being object, 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}};
theorem :: GLIBPRE1:60
for G2 being _Graph, v,e,w being object, G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 & W2 is minlength holds W1 is minlength;
:: 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));
theorem :: GLIBPRE1:62
for G2 being _Graph, v being Vertex of G2, e,w,x being object
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1, 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;
theorem :: GLIBPRE1:63
for G2 being _Graph, v,e,x being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for W1 being Walk of G1, 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;
registration
cluster non empty non non-Dmulti non non-multi for Graph-yielding Function;
end;
registration
cluster non empty non acyclic non connected for Graph-yielding Function;
end;
registration
cluster non empty non edgeless for Graph-yielding Function;
end;
registration
cluster non empty non loopfull for Graph-yielding Function;
end;
begin :: into GLIB_007
theorem :: GLIBPRE1:64
for G2,G3 being _Graph, V, E being set, 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;
theorem :: GLIBPRE1:65 :: ThD3
for G2,G3 being _Graph, 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;
theorem :: GLIBPRE1:66
for G2, G3 being _Graph, 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;
theorem :: GLIBPRE1:67
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is minlength iff W2 is minlength;
begin :: into GLIB_008
theorem :: GLIBPRE1:68
for G1 being edgeless _Graph, G2 being _Graph
holds G1 is Subgraph of G2 iff the_Vertices_of G1 c= the_Vertices_of G2;
registration
cluster loopless non edgeless for _Graph;
end;
begin :: into GLIB_009
registration
let G be _Graph;
cluster plain spanning acyclic for Subgraph of G;
cluster plain Tree-like for Subgraph of G;
cluster plain for Component of G;
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);
theorem :: GLIBPRE1:70
for G being _Graph, H being removeLoops of G
holds the_Edges_of G = G.loops() iff H is edgeless;
theorem :: GLIBPRE1:71
for G being _Graph, H being removeLoops of G, H9 being loopless Subgraph of G
holds H9 is Subgraph of H;
theorem :: GLIBPRE1:72
for G1 being _Graph, G2 being removeLoops of G1
for W1 being minlength Walk of G1 holds W1 is Walk of G2;
theorem :: GLIBPRE1:73
for G1 being _Graph, G2 being removeLoops of G1
for W1 being Walk of G1, W2 being Walk of G2
st W1 = W2 holds W1 is minlength iff W2 is minlength;
theorem :: GLIBPRE1:74
for G1 being _Graph, G2 being removeLoops of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff v2,w2 are_adjacent;
theorem :: GLIBPRE1:75
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff v2,w2 are_adjacent;
theorem :: GLIBPRE1:76
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 holds v1,w1 are_adjacent iff v2,w2 are_adjacent;
theorem :: GLIBPRE1:77
for G1 being _Graph, G2 being SimpleGraph of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff v2,w2 are_adjacent;
theorem :: GLIBPRE1:78
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1,w1 being Vertex of G1, v2,w2 being Vertex of G2
st v1 = v2 & w1 = w2 & v1 <> w1
holds v1,w1 are_adjacent iff v2,w2 are_adjacent;
begin :: into GLIB_010
theorem :: GLIBPRE1:79
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v2 = F_V.v1 & F is total
holds F_V.:G1.reachableFrom(v1) c= G2.reachableFrom(v2);
:: 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 :: GLIBPRE1:80
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 in dom F_V & v2 = F_V.v1 & F is one-to-one onto
holds G2.reachableFrom(v2) c= F_V.:G1.reachableFrom(v1);
theorem :: GLIBPRE1:81
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v2 = F_V.v1 & F is isomorphism
holds F_V.:G1.reachableFrom(v1) = G2.reachableFrom(v2);
theorem :: GLIBPRE1:82
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G2.componentSet() =
the set of all F_V.:C where C is Element of G1.componentSet();
theorem :: GLIBPRE1:83
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1.numComponents() = G2.numComponents();
registration
let G be loopless _Graph;
cluster G-isomorphic -> loopless for _Graph;
end;
theorem :: GLIBPRE1:84
for G1, G2, G3, G4 being _Graph, F1 being empty PGraphMapping of G1, G2
for F2 being empty PGraphMapping of G3, G4 holds F1 = F2;
theorem :: GLIBPRE1:85
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F | dom F = F & (rng F) |` F = F;
theorem :: GLIBPRE1:86
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is total holds (rng F) |` F is total;
theorem :: GLIBPRE1:87
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto holds F | dom F is onto;
theorem :: GLIBPRE1:88
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F is PGraphMapping of G1, rng F;
theorem :: GLIBPRE1:89
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
holds F is PGraphMapping of dom F, G2;
:: Proof mostly taken from GLIB_010:46, generalization of the same
theorem :: GLIBPRE1:90
for G1, G2 being _Graph, 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);
:: generalization of GLIB_010:7 and GLIB_010:46
theorem :: GLIBPRE1:91
for G1, G2 being _Graph, F being PGraphMapping of G1, G2, V being set
holds F_E.:G1.edgesBetween(V) c= G2.edgesBetween(F_V.:V);
:: generalization of GLIB_010:86
theorem :: GLIBPRE1:92
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for X,Y being Subset of the_Vertices_of G1 st F is weak_SG-embedding onto
holds F_E.:G1.edgesBetween(X,Y) = G2.edgesBetween(F_V.:X,F_V.:Y);
:: generalization of GLIB_010:87
theorem :: GLIBPRE1:93
for G1, G2 being _Graph, F being PGraphMapping of G1, G2, V being set
st F is continuous holds F_E.:G1.edgesBetween(V) = G2.edgesBetween(F_V.:V);
theorem :: GLIBPRE1:94
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2
holds (F"W2).vertices() = F_V"W2.vertices();
theorem :: GLIBPRE1:95
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2
holds (F"W2).edges() = F_E"W2.edges();
theorem :: GLIBPRE1:96
for G1, G2 being _Graph, F being non empty one-to-one PGraphMapping of G1, G2
for W2 being F-valued Walk of G2, v,w being object
holds W2 is_Walk_from v,w implies F"W2 is_Walk_from F"_V.v, F"_V.w;
theorem :: GLIBPRE1:97
for G1, G2 being _Graph, F being one-to-one PGraphMapping of G1, G2
for v1 being Vertex of G1, v2 being Vertex of G2
st v2 = F_V.v1 & F is isomorphism
holds F_V"G2.reachableFrom(v2) = G1.reachableFrom(v1);
theorem :: GLIBPRE1:98
for G1, G2 being _Graph
for F being PGraphMapping of G1, G2, H being Subgraph of G2
holds F_E"the_Edges_of H c= G1.edgesBetween(F_V"the_Vertices_of H);
theorem :: GLIBPRE1:99
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1, G2, 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;
theorem :: GLIBPRE1:100
for G1, G2 being _Graph, 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);
theorem :: GLIBPRE1:101
for G1, G2 being _Graph, 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
;
theorem :: GLIBPRE1:102
for G1, G2 being _Graph, 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;
theorem :: GLIBPRE1:103
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1, G2, 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 F-defined Walk of G1;
theorem :: GLIBPRE1:104
for G1, G2 being _Graph
for F being non empty PGraphMapping of G1, G2, 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 F-defined Walk of G1 st W1 is Walk of H1
holds F.:W1 is Walk of H2;
theorem :: GLIBPRE1:105
for G1, G2 being _Graph, F being non empty PGraphMapping of G1, G2
for H being Subgraph of rng F, W being Walk of H
holds W is F-valued Walk of G2;
theorem :: GLIBPRE1:106
for G1, G2 being _Graph, 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 F-valued Walk of G2 st W2 is Walk of H2
holds F"W2 is Walk of H1;
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;
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;
:: 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 :: GLIBPRE1:109
for G1, G2 being _Graph, 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
(F9 is non 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);
theorem :: GLIBPRE1:110
for G1, G2 being _Graph, 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 strong_SG-embedding implies F9 is Disomorphism);
begin :: into GLIB_013
:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem :: GLIBPRE1:111
for G1 being vertex-finite Dsimple _Graph, G2 being DGraphComplement of G1
for v1 being Vertex of G1, 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);
:: or into GLIB_012 (vertex-finite can be replaced by _finite)
theorem :: GLIBPRE1:112
for G1 being vertex-finite simple _Graph, G2 being GraphComplement of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.degree() = G1.order() - (v1.degree()+1);
theorem :: GLIBPRE1:113
for G being vertex-finite Dsimple _Graph, v being Vertex of G
holds v.inDegree() < G.order() & v.outDegree() < G.order();
theorem :: GLIBPRE1:114
for G being vertex-finite simple _Graph, v being Vertex of G
holds v.degree() < G.order();
registration
cluster 1-edge -> non-multi for _Graph;
end;
begin :: into GLIB_014
registration
let S be \/-tolerating Graph-membered set;
cluster -> \/-tolerating for Subset of S;
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;
theorem :: GLIBPRE1:116
for S being GraphUnionSet, G being GraphUnion of S
for e,v,w being object st e DJoins v,w,G
ex H being Element of S st e DJoins v,w,H;
theorem :: GLIBPRE1:117
for S being GraphUnionSet, G being GraphUnion of S
for e,v,w being object st e Joins v,w,G
ex H being Element of S st e Joins v,w,H;
theorem :: GLIBPRE1:118
for S1, S2 being GraphUnionSet
for G1 being (GraphUnion of S1), 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;
theorem :: GLIBPRE1:119
for S1, S2 being GraphUnionSet
for G1 being (GraphUnion of S1), G2 being GraphUnion of S2
st S2 c= S1 holds G2 is Subgraph of G1;
theorem :: GLIBPRE1:120
for G1, G2 being _Graph, 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();
theorem :: GLIBPRE1:121
for G1, G2 being _Graph, 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();
theorem :: GLIBPRE1:122
for G1, G2 being connected _Graph, G being GraphUnion of G1, G2
st the_Vertices_of G1 meets the_Vertices_of G2 holds G is connected;
theorem :: GLIBPRE1:123
for G1, G2 being _Graph, G being GraphUnion of G1, G2, W being Walk of G
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds W is Walk of G1 or W is Walk of G2;
theorem :: GLIBPRE1:124
for G1, G2 being _Graph, G being GraphUnion of G1, G2
for v1 being Vertex of G1, v being Vertex of G
st the_Vertices_of G1 misses the_Vertices_of G2
holds v = v1 implies G.reachableFrom(v) = G1.reachableFrom(v1);
theorem :: GLIBPRE1:125
for G1, G2 being _Graph, G being GraphUnion of G1, G2
for v2 being Vertex of G2, v being Vertex of G
st G1 tolerates G2 & the_Vertices_of G1 misses the_Vertices_of G2
holds v = v2 implies G.reachableFrom(v) = G2.reachableFrom(v2);
theorem :: GLIBPRE1:126
for G1, G2 being _Graph, 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();
begin :: into GLUNIR00
theorem :: GLIBPRE1:127
for V being non empty set, E being Relation of V
holds createGraph(V,E).loops() = E /\ id V;
theorem :: GLIBPRE1:128
for V being non empty set, E being Relation of V
holds createGraph(V, E \ id V) is removeLoops of createGraph(V,E);