:: Miscellaneous Graph Preliminaries
:: by Sebastian Koch
::
:: Received December 30, 2019
:: Copyright (c) 2019-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, FINSEQ_1, SUBSET_1, RELAT_1, FUNCT_1, TARSKI, ARYTM_3,
CARD_1, XBOOLE_0, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1, RELAT_2,
FUNCT_2, GLIB_009, MOD_4, WAYBEL_0, GLIB_006, GLIB_007, FUNCT_4,
ORDINAL2, CARD_2, SCMYCIEL, SGRAPH1, GLIB_010, MATRIX11, BSPACE,
SETFAM_1, ORDINAL1, FUNCT_7, YELLOW_1, WELLORD2, CHORD, NAT_1, GLIB_002,
XXREAL_0, CARD_3, FUNCOP_1, PBOOLE, EQREL_1, RFINSEQ, FINSEQ_8, GRAPH_2,
ORDINAL4, RING_3, GLIB_011, ARYTM_1, GLIB_001;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
ENUMSET1, FUNCT_1, RELAT_2, ORDINAL1, RELSET_1, PARTFUN1, WELLORD2,
FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CHORD,
PARTFUN2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, INT_1, VALUED_0, NAT_D,
CARD_2, FINSEQ_1, EQREL_1, FINSEQ_2, FINSEQ_4, NEWTON, FUNCT_7, RFINSEQ,
FINSEQ_6, FINSEQ_8, ORDERS_1, CARD_3, ABIAN, GLIB_000, GLIB_001,
STRUCT_0, ORDERS_2, GROUP_1, GROUP_2, GROUP_6, YELLOW_1, SGRAPH1,
MATRIX11, GLIB_002, GLIB_003, BSPACE, ORDERS_5, GLIB_006, GLIB_007,
GLIB_008, GLIB_009, GLIB_010, GLIB_011;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
GROUP_6, GLIB_006, GLIB_007, PARTFUN2, BSPACE, SETWISEO, CHORD, RAT_1,
MATRIX11, GLIB_008, FUNCT_7, GLIB_009, GLIB_010, SQUARE_1, NEWTON,
VALUED_0, CLASSES1, FINSEQ_2, SGRAPH1, ORDERS_2, YELLOW_1, RFINSEQ,
GRAPH_2, FINSEQ_8, GLIB_011, FINSEQ_6, ENUMSET1, ORDERS_5;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
XREAL_0, NAT_1, FINSEQ_1, GLIB_000, CARD_1, FUNCT_2, RELSET_1, XTUPLE_0,
CARD_3, GLIB_006, GLIB_008, GLIB_009, GLIB_010, MSAFREE5, GRFUNC_1,
RELAT_2, SUBSET_1, GLIB_011;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin :: Preliminaries not directly related to graphs
:: generalization of XBOOLE_1:45
:: into XBOOLE_1 ?
theorem :: GLIBPRE0:1
for X,Y,Z being set st Z c= X holds X \/ (Y \ Z) = X \/ Y;
:: generalization of XBOOLE_1:89
:: into XBOOLE_1 ?
theorem :: GLIBPRE0:2
for X, Y, Z being set holds X /\ Z misses Y \ Z;
:: into ZFMISC_1 ?
theorem :: GLIBPRE0:3
for x,y being object holds {x,y}\{the Element of {x,y}} = {} iff x = y;
:: into ZFMISC_1 ?
theorem :: GLIBPRE0:4
for a,b,x,y being object st a <> b & x = the Element of {a,b} &
y = the Element of ({a,b}\{the Element of {a,b}})
holds x = a & y = b or x = b & y = a;
:: into ZFMISC_1 ?
theorem :: GLIBPRE0:5
for a,b,x,y being object holds {a,b} = {x,y} iff
x = a & y = b or x = b & y = a;
:: into SUBSET_1 ?
theorem :: GLIBPRE0:6
for X being set, Y being non empty set
holds X c< Y iff X is proper Subset of Y;
registration
let X be non empty set;
cluster id X -> non irreflexive;
cluster [: X, X :] -> non irreflexive non asymmetric;
cluster non irreflexive non asymmetric for Relation of X;
cluster symmetric irreflexive non total for Relation of X;
cluster symmetric non irreflexive non empty for Relation of X;
end;
registration
let X be non trivial set;
cluster id X -> non connected;
cluster symmetric non connected for Relation of X;
cluster [: X, X :] -> non antisymmetric;
cluster non antisymmetric for Relation of X;
end;
:: into RELAT_1 ?
theorem :: GLIBPRE0:7
for R,S being Relation, X being set holds (R\/S).:X = R.:X \/ S.:X;
:: into RELAT_1 ?
theorem :: GLIBPRE0:8
for R,S being Relation, Y being set holds (R\/S)"Y = R"Y \/ S"Y;
:: into RELAT_1 ?
theorem :: GLIBPRE0:9
for R being Relation, X,Y being set holds Y|`R|X = Y|`R /\ R|X;
:: into RELAT_2 ?
theorem :: GLIBPRE0:10
for R being symmetric Relation, x being object holds Im(R,x) = Coim(R,x);
:: into RELSET_1 ?
theorem :: GLIBPRE0:11
for X being set, R being Relation of X
holds R is irreflexive iff id X misses R;
:: into ZFMISC_1 or SYSREL ? (in both cases the qua can be omitted)
theorem :: GLIBPRE0:12
for x,y being object holds ({[x,y]} qua Relation)~ = {[y,x]};
:: generalization of EQREL_1:6 (total is unneeded assumption)
:: into EQREL_1 ?
theorem :: GLIBPRE0:13
for X being set, x,y being object, R being symmetric Relation of X
holds [x,y] in R implies [y,x] in R;
:: into CARD_1 ?
registration
let a, b be Cardinal;
cluster a /\ b -> cardinal;
cluster a \/ b -> cardinal;
end;
:: into ORDINAL1 or WELLORD2 ?
registration
let X be c=-linear set;
cluster RelIncl X -> connected;
end;
:: into YELLOW_1 or ORDERS_5 ?
registration
let X be c=-linear set;
cluster InclPoset X -> connected;
end;
:: into CARD_1 ?
theorem :: GLIBPRE0:14
for X being non empty set
st for a being set st a in X holds a is cardinal number
ex A being Cardinal st A in X & A = meet X;
:: analogous to TOPGEN_2:3
:: into CARD_1 ?
theorem :: GLIBPRE0:15
for X being set st for a being set st a in X holds a is cardinal number
holds meet X is cardinal number;
:: into CARD_3 ?
registration
let f be Cardinal-yielding Function, x be object;
cluster f.x -> cardinal;
end;
registration
let X be functional set;
cluster meet X -> Function-like Relation-like;
end;
:: into PENCIL_1 ?
:: mostly copied from there
theorem :: GLIBPRE0:16
for X being set holds 4 c= card X iff
ex w,x,y,z being object st w in X & x in X & y in X & z in X &
w<>x & w<>y & w<>z & x<>y & x<>z & y<>z;
:: into PENCIL_1 ?
theorem :: GLIBPRE0:17
for X being set st 4 c= card X for w,x,y being object ex z being object
st z in X & w<>z & x<>z & y<>z;
:: into BSPACE or SGRAPH1 ?
theorem :: GLIBPRE0:18
for X being set holds singletons X misses 2Set X;
:: into SGRAPH1 or MATRIX11 ?
theorem :: GLIBPRE0:19
for X, Y being set st card X = card Y holds card 2Set X = card 2Set Y;
:: into MATRIX13 ?
theorem :: GLIBPRE0:20
for X being finite set holds card 2Set X = (card X) choose 2;
begin :: into GLIB_000
theorem :: GLIBPRE0:21
for G being _Graph, v being Vertex of G, e,w being object
st v is isolated holds not e Joins v,w,G;
theorem :: GLIBPRE0:22
for G being _Graph, v being Vertex of G, e,w being object
st v is isolated holds not e DJoins v,w,G & not e DJoins w,v,G;
:: into GLIB_000 ?
theorem :: GLIBPRE0:23
for G being _Graph, v being Vertex of G
holds v is isolated iff not v in rng the_Source_of G \/ rng the_Target_of G;
theorem :: GLIBPRE0:24
for G being _Graph, v being Vertex of G, e being object
st v is endvertex holds not e Joins v,v,G;
theorem :: GLIBPRE0:25
for G being _Graph, v being Vertex of G holds
v.edgesIn() = (the_Target_of G)"{v} & v.edgesOut() = (the_Source_of G)"{v};
theorem :: GLIBPRE0:26
for G being _trivial _Graph, v being Vertex of G holds
v.edgesIn() = the_Edges_of G & v.edgesOut() = the_Edges_of G &
v.edgesInOut() = the_Edges_of G;
theorem :: GLIBPRE0:27
for G being _trivial _Graph, v being Vertex of G holds
v.inDegree() = G.size() & v.outDegree() = G.size() &
v.degree() = G.size() +` G.size();
theorem :: GLIBPRE0:28
for G being _Graph, X, Y being set
holds G.edgesBetween(X,Y) = G.edgesDBetween(X,Y) \/ G.edgesDBetween(Y,X);
theorem :: GLIBPRE0:29
for G being _Graph, v being Vertex of G
holds v.edgesInOut() = G.edgesBetween(the_Vertices_of G,{v});
theorem :: GLIBPRE0:30
for G being _Graph, X,Y being set
holds G.edgesDBetween(X,Y) = G.edgesOutOf(X) /\ G.edgesInto(Y);
theorem :: GLIBPRE0:31
for G being _Graph, X, Y being set
holds G.edgesDBetween(X,Y) c= G.edgesBetween(X,Y);
:: generalized case for GLIB_000:19
theorem :: GLIBPRE0:32
for G being _Graph, v being Vertex of G
st for e being object holds not e Joins v,v,G
holds card v.edgesInOut() = v.degree();
theorem :: GLIBPRE0:33
for G being _Graph, v being Vertex of G
holds v is isolated iff v.edgesIn() = {} & v.edgesOut() = {};
theorem :: GLIBPRE0:34
for G being _Graph, v being Vertex of G
holds v is isolated iff v.inDegree() = 0 & v.outDegree() = 0;
:: generalization of GLIB_000:def 50
theorem :: GLIBPRE0:35
for G being _Graph, v being Vertex of G
holds v is isolated iff v.degree() = 0;
theorem :: GLIBPRE0:36
for G being _Graph, X being set
holds G.edgesInto(X) = union {v.edgesIn() where v is Vertex of G : v in X};
theorem :: GLIBPRE0:37
for G being _Graph, X being set
holds G.edgesOutOf(X) = union {v.edgesOut() where v is Vertex of G : v in X};
theorem :: GLIBPRE0:38
for G being _Graph, X being set holds G.edgesInOut(X)
= union {v.edgesInOut() where v is Vertex of G : v in X};
theorem :: GLIBPRE0:39
for G being _Graph, X, Y being set holds G.edgesDBetween(X,Y)
= union {v.edgesOut() /\ w.edgesIn()
where v, w is Vertex of G : v in X & w in Y};
theorem :: GLIBPRE0:40
for G being _Graph, X, Y being set holds G.edgesBetween(X,Y)
c= union {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y};
theorem :: GLIBPRE0:41
for G being _Graph, X, Y being set st X misses Y holds G.edgesBetween(X,Y)
= union {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y};
theorem :: GLIBPRE0:42
for G1 being _Graph, E being set, G2 being removeEdges of G1, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.edgesIn() = v1.edgesIn() \ E & v2.edgesOut() = v1.edgesOut() \ E &
v2.edgesInOut() = v1.edgesInOut() \ E;
theorem :: GLIBPRE0:43
for G1, G2 being _Graph, V being set
holds G2 is removeVertices of G1, V iff
G2 is removeVertices of G1, V /\ the_Vertices_of G1;
theorem :: GLIBPRE0:44
for G1 being _Graph, V being set, G2 being removeVertices of G1, V
for v1 being Vertex of G1, v2 being Vertex of G2
st V c< the_Vertices_of G1 & v1 = v2 holds
v2.edgesIn() = v1.edgesIn() \ G1.edgesOutOf(V) &
v2.edgesOut() = v1.edgesOut() \ G1.edgesInto(V) &
v2.edgesInOut() = v1.edgesInOut() \ G1.edgesInOut(V);
theorem :: GLIBPRE0:45
for G1 being non _trivial _Graph, v being Vertex of G1
for G2 being removeVertex of G1, v
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2 holds
v2.edgesIn() = v1.edgesIn() \ v.edgesOut() &
v2.edgesOut() = v1.edgesOut() \ v.edgesIn() &
v2.edgesInOut() = v1.edgesInOut() \ v.edgesInOut();
begin :: into GLIB_002
theorem :: GLIBPRE0:46
for G being _Graph, C being Component of G
for v1 being Vertex of G, v2 being Vertex of C st v1 = v2 holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();
begin :: into GLIB_006
theorem :: GLIBPRE0:47
for G2 being _Graph, V being set, G1 being addVertices of G2, V
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();
theorem :: GLIBPRE0:48
for G2 being _Graph, v,w,e being object, G1 being addEdge of G2,v,e,w
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & v2 <> v & v2 <> w holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();
theorem :: GLIBPRE0:49
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w for v1 being Vertex of G1
st not e in the_Edges_of G2 & v1 = v & v <> w holds
v1.edgesIn() = v.edgesIn() & v1.inDegree() = v.inDegree() &
v1.edgesOut() = v.edgesOut() \/ {e} & v1.outDegree() = v.outDegree() +` 1 &
v1.edgesInOut() = v.edgesInOut() \/ {e} & v1.degree() = v.degree() +` 1;
theorem :: GLIBPRE0:50
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w for w1 being Vertex of G1
st not e in the_Edges_of G2 & w1 = w & v <> w holds
w1.edgesIn() = w.edgesIn() \/ {e} & w1.inDegree() = w.inDegree() +` 1 &
w1.edgesOut() = w.edgesOut() & w1.outDegree() = w.outDegree() &
w1.edgesInOut() = w.edgesInOut() \/ {e} & w1.degree() = w.degree() +` 1;
theorem :: GLIBPRE0:51
for G2 being _Graph, v being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,v for v1 being Vertex of G1
st not e in the_Edges_of G2 & v1 = v holds
v1.edgesIn() = v.edgesIn() \/ {e} & v1.inDegree() = v.inDegree() +` 1 &
v1.edgesOut() = v.edgesOut() \/ {e} & v1.outDegree() = v.outDegree() +` 1 &
v1.edgesInOut() = v.edgesInOut() \/ {e} & v1.degree() = v.degree() +` 2;
begin :: into GLIB_007
theorem :: GLIBPRE0:52
for G3 being _Graph, E being set, G4 being reverseEdgeDirections of G3, E
for G1 being Supergraph of G3, G2 being reverseEdgeDirections of G1, E
st E c= the_Edges_of G3 holds G2 is Supergraph of G4;
:: counterpart of GLIB_007:55
theorem :: GLIBPRE0:53
for G2 being _Graph, v being object, G1 being addVertex of G2, v
holds G1 is addAdjVertexAll of G2,v,{};
theorem :: GLIBPRE0:54
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & E c= the_Edges_of G1 holds
v2.edgesIn() = (v1.edgesIn() \ E) \/ (v1.edgesOut() /\ E) &
v2.edgesOut() = (v1.edgesOut() \ E) \/ (v1.edgesIn() /\ E);
theorem :: GLIBPRE0:55
for G1 being _Graph, G2 being reverseEdgeDirections of G1
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v2.edgesIn() = v1.edgesOut() & v2.inDegree() = v1.outDegree() &
v2.edgesOut() = v1.edgesIn() & v2.outDegree() = v1.inDegree();
theorem :: GLIBPRE0:56
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.edgesInOut() = v1.edgesInOut() & v2.degree() = v1.degree();
theorem :: GLIBPRE0:57
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V, w being Vertex of G1
st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & v = w
holds w.allNeighbors() = V & w.degree() = card V;
theorem :: GLIBPRE0:58
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 & not v2 in V holds
v1.edgesIn() = v2.edgesIn() & v1.inDegree() = v2.inDegree() &
v1.edgesOut() = v2.edgesOut() & v1.outDegree() = v2.outDegree() &
v1.edgesInOut() = v2.edgesInOut() & v1.degree() = v2.degree();
theorem :: GLIBPRE0:59
for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2, v, V
for v1 being Vertex of G1, v2 being Vertex of G2
st not v in the_Vertices_of G2 & v1 = v2 & v2 in V holds
v1.allNeighbors() = v2.allNeighbors() \/ {v} &
v1.degree() = v2.degree() +` 1;
theorem :: GLIBPRE0:60
for G2 being _Graph, v being object, V being set
for G1 being addAdjVertexAll of G2, v, V
for v1 being Vertex of G1, v2 being Vertex of G2
st v1 = v2 holds
v1.degree() c= v2.degree() +` 1 &
v1.inDegree() c= v2.inDegree() +` 1 &
v1.outDegree() c= v2.outDegree() +` 1;
begin :: into GLIB_008
theorem :: GLIBPRE0:61
for G being _Graph holds G is edgeless iff
for v,w being Vertex of G holds not v,w are_adjacent;
theorem :: GLIBPRE0:62
for G being loopless _Graph holds G is edgeless iff
for v,w being Vertex of G st v <> w holds not v,w are_adjacent;
begin :: into GLIB_009
theorem :: GLIBPRE0:63
for G being _Graph
holds G.loops() = dom((the_Source_of G) /\ (the_Target_of G));
theorem :: GLIBPRE0:64
for G1, G2 being _Graph, E being set
holds G2 is reverseEdgeDirections of G1, E iff
G2 is reverseEdgeDirections of G1, E \ G1.loops();
theorem :: GLIBPRE0:65
for G1 being _Graph, G2 being removeLoops of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = v1.inNeighbors() \ {v1} &
v2.outNeighbors() = v1.outNeighbors() \ {v1} &
v2.allNeighbors() = v1.allNeighbors() \ {v1};
theorem :: GLIBPRE0:66
for G1 being _Graph, G2 being removeParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.allNeighbors() = v1.allNeighbors();
theorem :: GLIBPRE0:67
for G1 being _Graph, G2 being removeDParallelEdges of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = v1.inNeighbors() &
v2.outNeighbors() = v1.outNeighbors() &
v2.allNeighbors() = v1.allNeighbors();
theorem :: GLIBPRE0:68
for G1 being _Graph, G2 being SimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds v2.allNeighbors() = v1.allNeighbors() \ {v1};
theorem :: GLIBPRE0:69
for G1 being _Graph, G2 being DSimpleGraph of G1
for v1 being Vertex of G1, v2 being Vertex of G2 st v1 = v2
holds
v2.inNeighbors() = v1.inNeighbors() \ {v1} &
v2.outNeighbors() = v1.outNeighbors() \ {v1} &
v2.allNeighbors() = v1.allNeighbors() \ {v1};
registration
let G be non loopless _Graph;
cluster -> non loopless for removeParallelEdges of G;
cluster -> non loopless for removeDParallelEdges of G;
end;
registration
let G be non edgeless _Graph;
cluster -> non edgeless for removeParallelEdges of G;
cluster -> non edgeless for removeDParallelEdges of G;
end;
theorem :: GLIBPRE0:70
for G being _Graph, E being RepEdgeSelection of G
holds card E = card Class EdgeAdjEqRel(G);
theorem :: GLIBPRE0:71
for G being _Graph, E being RepDEdgeSelection of G
holds card E = card Class DEdgeAdjEqRel(G);
theorem :: GLIBPRE0:72
for G being _Graph, X being set, E being Subset of the_Edges_of G
for H being reverseEdgeDirections of G, X
holds E is RepEdgeSelection of G iff E is RepEdgeSelection of H;
theorem :: GLIBPRE0:73
for G being _Graph, V being non empty Subset of the_Vertices_of G
for H being (inducedSubgraph of G, V), E being RepEdgeSelection of G
holds E /\ G.edgesBetween(V) is RepEdgeSelection of H;
theorem :: GLIBPRE0:74
for G being _Graph, V being non empty Subset of the_Vertices_of G
for H being (inducedSubgraph of G, V), E being RepDEdgeSelection of G
holds E /\ G.edgesBetween(V) is RepDEdgeSelection of H;
theorem :: GLIBPRE0:75
for G being _Graph, V being set, H being addVertices of G, V
for E being Subset of the_Edges_of G
holds E is RepEdgeSelection of G iff E is RepEdgeSelection of H;
theorem :: GLIBPRE0:76
for G being _Graph, V being set, H being addVertices of G, V
for E being Subset of the_Edges_of G
holds E is RepDEdgeSelection of G iff E is RepDEdgeSelection of H;
registration
cluster non non-multi non-Dmulti for _Graph;
end;
definition
let GF be Graph-yielding Function;
attr GF is plain means
:: GLIBPRE0:def 1
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is plain;
end;
registration
let G be plain _Graph;
cluster <* G *> -> plain;
cluster NAT --> G -> plain;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is plain means
:: GLIBPRE0:def 2
for x being Element of dom GF holds GF.x is plain;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is plain means
:: GLIBPRE0:def 3
for n being Nat holds GSq.n is plain;
end;
registration
cluster empty -> plain for Graph-yielding Function;
end;
registration
cluster plain for GraphSeq;
cluster non empty plain for Graph-yielding FinSequence;
end;
registration
let GF be plain non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> plain;
end;
registration
let GSq be plain GraphSeq, x be Nat;
cluster GSq.x -> plain;
end;
registration
let p be plain Graph-yielding FinSequence, n be Nat;
cluster p | n -> plain;
cluster p /^ n -> plain;
let m be Nat;
cluster smid(p,m,n) -> plain;
cluster (m,n)-cut p -> plain;
end;
registration
let p, q be plain Graph-yielding FinSequence;
cluster p ^ q -> plain;
cluster p ^' q -> plain;
end;
registration
let G1, G2 be plain _Graph;
cluster <* G1, G2 *> -> plain;
let G3 be plain _Graph;
cluster <* G1, G2, G3 *> -> plain;
end;
begin :: into GLIB_010
theorem :: GLIBPRE0:77
for G1, G2 being _Graph st G1 == G2
ex F being PGraphMapping of G1, G2 st F = id G1 & F is Disomorphism;
theorem :: GLIBPRE0:78
for G1, G2 being _Graph st G1 == G2 holds G2 is G1-Disomorphic;
theorem :: GLIBPRE0:79
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
ex F being PGraphMapping of G1, G2 st F = id G1 & F is isomorphism;
theorem :: GLIBPRE0:80
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G2 is G1-isomorphic;
:: correction of GLIB_010:90
theorem :: GLIBPRE0:81
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Dcontinuous isomorphism holds
(G1 is non-Dmulti iff G2 is non-Dmulti) &
(G1 is Dsimple iff G2 is Dsimple);
theorem :: GLIBPRE0:82
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st v in dom F_V
holds F_E.:(v.edgesInOut()) c= (F_V/.v).edgesInOut();
theorem :: GLIBPRE0:83
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is directed & v in dom F_V holds
F_E.:(v.edgesIn()) c= (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) c= (F_V/.v).edgesOut();
theorem :: GLIBPRE0:84
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-continuous & v in dom F_V
holds F_E.:(v.edgesInOut()) = (F_V/.v).edgesInOut();
theorem :: GLIBPRE0:85
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V holds
F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) = (F_V/.v).edgesOut();
theorem :: GLIBPRE0:86
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is isomorphism
holds F_E.:(v.edgesInOut()) = (F_V/.v).edgesInOut();
theorem :: GLIBPRE0:87
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is Disomorphism holds
F_E.:(v.edgesIn()) = (F_V/.v).edgesIn() &
F_E.:(v.edgesOut()) = (F_V/.v).edgesOut();
registration
let G1 be _Graph, G2 be edgeless _Graph;
cluster -> directed for PGraphMapping of G1, G2;
end;
theorem :: GLIBPRE0:88
for G1, G2 being _Graph, F0 being PGraphMapping of G1, G2
st F0_E is one-to-one
ex E being Subset of the_Edges_of G2 st
for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is non empty implies F is non empty) &
(F0 is total implies F is total) &
(F0 is one-to-one implies F is one-to-one) &
(F0 is onto implies F is onto) &
(F0 is semi-continuous implies F is semi-continuous) &
(F0 is continuous implies F is continuous);
theorem :: GLIBPRE0:89
for G1, G2 being _Graph, F0 being PGraphMapping of G1, G2
st F0_E is one-to-one
ex E being Subset of the_Edges_of G2 st
for G3 being reverseEdgeDirections of G2, E
ex F being PGraphMapping of G1, G3 st F = F0 & F is directed &
(F0 is weak_SG-embedding implies F is weak_SG-embedding) &
(F0 is strong_SG-embedding implies F is strong_SG-embedding) &
(F0 is isomorphism implies F is isomorphism);
theorem :: GLIBPRE0:90
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is directed weak_SG-embedding holds
v.inDegree() c= (F_V/.v).inDegree() &
v.outDegree() c= (F_V/.v).outDegree();
theorem :: GLIBPRE0:91
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is weak_SG-embedding
holds v.degree() c= (F_V/.v).degree();
theorem :: GLIBPRE0:92
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V holds
(F_V/.v).inDegree() c= v.inDegree() &
(F_V/.v).outDegree() c= v.outDegree();
:: Can this theorem and all using it be improved to semi-continuous?
theorem :: GLIBPRE0:93
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is onto semi-Dcontinuous & v in dom F_V
holds (F_V/.v).degree() c= v.degree();
theorem :: GLIBPRE0:94
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is Disomorphism holds
v.inDegree() = (F_V/.v).inDegree() & v.outDegree() = (F_V/.v).outDegree();
theorem :: GLIBPRE0:95
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
for v being Vertex of G1 st F is isomorphism
holds v.degree() = (F_V/.v).degree();
begin :: into CHORD
theorem :: GLIBPRE0:96
for G being _Graph, u,v,w being Vertex of G st v is endvertex & u <> w
holds not u,v are_adjacent or not v,w are_adjacent;
theorem :: GLIBPRE0:97
for G being _Graph, v being Vertex of G st 3 c= G.order() & v is endvertex
ex u,w being Vertex of G
st u <> v & w <> v & u <> w & u,v are_adjacent & not v,w are_adjacent;
theorem :: GLIBPRE0:98
for G being _Graph, v being Vertex of G st 4 c= G.order() & v is endvertex
ex x,y,z being Vertex of G
st v <> x & v <> y & v <> z & x <> y & x <> z & y <> z & v,x are_adjacent &
not v,y are_adjacent & not v,z are_adjacent;
definition
let GF be Graph-yielding Function;
attr GF is chordal means
:: GLIBPRE0:def 4
for x being object st x in dom GF
ex G being _Graph st GF.x = G & G is chordal;
end;
registration
let G be chordal _Graph;
cluster <* G *> -> chordal;
cluster NAT --> G -> chordal;
end;
definition
let GF be non empty Graph-yielding Function;
redefine attr GF is chordal means
:: GLIBPRE0:def 5
for x being Element of dom GF holds GF.x is chordal;
end;
definition
let GSq be GraphSeq;
redefine attr GSq is chordal means
:: GLIBPRE0:def 6
for n being Nat holds GSq.n is chordal;
end;
registration
cluster empty -> chordal for Graph-yielding Function;
end;
registration
cluster chordal for GraphSeq;
cluster non empty chordal for Graph-yielding FinSequence;
end;
registration
let GF be chordal non empty Graph-yielding Function, x be Element of dom GF;
cluster GF.x -> chordal;
end;
registration
let GSq be chordal GraphSeq, x be Nat;
cluster GSq.x -> chordal;
end;
registration
let p be chordal Graph-yielding FinSequence, n be Nat;
cluster p | n -> chordal;
cluster p /^ n -> chordal;
let m be Nat;
cluster smid(p,m,n) -> chordal;
cluster (m,n)-cut p -> chordal;
end;
registration
let p, q be chordal Graph-yielding FinSequence;
cluster p ^ q -> chordal;
cluster p ^' q -> chordal;
end;
registration
let G1, G2 be chordal _Graph;
cluster <* G1, G2 *> -> chordal;
let G3 be chordal _Graph;
cluster <* G1, G2, G3 *> -> chordal;
end;
begin :: into GLIB_011
theorem :: GLIBPRE0:99
for G1, G2 being non-Dmulti _Graph, f being directed PVertexMapping of G1, G2
for v being Vertex of G1 st f is Disomorphism holds
v.inDegree() = (f/.v).inDegree() & v.outDegree() = (f/.v).outDegree();
theorem :: GLIBPRE0:100
for G1, G2 being non-multi _Graph, f being PVertexMapping of G1, G2
for v being Vertex of G1 st f is isomorphism
holds v.degree() = (f/.v).degree();