:: Refined Finiteness and Degree properties in Graphs
:: by Sebastian Koch
::
:: Received May 19, 2020
:: Copyright (c) 2020-2026 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 SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ARYTM_3, CARD_1,
XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1,
FUNCOP_1, FUNCT_2, GLIB_009, MOD_4, WAYBEL_0, GLIB_006, GLIB_007,
FUNCT_4, CARD_2, SCMYCIEL, SGRAPH1, GLIB_010, SIMPLEX0, XCMPLX_0,
MATRIX11, BSPACE, GLIB_013, SQUARE_1, SETFAM_1, RELAT_2, STRUCT_0,
ORDINAL1, GLIB_012, YELLOW_1, WELLORD2, FUNCT_7, PBOOLE, CHORD,
GLIB_001, GLIB_002, REWRITE1, RCOMP_1, FINSEQ_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, WELLORD2, FUNCT_2, DOMAIN_1, FUNCOP_1,
FUNCT_4, FINSET_1, CARD_1, FINSEQ_1, XCMPLX_0, XXREAL_0, SQUARE_1,
CARD_2, NEWTON, GLIB_000, STRUCT_0, ORDERS_2, SGRAPH1, MATRIX11,
YELLOW_1, ORDERS_5, BSPACE, GLIB_001, GLIB_002, GLIB_006, GLIB_007,
GLIB_008, GLIB_009, GLIB_010, GLIB_012, CHORD;
constructors DOMAIN_1, FUNCT_4, CARD_2, GLIB_002, GLIB_007, BSPACE, MATRIX11,
GLIB_008, GLIB_009, GLIB_010, SQUARE_1, NEWTON, YELLOW_1, ORDERS_5,
GLIB_012, CHORD, GLIB_001;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
GLIB_000, CARD_1, XTUPLE_0, GLIB_008, GLIB_010, SQUARE_1, CARD_2,
RAMSEY_1, MSAFREE5, SGRAPH1, CARD_5, GLIBPRE0, YELLOW_1, ORDINAL7,
CHORD, GLIB_001, FINSEQ_1;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
equalities ORDINAL1, GLIB_000, GLIB_010, BSPACE, SGRAPH1, STRUCT_0, YELLOW_1,
CHORD;
definitions GLIB_002;
theorems TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XBOOLE_1, CARD_1, CARD_2,
RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, XREAL_1, XXREAL_0, GLIB_000,
GLIB_006, GLIB_007, WELLORD2, XTUPLE_0, ORDINAL1, CHORD, GLIB_009,
GLIB_010, FINSET_1, SQUARE_1, SETFAM_1, BSPACE, NAT_1, GLIB_012,
TOPGEN_2, SUBSET_1, NUMPOLY1, GLIBPRE0, ORDERS_5, ORDERS_2, FIELD_5,
GLIB_001, GLIB_002, SCMYCIEL, XREAL_0;
schemes FUNCT_1, NAT_1, FRAENKEL;
begin :: Upper Size of Graphs without parallel Edges
theorem Th1:
for G being non-Dmulti _Graph ex f being one-to-one Function
st dom f = the_Edges_of G &
rng f c= [: the_Vertices_of G, the_Vertices_of G :] &
for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e]
proof
let G be non-Dmulti _Graph;
deffunc F(object) = [(the_Source_of G).$1,(the_Target_of G).$1];
consider f being Function such that
A1: dom f = the_Edges_of G and
A2: for e being object st e in the_Edges_of G holds f.e = F(e)
from FUNCT_1:sch 3;
now
let x1,x2 be object;
assume A3: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then f.x1 = [(the_Source_of G).x1,(the_Target_of G).x1] &
f.x2 = [(the_Source_of G).x2,(the_Target_of G).x2] by A1, A2;
then A4: (the_Source_of G).x1 = (the_Source_of G).x2 &
(the_Target_of G).x1 = (the_Target_of G).x2 by A3, XTUPLE_0:1;
x1 DJoins (the_Source_of G).x1,(the_Target_of G).x1,G &
x2 DJoins (the_Source_of G).x2,(the_Target_of G).x2,G
by A1, A3, GLIB_000:def 14;
hence x1 = x2 by A4, GLIB_000:def 21;
end;
then reconsider f as one-to-one Function by FUNCT_1:def 4;
take f;
thus dom f = the_Edges_of G by A1;
now
let y be object;
assume y in rng f;
then consider x being object such that
A5: x in dom f & f.x = y by FUNCT_1:def 3;
A6: y = [(the_Source_of G).x,(the_Target_of G).x] by A1, A2, A5;
x Joins (the_Source_of G).x,(the_Target_of G).x,G
by A1, A5, GLIB_000:def 13;
then (the_Source_of G).x is Vertex of G &
(the_Target_of G).x is Vertex of G by GLIB_000:13;
hence y in [: the_Vertices_of G,the_Vertices_of G :] by A6, ZFMISC_1:def 2;
end;
hence rng f c= [: the_Vertices_of G, the_Vertices_of G :] by TARSKI:def 3;
thus thesis by A1, A2;
end;
theorem Th2:
for G being non-Dmulti _Graph holds G.size() c= G.order() *` G.order()
proof
let G be non-Dmulti _Graph;
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G &
rng f c= [: the_Vertices_of G, the_Vertices_of G :] and
for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e] by Th1;
G.size() c= card [: the_Vertices_of G, the_Vertices_of G :]
by A1, CARD_1:10;
then G.size() c= card [: G.order(), card the_Vertices_of G :] by CARD_2:7;
hence thesis by CARD_2:def 2;
end;
theorem Th3:
for G being Dsimple _Graph ex f being one-to-one Function
st dom f = the_Edges_of G &
rng f c= [: the_Vertices_of G, the_Vertices_of G :]\id the_Vertices_of G &
for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e]
proof
let G be Dsimple _Graph;
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G &
rng f c= [: the_Vertices_of G, the_Vertices_of G :] and
A2: for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e] by Th1;
take f;
rng f misses id the_Vertices_of G
proof
assume rng f meets id the_Vertices_of G;
then consider y being object such that
A3: y in rng f & y in id the_Vertices_of G by XBOOLE_0:3;
consider x being object such that
A4: x in dom f & f.x = y by A3, FUNCT_1:def 3;
y = [(the_Source_of G).x,(the_Target_of G).x] by A2, A4;
then (the_Source_of G).x = (the_Target_of G).x by A3, RELAT_1:def 10;
hence contradiction by A1, A4, GLIB_000:def 18;
end;
hence thesis by A1, A2, XBOOLE_1:86;
end;
theorem Th4:
for G being non-multi _Graph ex f being one-to-one Function
st dom f = the_Edges_of G &
rng f c= 2Set the_Vertices_of G \/ singletons the_Vertices_of G &
for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e}
proof
let G be non-multi _Graph;
deffunc F(object) = {(the_Source_of G).$1,(the_Target_of G).$1};
consider f being Function such that
A1: dom f = the_Edges_of G and
A2: for e being object st e in the_Edges_of G holds f.e = F(e)
from FUNCT_1:sch 3;
now
let x1,x2 be object;
assume A3: x1 in dom f & x2 in dom f & f.x1 = f.x2;
then A4: f.x1 = {(the_Source_of G).x1,(the_Target_of G).x1} &
f.x2 = {(the_Source_of G).x2,(the_Target_of G).x2} by A1, A2;
A5: x1 Joins (the_Source_of G).x1,(the_Target_of G).x1,G &
x2 Joins (the_Source_of G).x2,(the_Target_of G).x2,G
by A1, A3, GLIB_000:def 13;
per cases by A3, A4, ZFMISC_1:22;
suppose (the_Source_of G).x1 = (the_Source_of G).x2 &
(the_Target_of G).x1 = (the_Target_of G).x2;
hence x1 = x2 by A5, GLIB_000:def 20;
end;
suppose (the_Source_of G).x1 = (the_Target_of G).x2 &
(the_Target_of G).x1 = (the_Source_of G).x2;
then x2 Joins (the_Source_of G).x1,(the_Target_of G).x1,G
by A5, GLIB_000:14;
hence x1 = x2 by A5, GLIB_000:def 20;
end;
end;
then reconsider f as one-to-one Function by FUNCT_1:def 4;
take f;
thus dom f = the_Edges_of G by A1;
for y being object st y in rng f holds y in
2Set the_Vertices_of G \/ singletons the_Vertices_of G
proof
let y be object;
assume y in rng f;
then consider x being object such that
A6: x in dom f & f.x = y by FUNCT_1:def 3;
reconsider z = y as set by TARSKI:1;
A7: y = {(the_Source_of G).x,(the_Target_of G).x} by A1, A2, A6;
x Joins (the_Source_of G).x,(the_Target_of G).x,G
by A1, A6, GLIB_000:def 13;
then A8: (the_Source_of G).x is Vertex of G &
(the_Target_of G).x is Vertex of G by GLIB_000:13;
per cases;
suppose (the_Source_of G).x = (the_Target_of G).x;
then y = {(the_Source_of G).x} by A7, ENUMSET1:29;
then z c= the_Vertices_of G & z is 1-element by A8, ZFMISC_1:31;
then z in singletons the_Vertices_of G;
hence thesis by XBOOLE_0:def 3;
end;
suppose (the_Source_of G).x <> (the_Target_of G).x;
then z c= the_Vertices_of G & card z = 2
by A7, A8, ZFMISC_1:32, CARD_2:57;
then z in TWOELEMENTSETS the_Vertices_of G;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence rng f c= 2Set the_Vertices_of G \/ singletons the_Vertices_of G
by TARSKI:def 3;
thus thesis by A1, A2;
end;
theorem Th5:
for G being simple _Graph ex f being one-to-one Function
st dom f = the_Edges_of G & rng f c= 2Set the_Vertices_of G &
for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e}
proof
let G be simple _Graph;
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G and
A2: rng f c= 2Set the_Vertices_of G \/ singletons the_Vertices_of G and
A3: for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e} by Th4;
take f;
rng f /\ singletons the_Vertices_of G = {}
proof
assume rng f /\ singletons the_Vertices_of G <> {};
then consider y being object such that
A4: y in rng f /\ singletons the_Vertices_of G by XBOOLE_0:def 1;
A5: y in rng f & y in singletons the_Vertices_of G by A4, XBOOLE_0:def 4;
then consider e being object such that
A6: e in dom f & f.e = y by FUNCT_1:def 3;
consider Y being Subset of the_Vertices_of G such that
A7: y = Y & Y is 1-element by A5;
card Y = 1 by A7, CARD_1:def 7
.= card {the object} by CARD_1:30;
then consider v being object such that
A8: Y = {v} by CARD_1:29;
y = {(the_Source_of G).e,(the_Target_of G).e} by A3, A6;
hence contradiction by A1, A6, A7, A8, ZFMISC_1:5, GLIB_000:def 18;
end;
hence thesis by A1, A2, A3, XBOOLE_1:73, XBOOLE_0:def 7;
end;
begin :: vertex- and edge-finite graph
definition
let G be _Graph;
attr G is vertex-finite means
:Def1:
the_Vertices_of G is finite;
attr G is edge-finite means
:Def2:
the_Edges_of G is finite;
end;
theorem Th6:
for G being _Graph holds G is vertex-finite iff G.order() is finite;
theorem Th7:
for G being _Graph holds G is edge-finite iff G.size() is finite;
theorem Th8:
for G1, G2 being _Graph st G1 == G2 holds
(G1 is vertex-finite implies G2 is vertex-finite) &
(G1 is edge-finite implies G2 is edge-finite) by GLIB_000:def 34;
registration
let V be non empty finite set, E be set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> vertex-finite;
coherence;
end;
registration
let V be infinite set, E be set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> non vertex-finite;
coherence;
end;
registration
let V be non empty set, E be finite set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> edge-finite;
coherence;
end;
registration
let V be non empty set, E be infinite set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> non edge-finite;
coherence;
end;
registration
cluster _finite -> vertex-finite edge-finite for _Graph;
coherence;
cluster vertex-finite edge-finite -> _finite for _Graph;
coherence by GLIB_000:def 17;
cluster edgeless -> edge-finite for _Graph;
coherence;
cluster _trivial -> vertex-finite for _Graph;
coherence;
cluster vertex-finite non-Dmulti -> edge-finite for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is vertex-finite non-Dmulti;
then A2: G.size() c= G.order() *` G.order() by Th2;
reconsider X = G.order() as finite set by A1;
G.order() *` G.order() = card [: G.order(), G.order() :] by CARD_2:def 2
.= card X * card X by CARD_2:46;
hence thesis by A2;
end;
cluster non vertex-finite loopfull -> non edge-finite for _Graph;
coherence
proof
let G be _Graph;
assume A3: G is non vertex-finite loopfull;
G.loops() is infinite
proof
assume A4: G.loops() is finite;
set f = (the_Source_of G)|G.loops();
now
let v be object;
assume v in the_Vertices_of G;
then consider e being object such that
A5: e Joins v,v,G by A3, GLIB_012:def 1;
A6: e in G.loops() by A5, GLIB_009:def 2;
A7: v = (the_Source_of G).e by A5, GLIB_000:def 13
.= f.e by A6, FUNCT_1:49;
e in the_Edges_of G by A5, GLIB_000:def 13;
then e in dom the_Source_of G by FUNCT_2:def 1;
then e in dom f by A6, RELAT_1:57;
hence v in rng f by A7, FUNCT_1:def 3;
end;
then the_Vertices_of G c= rng f by TARSKI:def 3;
hence contradiction by A3, A4;
end;
hence thesis;
end;
::cluster non vertex-finite without_isolated_vertices -> non edge-finite
::for _Graph;
::coherence; :: f(v) = the Element of v.edgesInOut has infinite range
::cluster edge-finite without_isolated_vertices ->
::vertex-finite for _Graph;
::coherence;
cluster vertex-finite edge-finite simple for _Graph;
existence
proof
take the _finite simple _Graph;
thus thesis;
end;
cluster vertex-finite non edge-finite for _Graph;
existence
proof
set x = the object;
set E = the infinite set;
set f = the Function of E,{x};
set G = createGraph({x},E,f,f);
take G;
thus thesis;
end;
cluster non vertex-finite edge-finite for _Graph;
existence
proof
set V = the infinite set;
set E = the empty set;
set f = the Function of E,V;
set G = createGraph(V,E,f,f);
take G;
thus thesis;
end;
cluster non vertex-finite non edge-finite for _Graph;
existence
proof
set V = the infinite set;
set f = the Function of V,V;
set G = createGraph(V,V,f,f);
take G;
thus thesis;
end;
end;
registration
let G be vertex-finite _Graph;
cluster G.order() -> non zero natural;
coherence
proof
G.order() is finite by Th6;
hence thesis;
end;
end;
definition
let G be vertex-finite _Graph;
redefine func G.order() -> non zero Nat; :: redefines .order() (GLIB_000, definition)
coherence;
end;
registration
let G be edge-finite _Graph;
cluster G.size() -> natural;
coherence
proof
G.size() is finite by Th7;
hence thesis;
end;
end;
definition
let G be edge-finite _Graph;
redefine func G.size() -> Nat; :: redefines .size() (GLIB_000, definition)
coherence;
end;
theorem
for G being vertex-finite non-Dmulti _Graph
holds G.size() <= G.order()^2
proof
let G be vertex-finite non-Dmulti _Graph;
G.order() *` G.order() = card [: G.order(), G.order() :] by CARD_2:def 2
.= card G.order() * G.order() by CARD_2:46
.= Segm(G.order() * G.order());
then Segm(G.size()) c= Segm(G.order() * G.order()) by Th2;
then G.size() <= G.order() * G.order() by NAT_1:39;
hence thesis by SQUARE_1:def 1;
end;
theorem
for G being vertex-finite Dsimple _Graph
holds G.size() <= G.order()^2 - G.order()
proof
let G be vertex-finite Dsimple _Graph;
set P = [: the_Vertices_of G, the_Vertices_of G :];
set I = id the_Vertices_of G;
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G & rng f c= P \ I and
for e being object st e in dom f holds
f.e = [(the_Source_of G).e,(the_Target_of G).e] by Th3;
A2: G.order()-1 is Nat by CHORD:1;
G.order()^2 - G.order() = G.order() * G.order() - G.order() by SQUARE_1:def 1
.= G.order()*(G.order()-1);
then A3: G.order()^2 - G.order() is Nat by A2;
card(P\I) = card P - card I by CARD_2:44
.= G.order() * card the_Vertices_of G - card I by CARD_2:46
.= G.order()^2 - card I by SQUARE_1:def 1
.= G.order()^2 - card dom id the_Vertices_of G by CARD_1:62
.= G.order()^2 - G.order();
then Segm(G.size()) c= Segm(G.order()^2 - G.order()) by A1, CARD_1:10;
hence G.size() <= G.order()^2 - G.order() by A3, NAT_1:39;
end;
theorem
for G being vertex-finite non-multi _Graph
holds G.size() <= (G.order()^2 + G.order())/2
proof
let G be vertex-finite non-multi _Graph;
set V1 = singletons the_Vertices_of G, V2 = 2Set the_Vertices_of G;
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G & rng f c= V2 \/ V1 and
for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e} by Th4;
reconsider n = G.order() - 1 as Nat by CHORD:1;
A2: card (V2 \/ V1) = card V2 +` card V1 by CARD_2:35, GLIBPRE0:18
.= card V2 +` card the_Vertices_of G by BSPACE:41
.= ((n+1) choose 2) + (n+1) by GLIBPRE0:20;
A3: ((n+1) choose 2) + (n+1) = n*(n+1)/2 + 2*(n+1)/2 by NUMPOLY1:72
.= (G.order()*G.order() + G.order())/2
.= (G.order()^2 + G.order())/2 by SQUARE_1:def 1;
card rng f c= ((n+1) choose 2) + (n+1) by A1, A2, CARD_1:11;
then Segm(G.size()) c= Segm(((n+1) choose 2) + (n+1)) by A1, CARD_1:70;
hence thesis by A3, NAT_1:39;
end;
theorem
for G being vertex-finite simple _Graph
holds G.size() <= (G.order()^2 - G.order())/2
proof
let G be vertex-finite simple _Graph;
consider f being one-to-one Function such that
A1: dom f = the_Edges_of G & rng f c= 2Set the_Vertices_of G and
for e being object st e in dom f holds
f.e = {(the_Source_of G).e,(the_Target_of G).e} by Th5;
reconsider n = G.order() - 1 as Nat by CHORD:1;
A2: card 2Set the_Vertices_of G
= (card the_Vertices_of G) choose 2 by GLIBPRE0:20
.= n * (n+1) / 2 by NUMPOLY1:72
.= (G.order()*G.order() - G.order())/2
.= (G.order()^2 - G.order())/2 by SQUARE_1:def 1;
card rng f c= card 2Set the_Vertices_of G by A1, CARD_1:11;
then Segm G.size() c= Segm card 2Set the_Vertices_of G by A1, CARD_1:70;
hence thesis by A2, NAT_1:39;
end;
registration
let G be vertex-finite _Graph;
cluster the_Vertices_of G -> finite;
coherence by Def1;
cluster -> vertex-finite for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
the_Vertices_of G2 c= the_Vertices_of G;
hence thesis;
end;
cluster -> vertex-finite edge-finite for DLGraphComplement of G;
coherence
proof
let H be DLGraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:def 6;
hence H is vertex-finite;
hence thesis;
end;
cluster -> vertex-finite edge-finite for LGraphComplement of G;
coherence
proof
let H be LGraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:def 7;
hence H is vertex-finite;
hence thesis;
end;
cluster -> vertex-finite edge-finite for DGraphComplement of G;
coherence
proof
let H be DGraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:80;
hence H is vertex-finite;
hence thesis;
end;
cluster -> vertex-finite edge-finite for GraphComplement of G;
coherence
proof
let H be GraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:98;
hence H is vertex-finite;
hence thesis;
end;
let V be finite set;
cluster -> vertex-finite for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
the_Vertices_of G1 = the_Vertices_of G \/ V by GLIB_006:def 10;
hence thesis;
end;
end;
registration
let G be vertex-finite _Graph, v be object;
cluster -> vertex-finite for addVertex of G, v;
coherence;
let e,w be object;
cluster -> vertex-finite for addEdge of G,v,e,w;
coherence
proof
let G1 be addEdge of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G;
hence thesis by GLIB_006:def 11;
end;
suppose not (v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G);
then G == G1 by GLIB_006:def 11;
hence thesis by Th8;
end;
end;
cluster -> vertex-finite for addAdjVertex of G,v,e,w;
coherence
proof
let G1 be addAdjVertex of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {w} by GLIB_006:def 12;
hence thesis;
end;
suppose not v in the_Vertices_of G & not e in the_Edges_of G &
w in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v} by GLIB_006:def 12;
hence thesis;
end;
suppose not(v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G) & not(not v in the_Vertices_of G &
not e in the_Edges_of G & w in the_Vertices_of G);
then G == G1 by GLIB_006:def 12;
hence thesis by Th8;
end;
end;
end;
registration
let G be vertex-finite _Graph, E be set;
cluster -> vertex-finite for reverseEdgeDirections of G, E;
coherence
proof
let G2 be reverseEdgeDirections of G, E;
the_Vertices_of G = the_Vertices_of G2 by GLIB_007:4;
hence thesis;
end;
end;
registration
let G be vertex-finite _Graph, v be object, V be set;
cluster -> vertex-finite for addAdjVertexAll of G,v,V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then the_Vertices_of G1 = the_Vertices_of G \/ {v} by GLIB_007:def 4;
hence thesis;
end;
suppose not(V c= the_Vertices_of G & not v in the_Vertices_of G);
then G == G1 by GLIB_007:def 4;
hence thesis by Th8;
end;
end;
end;
registration
let G be vertex-finite _Graph, V be set;
cluster -> vertex-finite for addLoops of G, V;
coherence
proof
let G1 be addLoops of G, V;
the_Vertices_of G1 = the_Vertices_of G by GLIB_012:15;
hence thesis;
end;
end;
registration
let G be _Graph;
let V be infinite set;
cluster -> non vertex-finite for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
the_Vertices_of G1 = the_Vertices_of G \/ V by GLIB_006:def 10;
hence thesis;
end;
end;
registration
let G be non vertex-finite _Graph;
cluster the_Vertices_of G -> infinite;
coherence by Def1;
cluster -> non vertex-finite for Supergraph of G;
coherence
proof
let G1 be Supergraph of G;
G is Subgraph of G1 by GLIB_006:57;
hence thesis;
end;
cluster spanning -> non vertex-finite for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
assume G2 is spanning;
then the_Vertices_of G2 = the_Vertices_of G by GLIB_000:def 33;
hence thesis;
end;
cluster -> non vertex-finite for DLGraphComplement of G;
coherence
proof
let H be DLGraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:def 6;
hence thesis;
end;
cluster -> non vertex-finite for LGraphComplement of G;
coherence
proof
let H be LGraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:def 7;
hence thesis;
end;
cluster -> non vertex-finite for DGraphComplement of G;
coherence
proof
let H be DGraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:80;
hence thesis;
end;
cluster -> non vertex-finite for GraphComplement of G;
coherence
proof
let H be GraphComplement of G;
the_Vertices_of H = the_Vertices_of G by GLIB_012:98;
hence thesis;
end;
let V be infinite set, E be set;
cluster -> non vertex-finite for inducedSubgraph of G, V, E;
coherence
proof
let G2 be inducedSubgraph of G,V,E;
per cases;
suppose V is non empty Subset of the_Vertices_of G &
E c= G.edgesBetween(V);
hence thesis by GLIB_000:def 37;
end;
suppose not(V is non empty Subset of the_Vertices_of G &
E c= G.edgesBetween(V));
then G == G2 by GLIB_000:def 37;
hence thesis by Th8;
end;
end;
end;
registration
let G be non vertex-finite _Graph, V be infinite Subset of the_Vertices_of G;
cluster -> non edge-finite for addLoops of G, V;
coherence
proof
let G1 be addLoops of G, V;
consider E being set, f being one-to-one Function such that
A1: E misses the_Edges_of G & the_Edges_of G1 = the_Edges_of G \/ E and
A2: dom f = E & rng f = V and
the_Source_of G1 = the_Source_of G +* f &
the_Target_of G1 = the_Target_of G +* f by GLIB_012:def 5;
E is infinite by A2, FINSET_1:8;
hence thesis by A1;
end;
end;
registration
let G be edge-finite _Graph;
cluster the_Edges_of G -> finite;
coherence by Def2;
cluster -> edge-finite for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
the_Edges_of G2 c= the_Edges_of G;
hence thesis;
end;
let V be set;
cluster -> edge-finite for addVertices of G, V;
coherence
proof
let G1 be addVertices of G,V;
the_Edges_of G1 = the_Edges_of G by GLIB_006:def 10;
hence thesis;
end;
end;
registration
let G be edge-finite _Graph, E be set;
cluster -> edge-finite for reverseEdgeDirections of G, E;
coherence
proof
let G2 be reverseEdgeDirections of G,E;
the_Edges_of G2 = the_Edges_of G by GLIB_007:4;
hence thesis;
end;
end;
registration
let G be edge-finite _Graph, v be object;
cluster -> edge-finite for addVertex of G, v;
coherence;
let e,w be object;
cluster -> edge-finite for addEdge of G,v,e,w;
coherence
proof
let G1 be addEdge of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G;
then the_Edges_of G1 = the_Edges_of G \/ {e} by GLIB_006:def 11;
hence thesis;
end;
suppose not (v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G);
then G == G1 by GLIB_006:def 11;
hence thesis by Th8;
end;
end;
cluster -> edge-finite for addAdjVertex of G,v,e,w;
coherence
proof
let G1 be addAdjVertex of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G;
then the_Edges_of G1 = the_Edges_of G \/ {e} by GLIB_006:def 12;
hence thesis;
end;
suppose not v in the_Vertices_of G & not e in the_Edges_of G &
w in the_Vertices_of G;
then the_Edges_of G1 = the_Edges_of G \/ {e} by GLIB_006:def 12;
hence thesis;
end;
suppose not(v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G) & not(not v in the_Vertices_of G &
not e in the_Edges_of G & w in the_Vertices_of G);
then G == G1 by GLIB_006:def 12;
hence thesis by Th8;
end;
end;
end;
registration
let G be edge-finite _Graph, v be object, V be finite set;
cluster -> edge-finite for addAdjVertexAll of G, v, V;
coherence
proof
let G1 be addAdjVertexAll of G, v, V;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
then consider E being set such that
A1: card V = card E & E misses the_Edges_of G and
A2: the_Edges_of G1 = the_Edges_of G \/ E and
for v1 being object st v1 in V ex e1 being object st e1 in E &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by GLIB_007:def 4;
E is finite by A1;
hence thesis by A2;
end;
suppose not(V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by GLIB_007:def 4;
hence thesis by Th8;
end;
end;
end;
registration
let G be edge-finite _Graph, V be finite Subset of the_Vertices_of G;
cluster -> edge-finite for addLoops of G, V;
coherence
proof
let G1 be addLoops of G, V;
consider E being set, f being one-to-one Function such that
A1: E misses the_Edges_of G & the_Edges_of G1 = the_Edges_of G \/ E and
A2: dom f = E & rng f = V and
the_Source_of G1 = the_Source_of G +* f &
the_Target_of G1 = the_Target_of G +* f by GLIB_012:def 5;
card E = card V by A2, CARD_1:70;
then E is finite;
hence thesis by A1;
end;
end;
registration
let G be non vertex-finite edge-finite _Graph;
cluster isolated for Vertex of G;
existence
proof
set R = rng the_Source_of G \/ rng the_Target_of G;
set v = the Element of the_Vertices_of G \ R;
reconsider v as Vertex of G;
take v;
not v in R by XBOOLE_0:def 5;
hence v is isolated by GLIB_000:145;
end;
end;
registration
let G be non vertex-finite edge-finite _Graph;
cluster -> non edge-finite for DLGraphComplement of G;
coherence
proof
let H be DLGraphComplement of G;
set v = the isolated Vertex of G;
reconsider w = v as Vertex of H by GLIB_012:def 6;
the_Vertices_of H = w.inNeighbors() by GLIB_012:61
.= (the_Source_of H).:w.edgesIn();
hence thesis;
end;
cluster -> non edge-finite for LGraphComplement of G;
coherence
proof
let H be LGraphComplement of G;
set v = the isolated Vertex of G;
reconsider w = v as Vertex of H by GLIB_012:def 7;
the_Vertices_of H = w.allNeighbors() by GLIB_012:78
.= w.inNeighbors() \/ w.outNeighbors();
hence thesis;
end;
cluster -> non edge-finite for DGraphComplement of G;
coherence
proof
let H be DGraphComplement of G;
set v = the isolated Vertex of G;
reconsider w = v as Vertex of H by GLIB_012:80;
the_Vertices_of H \ {w} = w.inNeighbors() by GLIB_012:96
.= (the_Source_of H).:w.edgesIn();
hence thesis;
end;
cluster -> non edge-finite for GraphComplement of G;
coherence
proof
let H be GraphComplement of G;
set v = the isolated Vertex of G;
reconsider w = v as Vertex of H by GLIB_012:98;
the_Vertices_of H \ {w} = w.allNeighbors() by GLIB_012:119
.= w.inNeighbors() \/ w.outNeighbors();
hence thesis;
end;
end;
registration
let G be non edge-finite _Graph;
cluster the_Edges_of G -> infinite;
coherence by Def2;
cluster -> non edge-finite for Supergraph of G;
coherence
proof
let G1 be Supergraph of G;
G is Subgraph of G1 by GLIB_006:57;
hence thesis;
end;
let V be set, E be infinite Subset of the_Edges_of G;
cluster -> non edge-finite for inducedSubgraph of G, V, E;
coherence
proof
let G2 be inducedSubgraph of G,V,E;
per cases;
suppose V is non empty Subset of the_Vertices_of G &
E c= G.edgesBetween(V);
hence thesis by GLIB_000:def 37;
end;
suppose not(V is non empty Subset of the_Vertices_of G &
E c= G.edgesBetween(V));
then G == G2 by GLIB_000:def 37;
hence thesis by Th8;
end;
end;
end;
registration
let G be non edge-finite _Graph, E be finite set;
cluster -> non edge-finite for removeEdges of G, E;
coherence;
end;
registration
let G be non edge-finite _Graph, e be set;
cluster -> non edge-finite for removeEdge of G, e;
coherence;
end;
theorem Th13:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding holds
(G2 is vertex-finite implies G1 is vertex-finite) &
(G2 is edge-finite implies G1 is edge-finite)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding;
hereby
assume A2: G2 is vertex-finite;
dom F_V = the_Vertices_of G1 & F_V is one-to-one by A1, GLIB_010:def 11;
then the_Vertices_of G1, F_V.:the_Vertices_of G1 are_equipotent
by CARD_1:33;
hence G1 is vertex-finite by A2, CARD_1:38;
end;
assume A3: G2 is edge-finite;
dom F_E = the_Edges_of G1 & F_E is one-to-one by A1, GLIB_010:def 11;
then the_Edges_of G1, F_E.:the_Edges_of G1 are_equipotent
by CARD_1:33;
hence G1 is edge-finite by A3, CARD_1:38;
end;
theorem Th14:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto holds
(G1 is vertex-finite implies G2 is vertex-finite) &
(G1 is edge-finite implies G2 is edge-finite)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto;
hereby
assume A2: G1 is vertex-finite;
dom F_V is finite by A2;
then rng F_V is finite by FINSET_1:8;
hence G2 is vertex-finite by A1, GLIB_010:def 12;
end;
assume G1 is edge-finite;
then dom F_E is finite;
then rng F_E is finite by FINSET_1:8;
hence G2 is edge-finite by A1, GLIB_010:def 12;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds
(G1 is vertex-finite iff G2 is vertex-finite) &
(G1 is edge-finite iff G2 is edge-finite) by Th13, Th14;
begin :: Order and Size of a Graph as attributes
definition
let c be Cardinal, G be _Graph;
attr G is c-vertex means
:Def3:
G.order() = c;
attr G is c-edge means
:Def4:
G.size() = c;
end;
theorem
for G being _Graph
holds G is vertex-finite iff ex n being non zero Nat st G is n-vertex
proof
let G be _Graph;
hereby
assume G is vertex-finite;
then reconsider n = card the_Vertices_of G as Nat;
reconsider n as non zero Nat;
take n;
thus G is n-vertex;
end;
thus thesis;
end;
theorem
for G being _Graph
holds G is edge-finite iff ex n being Nat st G is n-edge
proof
let G be _Graph;
hereby
assume G is edge-finite;
then reconsider n = card the_Edges_of G as Nat;
take n;
thus G is n-edge;
end;
thus thesis;
end;
theorem Th18:
for G1, G2 being _Graph, c being Cardinal
st the_Vertices_of G1 = the_Vertices_of G2
holds G1 is c-vertex implies G2 is c-vertex;
theorem Th19:
for G1, G2 being _Graph, c being Cardinal
st the_Edges_of G1 = the_Edges_of G2
holds G1 is c-edge implies G2 is c-edge;
theorem Th20:
for G1, G2 being _Graph, c being Cardinal st G1 == G2 holds
(G1 is c-vertex implies G2 is c-vertex) &
(G1 is c-edge implies G2 is c-edge) by GLIB_000:def 34;
theorem
for G being _Graph holds G is G.order()-vertex G.size()-edge;
registration
let V be non empty set, E be set;
let S, T be Function of E, V;
cluster createGraph(V,E,S,T) -> (card V)-vertex (card E)-edge;
coherence;
end;
registration
let a be non zero Cardinal, b be Cardinal;
cluster a-vertex b-edge for _Graph;
existence
proof
set V = the a-element set;
set E = the b-element set;
set v = the Element of V;
set f = E --> v;
reconsider f as Function of E, V;
take G = createGraph(V,E,f,f);
card V = a & card E = b by CARD_1:def 7;
hence thesis;
end;
end;
registration
let c be Cardinal;
cluster _trivial c-edge for _Graph;
existence
proof
take G = the 1-vertex c-edge _Graph;
G.order() = 1 by Def3;
hence thesis by GLIB_000:def 19;
end;
end;
registration
cluster -> non 0-vertex for _Graph;
coherence;
cluster _trivial -> 1-vertex for _Graph;
coherence by GLIB_000:def 19;
cluster 1-vertex -> _trivial for _Graph;
coherence by GLIB_000:def 19;
let n be non zero Nat;
cluster n-vertex -> vertex-finite for _Graph;
coherence;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph;
cluster spanning -> c-vertex for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
assume G2 is spanning;
then the_Vertices_of G = the_Vertices_of G2 by GLIB_000:def 33;
hence thesis by Th18;
end;
cluster -> c-vertex for DLGraphComplement of G;
coherence
proof
let H be DLGraphComplement of G;
the_Vertices_of G = the_Vertices_of H by GLIB_012:def 6;
hence thesis by Th18;
end;
cluster -> c-vertex for LGraphComplement of G;
coherence
proof
let H be LGraphComplement of G;
the_Vertices_of G = the_Vertices_of H by GLIB_012:def 7;
hence thesis by Th18;
end;
cluster -> c-vertex for DGraphComplement of G;
coherence
proof
let H be DGraphComplement of G;
the_Vertices_of G = the_Vertices_of H by GLIB_012:80;
hence thesis by Th18;
end;
cluster -> c-vertex for GraphComplement of G;
coherence
proof
let H be GraphComplement of G;
the_Vertices_of G = the_Vertices_of H by GLIB_012:98;
hence thesis by Th18;
end;
let E be set;
cluster -> c-vertex for reverseEdgeDirections of G, E;
coherence
proof
let G2 be reverseEdgeDirections of G, E;
the_Vertices_of G = the_Vertices_of G2 by GLIB_007:4;
hence thesis by Th18;
end;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph, V be set;
cluster -> c-vertex for addLoops of G, V;
coherence
proof
let G1 be addLoops of G, V;
the_Vertices_of G = the_Vertices_of G1 by GLIB_012:15;
hence thesis by Th18;
end;
end;
registration
let c be non zero Cardinal, G be c-vertex _Graph, v,e,w be object;
cluster -> c-vertex for addEdge of G,v,e,w;
coherence
proof
let G1 be addEdge of G,v,e,w;
per cases;
suppose v is Vertex of G & w is Vertex of G;
then the_Vertices_of G = the_Vertices_of G1 by GLIB_006:102;
hence thesis by Th18;
end;
suppose not(v is Vertex of G & w is Vertex of G);
then G1 == G by GLIB_006:def 11;
hence thesis by Th20;
end;
end;
end;
registration
cluster edgeless -> 0-edge for _Graph;
coherence;
cluster 0-edge -> edgeless for _Graph;
coherence;
let n be Nat;
cluster n-edge -> edge-finite for _Graph;
coherence;
end;
registration
let c be Cardinal, G be c-edge _Graph, E be set;
cluster -> c-edge for reverseEdgeDirections of G, E;
coherence
proof
let G2 be reverseEdgeDirections of G, E;
the_Edges_of G = the_Edges_of G2 by GLIB_007:4;
hence thesis by Th19;
end;
end;
registration
let c be Cardinal, G be c-edge _Graph, V be set;
cluster -> c-edge for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
the_Edges_of G = the_Edges_of G1 by GLIB_006:def 10;
hence thesis by Th19;
end;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2, c being Cardinal
st F is isomorphism holds
(G1 is c-vertex iff G2 is c-vertex) &
(G1 is c-edge iff G2 is c-edge) by GLIB_010:84;
begin :: Locally finite Graphs
definition
let G be _Graph;
attr G is locally-finite means :: or finite-branching
:Def5:
for v being Vertex of G holds v.edgesInOut() is finite;
end;
theorem Th23:
for G being _Graph holds G is locally-finite
iff for v being Vertex of G holds v.degree() is finite
proof
let G be _Graph;
hereby
assume A1: G is locally-finite;
let v be Vertex of G;
v.edgesInOut() is finite by A1;
then v.edgesIn() is finite & v.edgesOut() is finite;
hence v.degree() is finite;
end;
assume A2: for v being Vertex of G holds v.degree() is finite;
let v be Vertex of G;
v.degree() is finite by A2;
then v.edgesIn() is finite & v.edgesOut() is finite;
hence thesis;
end;
theorem Th24:
for G1, G2 being _Graph st G1 == G2
holds G1 is locally-finite implies G2 is locally-finite
proof
let G1, G2 be _Graph;
assume A1: G1 == G2 & G1 is locally-finite;
let v be Vertex of G2;
reconsider w = v as Vertex of G1 by A1, GLIB_000:def 34;
v.edgesInOut() = w.edgesInOut() by A1, GLIB_000:96;
hence thesis by A1;
end;
theorem Th25:
for G being _Graph holds G is locally-finite iff
for v being Vertex of G
holds v.edgesIn() is finite & v.edgesOut() is finite
proof
let G be _Graph;
hereby
assume A1: G is locally-finite;
let v be Vertex of G;
v.edgesInOut() is finite by A1;
hence v.edgesIn() is finite & v.edgesOut() is finite;
end;
assume A2: for v being Vertex of G holds
v.edgesIn() is finite & v.edgesOut() is finite;
let v be Vertex of G;
v.edgesIn() is finite & v.edgesOut() is finite by A2;
hence v.edgesInOut() is finite;
end;
theorem
for G being _Graph holds G is locally-finite iff
for v being Vertex of G
holds v.inDegree() is finite & v.outDegree() is finite
proof
let G be _Graph;
hereby
assume A1: G is locally-finite;
let v be Vertex of G;
v.degree() is finite by A1, Th23;
hence v.inDegree() is finite & v.outDegree() is finite;
end;
assume A2: for v being Vertex of G holds
v.inDegree() is finite & v.outDegree() is finite;
now
let v be Vertex of G;
v.inDegree() is finite & v.outDegree() is finite by A2;
hence v.degree() is finite;
end;
hence thesis by Th23;
end;
theorem
for V being non empty set, E being set, S,T being Function of E,V
st for v being Element of V holds S"{v} is finite & T"{v} is finite
holds createGraph(V,E,S,T) is locally-finite
proof
let V be non empty set, E be set, S,T be Function of E,V;
assume A1: for v being Element of V holds S"{v} is finite & T"{v} is finite;
set G = createGraph(V,E,S,T);
now
let v be Vertex of G;
S"{v} is finite & T"{v} is finite by A1;
then (the_Source_of G)"{v} is finite &
(the_Target_of G)"{v} is finite;
hence v.edgesIn() is finite & v.edgesOut() is finite by GLIB_000:147;
end;
hence thesis by Th25;
end;
theorem
for V being non empty set, E being set, S,T being Function of E,V
st ex v being Element of V st S"{v} is infinite or T"{v} is infinite
holds createGraph(V,E,S,T) is non locally-finite
proof
let V be non empty set, E be set, S,T be Function of E,V;
given v being Element of V such that
A1: S"{v} is infinite or T"{v} is infinite;
set G = createGraph(V,E,S,T);
reconsider v as Vertex of G;
per cases by A1;
suppose S"{v} is infinite;
then (the_Source_of G)"{v} is infinite;
then v.edgesOut() is infinite by GLIB_000:147;
hence thesis by Th25;
end;
suppose T"{v} is infinite;
then (the_Target_of G)"{v} is infinite;
then v.edgesIn() is infinite by GLIB_000:147;
hence thesis by Th25;
end;
end;
:: easy creation of non locally-finite graph
registration
let G be non vertex-finite _Graph;
let V be infinite Subset of the_Vertices_of G;
cluster -> non locally-finite for addAdjVertexAll of G,the_Vertices_of G,V;
coherence
proof
let G1 be addAdjVertexAll of G,the_Vertices_of G,V;
A1: not the_Vertices_of G in the_Vertices_of G;
then reconsider v = the_Vertices_of G as Vertex of G1 by GLIB_007:50;
v.degree() = card V by A1, GLIBPRE0:55;
hence thesis by Th23;
end;
end;
registration
cluster edge-finite -> locally-finite for _Graph;
coherence;
cluster locally-finite for _Graph;
existence
proof
take the edge-finite _Graph;
thus thesis;
end;
cluster non locally-finite for _Graph;
existence
proof
set G0 = the non vertex-finite _Graph;
take G = the addAdjVertexAll of G0, the_Vertices_of G0, the_Vertices_of G0;
the_Vertices_of G0 is infinite & the_Vertices_of G0 c= the_Vertices_of G0;
hence thesis;
end;
end;
registration
let G be locally-finite _Graph;
cluster -> locally-finite for Subgraph of G;
coherence
proof
let G2 be Subgraph of G;
let v2 be Vertex of G2;
the_Vertices_of G2 c= the_Vertices_of G;
then reconsider v1 = v2 as Vertex of G by TARSKI:def 3;
A1: v2.edgesInOut() c= v1.edgesInOut() by GLIB_000:78;
v1.edgesInOut() is finite by Def5;
hence thesis by A1;
end;
let X be finite set;
cluster G.edgesInto(X) -> finite;
coherence
proof
set S = {v.edgesIn() where v is Vertex of G : v in X};
defpred P[object,object] means ex v being Vertex of G
st $1 = v & $2 = v.edgesIn();
A2: for x,y1,y2 being object st x in X /\ the_Vertices_of G &
P[x,y1] & P[x,y2] holds y1 = y2;
A3: for x being object st x in X /\ the_Vertices_of G
ex y being object st P[x,y]
proof
let x be object;
assume x in X /\ the_Vertices_of G;
then reconsider v = x as Vertex of G by XBOOLE_0:def 4;
take v.edgesIn(), v;
thus thesis;
end;
consider f being Function such that
A4: dom f = X /\ the_Vertices_of G and
A5: for x being object st x in X /\ the_Vertices_of G holds P[x,f.x]
from FUNCT_1:sch 2(A2, A3);
A6: rng f is finite by A4, FINSET_1:8;
now
let E be object;
assume E in S;
then consider v being Vertex of G such that
A7: E = v.edgesIn() & v in X;
A8: v in X /\ the_Vertices_of G by A7, XBOOLE_0:def 4;
then consider v0 being Vertex of G such that
A9: v = v0 & f.v = v0.edgesIn() by A5;
thus E in rng f by A4, A7, A8, A9, FUNCT_1:3;
end;
then S c= rng f by TARSKI:def 3;
then A10: S is finite by A6;
for E being set st E in S holds E is finite
proof
let E be set;
assume E in S;
then consider v being Vertex of G such that
A11: E = v.edgesIn() & v in X;
thus E is finite by A11, Th25;
end;
then union S is finite by A10, FINSET_1:7;
hence thesis by GLIB_000:158;
end;
cluster G.edgesOutOf(X) -> finite;
coherence
proof
set S = {v.edgesOut() where v is Vertex of G : v in X};
defpred P[object,object] means ex v being Vertex of G
st $1 = v & $2 = v.edgesOut();
A12: for x,y1,y2 being object st x in X /\ the_Vertices_of G &
P[x,y1] & P[x,y2] holds y1 = y2;
A13: for x being object st x in X /\ the_Vertices_of G
ex y being object st P[x,y]
proof
let x be object;
assume x in X /\ the_Vertices_of G;
then reconsider v = x as Vertex of G by XBOOLE_0:def 4;
take v.edgesOut(), v;
thus thesis;
end;
consider f being Function such that
A14: dom f = X /\ the_Vertices_of G and
A15: for x being object st x in X /\ the_Vertices_of G holds P[x,f.x]
from FUNCT_1:sch 2(A12, A13);
A16: rng f is finite by A14, FINSET_1:8;
now
let E be object;
assume E in S;
then consider v being Vertex of G such that
A17: E = v.edgesOut() & v in X;
A18: v in X /\ the_Vertices_of G by A17, XBOOLE_0:def 4;
then consider v0 being Vertex of G such that
A19: v = v0 & f.v = v0.edgesOut() by A15;
thus E in rng f by A14, A17, A18, A19, FUNCT_1:3;
end;
then S c= rng f by TARSKI:def 3;
then A20: S is finite by A16;
for E being set st E in S holds E is finite
proof
let E be set;
assume E in S;
then consider v being Vertex of G such that
A21: E = v.edgesOut() & v in X;
thus E is finite by A21, Th25;
end;
then union S is finite by A20, FINSET_1:7;
hence thesis by GLIB_000:159;
end;
cluster G.edgesInOut(X) -> finite;
coherence;
cluster G.edgesBetween(X) -> finite;
coherence;
let Y be finite set;
cluster G.edgesBetween(X,Y) -> finite;
coherence
proof
set V = the_Vertices_of G;
set S = {v.edgesInOut() /\ w.edgesInOut()
where v, w is Vertex of G : v in X & w in Y};
defpred P[object,object] means ex v,w being Vertex of G
st $1 = [v,w] & $2 = v.edgesInOut() /\ w.edgesInOut();
A22: for x,y1,y2 being object st x in [: X,Y :] /\ [: V,V :] &
P[x,y1] & P[x,y2] holds y1 = y2
proof
let x,y1,y2 be object;
assume A23: x in [: X,Y :] /\ [: V,V :] & P[x,y1] & P[x,y2];
then consider v1,w1 being Vertex of G such that
A24: x = [v1,w1] & y1 = v1.edgesInOut() /\ w1.edgesInOut();
consider v2,w2 being Vertex of G such that
A25: x = [v2,w2] & y2 = v2.edgesInOut() /\ w2.edgesInOut() by A23;
v1 = v2 & w1 = w2 by A24, A25, XTUPLE_0:1;
hence thesis by A24, A25;
end;
A26: for x being object st x in [: X,Y :] /\ [: V,V :]
ex y being object st P[x,y]
proof
let x be object;
assume A27: x in [: X,Y :] /\ [: V,V :];
then x in [: X,Y :] by XBOOLE_0:def 4;
then consider v,w being object such that
A28: v in X & w in Y & x = [v,w] by ZFMISC_1:def 2;
x in [: V,V :] by A27, XBOOLE_0:def 4;
then consider v9,w9 being object such that
A29: v9 in V & w9 in V & x = [v9,w9] by ZFMISC_1:def 2;
reconsider v,w as Vertex of G by A28, A29, XTUPLE_0:1;
take v.edgesInOut() /\ w.edgesInOut(), v,w;
thus thesis by A28;
end;
consider f being Function such that
A30: dom f = [: X,Y :] /\ [: V,V :] and
A31: for x being object st x in [: X,Y :] /\ [: V,V :] holds P[x,f.x]
from FUNCT_1:sch 2(A22, A26);
A32: rng f is finite by A30, FINSET_1:8;
now
let E be object;
assume E in S;
then consider v,w being Vertex of G such that
A33: E = v.edgesInOut() /\ w.edgesInOut() & v in X & w in Y;
A34: [v,w] in [: X,Y :] by A33, ZFMISC_1:def 2;
[v,w] in [: V,V :] by ZFMISC_1:def 2;
then A35: [v,w] in [: X,Y :] /\ [: V,V :] by A34, XBOOLE_0:def 4;
then consider v0,w0 being Vertex of G such that
A36: [v,w] = [v0,w0] & f.[v,w] = v0.edgesInOut() /\ w0.edgesInOut()
by A31;
v = v0 & w = w0 by A36, XTUPLE_0:1;
hence E in rng f by A30, A33, A35, A36, FUNCT_1:3;
end;
then S c= rng f by TARSKI:def 3;
then A37: S is finite by A32;
for E being set st E in S holds E is finite
proof
let E be set;
assume E in S;
then consider v,w being Vertex of G such that
A38: E = v.edgesInOut() /\ w.edgesInOut() & v in X & w in Y;
thus E is finite by A38;
end;
then A39: union S is finite by A37, FINSET_1:7;
G.edgesBetween(X,Y) c= union S by GLIB_000:162;
hence thesis by A39;
end;
cluster G.edgesDBetween(X,Y) -> finite;
coherence
proof
G.edgesDBetween(X,Y) c= G.edgesBetween(X,Y) by GLIB_000:153;
hence thesis;
end;
end;
registration
let G be locally-finite _Graph, v be Vertex of G;
cluster v.edgesIn() -> finite;
coherence;
cluster v.edgesOut() -> finite;
coherence;
cluster v.edgesInOut() -> finite;
coherence;
cluster v.inDegree() -> finite;
coherence;
cluster v.outDegree() -> finite;
coherence;
cluster v.degree() -> finite;
coherence;
end;
definition
let G be locally-finite _Graph, v be Vertex of G;
redefine func v.inDegree() -> Nat; :: redefines .inDegree() (GLIB_000, definition)
coherence;
redefine func v.outDegree() -> Nat; :: redefines .outDegree() (GLIB_000, definition)
coherence;
redefine func v.degree() -> Nat; :: redefines .degree() (GLIB_000, definition)
coherence;
end;
registration
let G be locally-finite _Graph, V be set;
cluster -> locally-finite for addVertices of G, V;
coherence
proof
let G1 be addVertices of G, V;
let v be Vertex of G1;
the_Vertices_of G1 = the_Vertices_of G \/ V by GLIB_006:def 10;
then per cases by XBOOLE_0:def 3;
suppose v in the_Vertices_of G;
then reconsider v0 = v as Vertex of G;
v0.edgesInOut() is finite;
hence v.edgesInOut() is finite by GLIBPRE0:45;
end;
suppose v in V & not v in the_Vertices_of G;
then v in V \ the_Vertices_of G by XBOOLE_0:def 5;
hence v.edgesInOut() is finite by GLIB_006:88, GLIB_000:def 49;
end;
end;
cluster -> locally-finite for addLoops of G, V;
coherence
proof
let G1 be addLoops of G, V;
per cases;
suppose A1: V c= the_Vertices_of G;
let v1 be Vertex of G1;
reconsider v2 = v1 as Vertex of G by A1, GLIB_012:def 5;
per cases;
suppose v1 in V;
then consider e being object such that
e DJoins v1,v1,G1 & not e in the_Edges_of G and
v1.edgesIn() = v2.edgesIn() \/ {e} and
v1.edgesOut() = v2.edgesOut() \/ {e} and
A2: v1.edgesInOut() = v2.edgesInOut() \/ {e} by A1, GLIB_012:42;
thus thesis by A2;
end;
suppose not v1 in V;
then v1.edgesInOut() = v2.edgesInOut() by A1, GLIB_012:44;
hence thesis;
end;
end;
suppose not V c= the_Vertices_of G;
then G1 == G by GLIB_012:def 5;
hence thesis by Th24;
end;
end;
end;
registration
let G be locally-finite _Graph, E be set;
cluster -> locally-finite for reverseEdgeDirections of G, E;
coherence
proof
let G2 be reverseEdgeDirections of G, E;
let v2 be Vertex of G2;
reconsider v1 = v2 as Vertex of G by GLIB_007:4;
v1.edgesInOut() = v2.edgesInOut() by GLIB_007:12;
hence thesis;
end;
end;
registration
let G be locally-finite _Graph;
let v,e,w be object;
cluster -> locally-finite for addEdge of G, v, e, w;
coherence
proof
let G1 be addEdge of G, v, e, w;
per cases;
suppose A1: v is Vertex of G & w is Vertex of G & not e in the_Edges_of G;
then reconsider v0 = v, w0 = w as Vertex of G;
let v1 be Vertex of G1;
reconsider v2 = v1 as Vertex of G by A1, GLIB_006:def 11;
per cases;
suppose v2 <> v & v2 <> w;
then v1.edgesInOut() = v2.edgesInOut() by GLIBPRE0:46;
hence thesis;
end;
suppose v2 = v & v <> w;
then v1.edgesInOut() = v0.edgesInOut() \/ {e} by A1, GLIBPRE0:47;
hence thesis;
end;
suppose v2 = w & v <> w;
then v1.edgesInOut() = w0.edgesInOut() \/ {e} by A1, GLIBPRE0:48;
hence thesis;
end;
suppose v2 = v & v = w;
then v1.edgesInOut() = v0.edgesInOut() \/ {e} by A1, GLIBPRE0:49;
hence thesis;
end;
end;
suppose not(v is Vertex of G & w is Vertex of G & not e in the_Edges_of G);
then G1 == G by GLIB_006:def 11;
hence thesis by Th24;
end;
end;
cluster -> locally-finite for addAdjVertex of G, v, e, w;
coherence
proof
let G1 be addAdjVertex of G, v, e, w;
per cases;
suppose v in the_Vertices_of G & not w in the_Vertices_of G &
not e in the_Edges_of G;
then consider G3 being addVertex of G,w such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:125;
thus thesis by A2;
end;
suppose not v in the_Vertices_of G & w in the_Vertices_of G &
not e in the_Edges_of G;
then consider G3 being addVertex of G,v such that
A3: G1 is addEdge of G3,v,e,w by GLIB_006:126;
thus thesis by A3;
end;
suppose not((v in the_Vertices_of G & not w in the_Vertices_of G &
not e in the_Edges_of G) or (not v in the_Vertices_of G &
w in the_Vertices_of G & not e in the_Edges_of G));
then G1 == G by GLIB_006:def 12;
hence thesis by Th24;
end;
end;
end;
theorem Th29:
for G2 being _Graph, v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2, v, V st not v in the_Vertices_of G2
holds (G2 is locally-finite & V is finite) iff G1 is locally-finite
proof
let G2 be _Graph, v be object, V be Subset of the_Vertices_of G2;
let G1 be addAdjVertexAll of G2, v, V;
assume A1: not v in the_Vertices_of G2;
hereby
assume A2: G2 is locally-finite & V is finite;
now
let v1 be Vertex of G1;
per cases;
suppose v1 = v;
then v1.degree() = card V by A1, GLIBPRE0:55;
hence v1.degree() is finite by A2;
end;
suppose v1 <> v;
then A3: not v1 in {v} by TARSKI:def 1;
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, GLIB_007:def 4;
then reconsider v2 = v1 as Vertex of G2 by A3, XBOOLE_0:def 3;
per cases;
suppose not v2 in V;
then v1.degree() = v2.degree() by GLIBPRE0:56;
hence v1.degree() is finite by A2;
end;
suppose v2 in V;
then v1.degree() = v2.degree() +` 1 by A1, GLIBPRE0:57;
hence v1.degree() is finite by A2;
end;
end;
end;
hence G1 is locally-finite by Th23;
end;
assume A4: G1 is locally-finite;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is locally-finite by A4;
reconsider w = v as Vertex of G1 by A1, GLIB_007:50;
w.degree() is finite by A4;
then card V is finite by A1, GLIBPRE0:55;
hence V is finite;
end;
registration
let G be locally-finite _Graph;
let v be object, V be finite set;
cluster -> locally-finite for addAdjVertexAll of G, v, V;
coherence
proof
let G1 be addAdjVertexAll of G,v,V;
per cases;
suppose V c= the_Vertices_of G & not v in the_Vertices_of G;
hence thesis by Th29;
end;
suppose not(V c= the_Vertices_of G & not v in the_Vertices_of G);
then G1 == G by GLIB_007:def 4;
hence thesis by Th24;
end;
end;
end;
registration
let G be non locally-finite _Graph;
cluster -> non locally-finite for Supergraph of G;
coherence
proof
let G1 be Supergraph of G;
G is Subgraph of G1 by GLIB_006:57;
hence thesis;
end;
let E be finite set;
cluster -> non locally-finite for removeEdges of G, E;
coherence
proof
let G2 be removeEdges of G, E;
consider v1 being Vertex of G such that
A1: v1.edgesInOut() is infinite by Def5;
reconsider v2 = v1 as Vertex of G2 by GLIB_000:53;
v2.edgesInOut() = v1.edgesInOut() \ E by GLIB_000:164;
hence thesis by A1;
end;
end;
registration
let G be non locally-finite _Graph, e be set;
cluster -> non locally-finite for removeEdge of G, e;
coherence;
end;
theorem Th30:
for G1 being non locally-finite _Graph
for V being finite Subset of the_Vertices_of G1
for G2 being removeVertices of G1, V
st for v being Vertex of G1 st v in V holds v.edgesInOut() is finite
holds G2 is non locally-finite
proof
let G1 be non locally-finite _Graph;
let V be finite Subset of the_Vertices_of G1;
let G2 be removeVertices of G1, V;
assume A1: for v being Vertex of G1 st v in V holds v.edgesInOut() is finite;
per cases;
suppose A2: the_Vertices_of G1 \ V is non empty Subset of the_Vertices_of G1;
consider v1 being Vertex of G1 such that
A3: v1.edgesInOut() is infinite by Def5;
A4: the_Vertices_of G2 = the_Vertices_of G1 \ V by A2, GLIB_000:def 37;
not v1 in V by A1, A3;
then reconsider v2 = v1 as Vertex of G2 by A4, XBOOLE_0:def 5;
not the_Vertices_of G1 c= V by A2, XBOOLE_1:37;
then V c< the_Vertices_of G1 by XBOOLE_0:def 8;
then A5: v2.edgesInOut() = v1.edgesInOut() \ G1.edgesInOut(V)
by GLIB_000:166;
deffunc F(Vertex of G1) = $1.edgesInOut();
set S = {F(v) where v is Vertex of G1 : v in V};
A6: V is finite;
A7: S is finite from FRAENKEL:sch 21(A6);
now
let X be set;
assume X in S;
then consider v being Vertex of G1 such that
A8: X = F(v) & v in V;
thus X is finite by A1, A8;
end;
then union S is finite by A7, FINSET_1:7;
then G1.edgesInOut(V) is finite by GLIB_000:160;
hence thesis by A3, A5;
end;
suppose not(the_Vertices_of G1\V is non empty Subset of the_Vertices_of G1);
then G1 == G2 by GLIB_000:def 37;
hence thesis by Th24;
end;
end;
theorem
for G1 being non locally-finite _Graph, v being Vertex of G1
for G2 being removeVertex of G1, v st v.edgesInOut() is finite
holds G2 is non locally-finite
proof
let G1 be non locally-finite _Graph, v be Vertex of G1;
let G2 be removeVertex of G1, v;
assume A1: v.edgesInOut() is finite;
for w being Vertex of G1 st w in {v} holds w.edgesInOut() is finite
by A1, TARSKI:def 1;
hence thesis by Th30;
end;
theorem Th32:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding & G2 is locally-finite holds G1 is locally-finite
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is locally-finite;
now
let v be Vertex of G1;
v.degree() c= (F_V/.v).degree() by A1, GLIBPRE0:89;
hence v.degree() is finite by A1;
end;
hence thesis by Th23;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous & G1 is locally-finite
holds G2 is locally-finite
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto semi-Dcontinuous & G1 is locally-finite;
now
let v be Vertex of G2;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A2: v0 in dom F_V & F_V.v0 = v by FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A2;
(F_V/.v0).degree() c= v0.degree() by A1, A2, GLIBPRE0:91;
hence v.degree() is finite by A1, A2, PARTFUN1:def 6;
end;
hence thesis by Th23;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is locally-finite iff G2 is locally-finite
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
hereby
assume A2: G1 is locally-finite;
now
let v be Vertex of G2;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A3: v0 in dom F_V & F_V.v0 = v by FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A3;
(F_V/.v0).degree() = v0.degree() by A1, GLIBPRE0:93;
hence v.degree() is finite by A2, A3, PARTFUN1:def 6;
end;
hence G2 is locally-finite by Th23;
end;
thus thesis by A1, Th32;
end;
begin :: Degree properties in Graphs
definition
let G be _Graph;
func G.supDegree() -> Cardinal equals
union the set of all v.degree() where v is Vertex of G;
coherence
proof
now
let x be set;
assume x in the set of all v.degree() where v is Vertex of G;
then consider v being Vertex of G such that
A1: x = v.degree();
thus x is cardinal number by A1;
end;
hence thesis by TOPGEN_2:3;
end;
func G.supInDegree() -> Cardinal equals
union the set of all v.inDegree() where v is Vertex of G;
coherence
proof
now
let x be set;
assume x in the set of all v.inDegree() where v is Vertex of G;
then consider v being Vertex of G such that
A2: x = v.inDegree();
thus x is cardinal number by A2;
end;
hence thesis by TOPGEN_2:3;
end;
func G.supOutDegree() -> Cardinal equals
union the set of all v.outDegree() where v is Vertex of G;
coherence
proof
now
let x be set;
assume x in the set of all v.outDegree() where v is Vertex of G;
then consider v being Vertex of G such that
A3: x = v.outDegree();
thus x is cardinal number by A3;
end;
hence thesis by TOPGEN_2:3;
end;
func G.minDegree() -> Cardinal equals
meet the set of all v.degree() where v is Vertex of G;
coherence
proof
now
let x be set;
assume x in the set of all v.degree() where v is Vertex of G;
then consider v being Vertex of G such that
A4: x = v.degree();
thus x is cardinal number by A4;
end;
hence thesis by GLIBPRE0:15;
end;
func G.minInDegree() -> Cardinal equals
meet the set of all v.inDegree() where v is Vertex of G;
coherence
proof
now
let x be set;
assume x in the set of all v.inDegree() where v is Vertex of G;
then consider v being Vertex of G such that
A5: x = v.inDegree();
thus x is cardinal number by A5;
end;
hence thesis by GLIBPRE0:15;
end;
func G.minOutDegree() -> Cardinal equals
meet the set of all v.outDegree() where v is Vertex of G;
coherence
proof
now
let x be set;
assume x in the set of all v.outDegree() where v is Vertex of G;
then consider v being Vertex of G such that
A6: x = v.outDegree();
thus x is cardinal number by A6;
end;
hence thesis by GLIBPRE0:15;
end;
end;
theorem Th35:
for G being _Graph, v being Vertex of G holds
G.minDegree() c= v.degree() & v.degree() c= G.supDegree() &
G.minInDegree() c= v.inDegree() & v.inDegree() c= G.supInDegree() &
G.minOutDegree() c= v.outDegree() & v.outDegree() c= G.supOutDegree()
proof
let G be _Graph, v be Vertex of G;
v.degree() in the set of all w.degree() where w is Vertex of G;
hence G.minDegree() c= v.degree() & v.degree() c= G.supDegree()
by ZFMISC_1:74, SETFAM_1:3;
v.inDegree() in the set of all w.inDegree() where w is Vertex of G;
hence G.minInDegree() c= v.inDegree() & v.inDegree() c= G.supInDegree()
by ZFMISC_1:74, SETFAM_1:3;
v.outDegree() in the set of all w.outDegree() where w is Vertex of G;
hence G.minOutDegree() c= v.outDegree() & v.outDegree() c= G.supOutDegree()
by ZFMISC_1:74, SETFAM_1:3;
end;
theorem Th36:
for G being _Graph, c being Cardinal holds G.minDegree() = c iff
ex v being Vertex of G st v.degree() = c &
for w being Vertex of G holds v.degree() c= w.degree()
proof
let G be _Graph, c be Cardinal;
set S = the set of all v.degree() where v is Vertex of G;
(the Vertex of G).degree() in S;
then A1: S <> {};
now
let x be set;
assume x in S;
then consider v being Vertex of G such that
A2: x = v.degree();
thus x is cardinal number by A2;
end;
then consider A being Cardinal such that
A3: A in S & A = G.minDegree() by A1, GLIBPRE0:14;
hereby
assume A4: G.minDegree() = c;
consider v being Vertex of G such that
A5: A = v.degree() by A3;
take v;
thus v.degree() = c by A4, A3, A5;
let w be Vertex of G;
w.degree() in S;
hence v.degree() c= w.degree() by A3, A5, SETFAM_1:3;
end;
given v being Vertex of G such that
A6: v.degree() = c and
A7: for w being Vertex of G holds v.degree() c= w.degree();
c in S by A6;
then A8: G.minDegree() c= c by SETFAM_1:3;
now
let x be object;
assume A9: x in c;
now
let X be set;
assume X in S;
then consider w being Vertex of G such that
A10: X = w.degree();
c c= X by A6, A7, A10;
hence x in X by A9;
end;
hence x in meet S by A1, SETFAM_1:def 1;
end;
then c c= G.minDegree() by TARSKI:def 3;
hence G.minDegree() = c by A8, XBOOLE_0:def 10;
end;
theorem Th37:
for G being _Graph, c being Cardinal holds G.minInDegree() = c iff
ex v being Vertex of G st v.inDegree() = c &
for w being Vertex of G holds v.inDegree() c= w.inDegree()
proof
let G be _Graph, c be Cardinal;
set S = the set of all v.inDegree() where v is Vertex of G;
(the Vertex of G).inDegree() in S;
then A1: S <> {};
now
let x be set;
assume x in S;
then consider v being Vertex of G such that
A2: x = v.inDegree();
thus x is cardinal number by A2;
end;
then consider A being Cardinal such that
A3: A in S & A = G.minInDegree() by A1, GLIBPRE0:14;
hereby
assume A4: G.minInDegree() = c;
consider v being Vertex of G such that
A5: A = v.inDegree() by A3;
take v;
thus v.inDegree() = c by A4, A3, A5;
let w be Vertex of G;
w.inDegree() in S;
hence v.inDegree() c= w.inDegree() by A3, A5, SETFAM_1:3;
end;
given v being Vertex of G such that
A6: v.inDegree() = c and
A7: for w being Vertex of G holds v.inDegree() c= w.inDegree();
c in S by A6;
then A8: G.minInDegree() c= c by SETFAM_1:3;
now
let x be object;
assume A9: x in c;
now
let X be set;
assume X in S;
then consider w being Vertex of G such that
A10: X = w.inDegree();
c c= X by A6, A7, A10;
hence x in X by A9;
end;
hence x in meet S by A1, SETFAM_1:def 1;
end;
then c c= G.minInDegree() by TARSKI:def 3;
hence G.minInDegree() = c by A8, XBOOLE_0:def 10;
end;
theorem Th38:
for G being _Graph, c being Cardinal holds G.minOutDegree() = c iff
ex v being Vertex of G st v.outDegree() = c &
for w being Vertex of G holds v.outDegree() c= w.outDegree()
proof
let G be _Graph, c be Cardinal;
set S = the set of all v.outDegree() where v is Vertex of G;
(the Vertex of G).outDegree() in S;
then A1: S <> {};
now
let x be set;
assume x in S;
then consider v being Vertex of G such that
A2: x = v.outDegree();
thus x is cardinal number by A2;
end;
then consider A being Cardinal such that
A3: A in S & A = G.minOutDegree() by A1, GLIBPRE0:14;
hereby
assume A4: G.minOutDegree() = c;
consider v being Vertex of G such that
A5: A = v.outDegree() by A3;
take v;
thus v.outDegree() = c by A4, A3, A5;
let w be Vertex of G;
w.outDegree() in S;
hence v.outDegree() c= w.outDegree() by A3, A5, SETFAM_1:3;
end;
given v being Vertex of G such that
A6: v.outDegree() = c and
A7: for w being Vertex of G holds v.outDegree() c= w.outDegree();
c in S by A6;
then A8: G.minOutDegree() c= c by SETFAM_1:3;
now
let x be object;
assume A9: x in c;
now
let X be set;
assume X in S;
then consider w being Vertex of G such that
A10: X = w.outDegree();
c c= X by A6, A7, A10;
hence x in X by A9;
end;
hence x in meet S by A1, SETFAM_1:def 1;
end;
then c c= G.minOutDegree() by TARSKI:def 3;
hence G.minOutDegree() = c by A8, XBOOLE_0:def 10;
end;
theorem Th39:
for G being _Graph holds G.supInDegree() c= G.supDegree()
proof
let G be _Graph;
now
let x be object;
assume x in G.supInDegree();
then consider X being set such that
A1: x in X & X in the set of all v.inDegree() where v is Vertex of G
by TARSKI:def 4;
consider v being Vertex of G such that
A2: X = v.inDegree() by A1;
v.inDegree() c= v.degree() by CARD_2:94;
then A3: x in v.degree() by A1, A2;
v.degree() in the set of all w.degree() where w is Vertex of G;
hence x in G.supDegree() by A3, TARSKI:def 4;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th40:
for G being _Graph holds G.supOutDegree() c= G.supDegree()
proof
let G be _Graph;
now
let x be object;
assume x in G.supOutDegree();
then consider X being set such that
A1: x in X & X in the set of all v.outDegree() where v is Vertex of G
by TARSKI:def 4;
consider v being Vertex of G such that
A2: X = v.outDegree() by A1;
v.outDegree() c= v.degree() by CARD_2:94;
then A3: x in v.degree() by A1, A2;
v.degree() in the set of all w.degree() where w is Vertex of G;
hence x in G.supDegree() by A3, TARSKI:def 4;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for G being _Graph holds G.minInDegree() c= G.minDegree()
proof
let G be _Graph;
consider v1 being Vertex of G such that
A1: v1.inDegree() = G.minInDegree() and
A2: for w being Vertex of G holds v1.inDegree() c= w.inDegree() by Th37;
consider v2 being Vertex of G such that
A3: v2.degree() = G.minDegree() and
for w being Vertex of G holds v2.degree() c= w.degree() by Th36;
A4: v2.inDegree() c= G.minDegree() by A3, CARD_2:94;
v1.inDegree() c= v2.inDegree() by A2;
hence thesis by A1, A4, XBOOLE_1:1;
end;
theorem
for G being _Graph holds G.minOutDegree() c= G.minDegree()
proof
let G be _Graph;
consider v1 being Vertex of G such that
A1: v1.outDegree() = G.minOutDegree() and
A2: for w being Vertex of G holds v1.outDegree() c= w.outDegree() by Th38;
consider v2 being Vertex of G such that
A3: v2.degree() = G.minDegree() and
for w being Vertex of G holds v2.degree() c= w.degree() by Th36;
A4: v2.outDegree() c= G.minDegree() by A3, CARD_2:94;
v1.outDegree() c= v2.outDegree() by A2;
hence thesis by A1, A4, XBOOLE_1:1;
end;
theorem
for G being _Graph holds G.minDegree() c= G.supDegree() by SETFAM_1:2;
theorem
for G being _Graph holds G.minInDegree() c= G.supInDegree() by SETFAM_1:2;
theorem
for G being _Graph holds G.minOutDegree() c= G.supOutDegree() by SETFAM_1:2;
theorem Th46:
for G being _Graph st ex v being Vertex of G st v is isolated
holds G.minDegree() = 0 & G.minInDegree() = 0 & G.minOutDegree() = 0
proof
let G be _Graph;
given v being Vertex of G such that
A1: v is isolated;
A2: v.degree() = 0 by A1, GLIB_000:157;
for w be Vertex of G holds v.degree() c= w.degree() by A2, XBOOLE_1:2;
hence G.minDegree() = 0 by A2, Th36;
A3: v.inDegree() = 0 & v.outDegree() = 0 by A1, GLIB_000:156;
for w be Vertex of G holds v.inDegree() c= w.inDegree() by A3, XBOOLE_1:2;
hence G.minInDegree() = 0 by A3, Th37;
for w be Vertex of G holds v.outDegree() c= w.outDegree() by A3, XBOOLE_1:2;
hence G.minOutDegree() = 0 by A3, Th38;
end;
theorem
for G being _Graph st G.minDegree() = 0
ex v being Vertex of G st v is isolated
proof
let G be _Graph;
assume G.minDegree() = 0;
then consider v being Vertex of G such that
A1: v.degree() = 0 and
for w being Vertex of G holds v.degree() c= w.degree() by Th36;
take v;
thus thesis by A1, GLIB_000:157;
end;
::theorem
::for G being with_isolated_vertices _Graph
::holds G.minDegree() = 0 & G.minInDegree() = 0 & G.minOutDegree() = 0;
::theorem
::for G being without_isolated_vertices _Graph holds G.minDegree() <> 0;
theorem Th48:
for G being _Graph, c being Cardinal
st ex v being Vertex of G st v.degree() = c &
for w being Vertex of G holds w.degree() c= v.degree()
holds G.supDegree() = c
proof
let G be _Graph, c be Cardinal;
given v being Vertex of G such that
A1: v.degree() = c and
A2: for w being Vertex of G holds w.degree() c= v.degree();
set S = the set of all v.degree() where v is Vertex of G;
c in S by A1;
then A3: c c= G.supDegree() by ZFMISC_1:74;
now
let x be object;
assume x in G.supDegree();
then consider X being set such that
A4: x in X & X in S by TARSKI:def 4;
consider w being Vertex of G such that
A5: X = w.degree() by A4;
X c= v.degree() by A2, A5;
hence x in c by A1, A4;
end;
then G.supDegree() c= c by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
theorem Th49:
for G being _Graph, c being Cardinal
st ex v being Vertex of G st v.inDegree() = c &
for w being Vertex of G holds w.inDegree() c= v.inDegree()
holds G.supInDegree() = c
proof
let G be _Graph, c be Cardinal;
given v being Vertex of G such that
A1: v.inDegree() = c and
A2: for w being Vertex of G holds w.inDegree() c= v.inDegree();
set S = the set of all v.inDegree() where v is Vertex of G;
c in S by A1;
then A3: c c= G.supInDegree() by ZFMISC_1:74;
now
let x be object;
assume x in G.supInDegree();
then consider X being set such that
A4: x in X & X in S by TARSKI:def 4;
consider w being Vertex of G such that
A5: X = w.inDegree() by A4;
X c= v.inDegree() by A2, A5;
hence x in c by A1, A4;
end;
then G.supInDegree() c= c by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
theorem Th50:
for G being _Graph, c being Cardinal
st ex v being Vertex of G st v.outDegree() = c &
for w being Vertex of G holds w.outDegree() c= v.outDegree()
holds G.supOutDegree() = c
proof
let G be _Graph, c be Cardinal;
given v being Vertex of G such that
A1: v.outDegree() = c and
A2: for w being Vertex of G holds w.outDegree() c= v.outDegree();
set S = the set of all v.outDegree() where v is Vertex of G;
c in S by A1;
then A3: c c= G.supOutDegree() by ZFMISC_1:74;
now
let x be object;
assume x in G.supOutDegree();
then consider X being set such that
A4: x in X & X in S by TARSKI:def 4;
consider w being Vertex of G such that
A5: X = w.outDegree() by A4;
X c= v.outDegree() by A2, A5;
hence x in c by A1, A4;
end;
then G.supOutDegree() c= c by TARSKI:def 3;
hence thesis by A3, XBOOLE_0:def 10;
end;
theorem Th51:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding holds G1.supDegree() c= G2.supDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding;
set D1 = the set of all v.degree() where v is Vertex of G1;
set D2 = the set of all w.degree() where w is Vertex of G2;
now
let x be object;
assume x in G1.supDegree();
then consider d1 being set such that
A2: x in d1 & d1 in D1 by TARSKI:def 4;
consider v being Vertex of G1 such that
A3: d1 = v.degree() by A2;
v.degree() c= (F_V/.v).degree() by A1, GLIBPRE0:89;
then A4: x in (F_V/.v).degree() by A2, A3;
(F_V/.v).degree() in D2;
hence x in G2.supDegree() by A4, TARSKI:def 4;
end;
hence G1.supDegree() c= G2.supDegree() by TARSKI:def 3;
end;
theorem Th52:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is weak_SG-embedding & rng F_V = the_Vertices_of G2 holds
G1.minDegree() c= G2.minDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & rng F_V = the_Vertices_of G2;
consider v1 being Vertex of G1 such that
A2: v1.degree() = G1.minDegree() and
A3: for w1 being Vertex of G1 holds v1.degree() c= w1.degree() by Th36;
consider v2 being Vertex of G2 such that
A4: v2.degree() = G2.minDegree() and
for w2 being Vertex of G2 holds v2.degree() c= w2.degree() by Th36;
consider v0 being object such that
A5: v0 in dom F_V & F_V.v0 = v2 by A1, FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A5;
v0.degree() c= (F_V/.v0).degree() by A1, GLIBPRE0:89;
then A6: v0.degree() c= v2.degree() by A5, PARTFUN1:def 6;
v1.degree() c= v0.degree() by A3;
hence thesis by A2, A4, A6, XBOOLE_1:1;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous holds G2.supDegree() c= G1.supDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto semi-Dcontinuous;
set D1 = the set of all v.degree() where v is Vertex of G1;
set D2 = the set of all w.degree() where w is Vertex of G2;
now
let x be object;
assume x in G2.supDegree();
then consider d2 being set such that
A2: x in d2 & d2 in D2 by TARSKI:def 4;
consider w being Vertex of G2 such that
A3: d2 = w.degree() by A2;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v being object such that
A4: v in dom F_V & F_V.v = w by FUNCT_1:def 3;
reconsider v as Vertex of G1 by A4;
(F_V/.v).degree() c= v.degree() by A1, A4, GLIBPRE0:91;
then w.degree() c= v.degree() by A4, PARTFUN1:def 6;
then A5: x in v.degree() by A2, A3;
v.degree() in D1;
hence x in G1.supDegree() by A5, TARSKI:def 4;
end;
hence thesis by TARSKI:def 3;
end;
theorem
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous & dom F_V = the_Vertices_of G1
holds G2.minDegree() c= G1.minDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto semi-Dcontinuous & dom F_V = the_Vertices_of G1;
consider v1 being Vertex of G1 such that
A2: v1.degree() = G1.minDegree() and
for w1 being Vertex of G1 holds v1.degree() c= w1.degree() by Th36;
consider v2 being Vertex of G2 such that
A3: v2.degree() = G2.minDegree() and
A4: for w2 being Vertex of G2 holds v2.degree() c= w2.degree() by Th36;
A5: (F_V/.v1).degree() c= v1.degree() by A1, GLIBPRE0:91;
v2.degree() c= (F_V/.v1).degree() by A4;
hence thesis by A2, A3, A5, XBOOLE_1:1;
end;
theorem Th55:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism
holds G1.supDegree() = G2.supDegree() & G1.minDegree() = G2.minDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then rng F_V = the_Vertices_of G2 by GLIB_010:def 12;
then A2: G1.supDegree() c= G2.supDegree() & G1.minDegree() c= G2.minDegree()
by A1, Th51, Th52;
reconsider F0 = F as one-to-one PGraphMapping of G1, G2 by A1;
A3: F0" is isomorphism by A1, GLIB_010:75;
then rng (F0"_V) = the_Vertices_of G1 by GLIB_010:def 12;
then G2.supDegree() c= G1.supDegree() & G2.minDegree() c= G1.minDegree()
by A3, Th51, Th52;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th56:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is directed weak_SG-embedding holds
G1.supInDegree() c= G2.supInDegree() &
G1.supOutDegree() c= G2.supOutDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is directed weak_SG-embedding;
set D1 = the set of all v.inDegree() where v is Vertex of G1;
set D2 = the set of all w.inDegree() where w is Vertex of G2;
now
let x be object;
assume x in G1.supInDegree();
then consider d1 being set such that
A2: x in d1 & d1 in D1 by TARSKI:def 4;
consider v being Vertex of G1 such that
A3: d1 = v.inDegree() by A2;
v.inDegree() c= (F_V/.v).inDegree() by A1, GLIBPRE0:88;
then A4: x in (F_V/.v).inDegree() by A2, A3;
(F_V/.v).inDegree() in D2;
hence x in G2.supInDegree() by A4, TARSKI:def 4;
end;
hence G1.supInDegree() c= G2.supInDegree() by TARSKI:def 3;
set D3 = the set of all v.outDegree() where v is Vertex of G1;
set D4 = the set of all w.outDegree() where w is Vertex of G2;
now
let x be object;
assume x in G1.supOutDegree();
then consider d1 being set such that
A5: x in d1 & d1 in D3 by TARSKI:def 4;
consider v being Vertex of G1 such that
A6: d1 = v.outDegree() by A5;
v.outDegree() c= (F_V/.v).outDegree() by A1, GLIBPRE0:88;
then A7: x in (F_V/.v).outDegree() by A5, A6;
(F_V/.v).outDegree() in D4;
hence x in G2.supOutDegree() by A7, TARSKI:def 4;
end;
hence G1.supOutDegree() c= G2.supOutDegree() by TARSKI:def 3;
end;
theorem Th57:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is directed weak_SG-embedding & rng F_V = the_Vertices_of G2 holds
G1.minInDegree() c= G2.minInDegree() &
G1.minOutDegree() c= G2.minOutDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is directed weak_SG-embedding & rng F_V = the_Vertices_of G2;
consider v1 being Vertex of G1 such that
A2: v1.inDegree() = G1.minInDegree() and
A3: for w1 being Vertex of G1 holds v1.inDegree() c= w1.inDegree() by Th37;
consider v2 being Vertex of G2 such that
A4: v2.inDegree() = G2.minInDegree() and
for w2 being Vertex of G2 holds v2.inDegree() c= w2.inDegree() by Th37;
consider v0 being object such that
A5: v0 in dom F_V & F_V.v0 = v2 by A1, FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A5;
v0.inDegree() c= (F_V/.v0).inDegree() by A1, GLIBPRE0:88;
then A6: v0.inDegree() c= v2.inDegree() by A5, PARTFUN1:def 6;
v1.inDegree() c= v0.inDegree() by A3;
hence G1.minInDegree() c= G2.minInDegree() by A2, A4, A6, XBOOLE_1:1;
consider v3 being Vertex of G1 such that
A7: v3.outDegree() = G1.minOutDegree() and
A8: for w3 being Vertex of G1 holds v3.outDegree()c=w3.outDegree() by Th38;
consider v4 being Vertex of G2 such that
A9: v4.outDegree() = G2.minOutDegree() and
for w4 being Vertex of G2 holds v4.outDegree() c= w4.outDegree() by Th38;
consider v9 being object such that
A10: v9 in dom F_V & F_V.v9 = v4 by A1, FUNCT_1:def 3;
reconsider v9 as Vertex of G1 by A10;
v9.outDegree() c= (F_V/.v9).outDegree() by A1, GLIBPRE0:88;
then A11: v9.outDegree() c= v4.outDegree() by A10, PARTFUN1:def 6;
v3.outDegree() c= v9.outDegree() by A8;
hence thesis by A7, A9, A11, XBOOLE_1:1;
end;
theorem Th58:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous holds
G2.supInDegree() c= G1.supInDegree() &
G2.supOutDegree() c= G1.supOutDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto semi-Dcontinuous;
set D1 = the set of all v.inDegree() where v is Vertex of G1;
set D2 = the set of all w.inDegree() where w is Vertex of G2;
now
let x be object;
assume x in G2.supInDegree();
then consider d2 being set such that
A2: x in d2 & d2 in D2 by TARSKI:def 4;
consider w being Vertex of G2 such that
A3: d2 = w.inDegree() by A2;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v being object such that
A4: v in dom F_V & F_V.v = w by FUNCT_1:def 3;
reconsider v as Vertex of G1 by A4;
(F_V/.v).inDegree() c= v.inDegree() by A1, A4, GLIBPRE0:90;
then w.inDegree() c= v.inDegree() by A4, PARTFUN1:def 6;
then A5: x in v.inDegree() by A2, A3;
v.inDegree() in D1;
hence x in G1.supInDegree() by A5, TARSKI:def 4;
end;
hence G2.supInDegree() c= G1.supInDegree() by TARSKI:def 3;
set D3 = the set of all v.outDegree() where v is Vertex of G1;
set D4 = the set of all w.outDegree() where w is Vertex of G2;
now
let x be object;
assume x in G2.supOutDegree();
then consider d2 being set such that
A6: x in d2 & d2 in D4 by TARSKI:def 4;
consider w being Vertex of G2 such that
A7: d2 = w.outDegree() by A6;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v being object such that
A8: v in dom F_V & F_V.v = w by FUNCT_1:def 3;
reconsider v as Vertex of G1 by A8;
(F_V/.v).outDegree() c= v.outDegree() by A1, A8, GLIBPRE0:90;
then w.outDegree() c= v.outDegree() by A8, PARTFUN1:def 6;
then A9: x in v.outDegree() by A6, A7;
v.outDegree() in D3;
hence x in G1.supOutDegree() by A9, TARSKI:def 4;
end;
hence G2.supOutDegree() c= G1.supOutDegree() by TARSKI:def 3;
end;
theorem Th59:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is onto semi-Dcontinuous & dom F_V = the_Vertices_of G1 holds
G2.minInDegree() c= G1.minInDegree() &
G2.minOutDegree() c= G1.minOutDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is onto semi-Dcontinuous & dom F_V = the_Vertices_of G1;
consider v1 being Vertex of G1 such that
A2: v1.inDegree() = G1.minInDegree() and
for w1 being Vertex of G1 holds v1.inDegree() c= w1.inDegree() by Th37;
consider v2 being Vertex of G2 such that
A3: v2.inDegree() = G2.minInDegree() and
A4: for w2 being Vertex of G2 holds v2.inDegree() c= w2.inDegree() by Th37;
A5: (F_V/.v1).inDegree() c= v1.inDegree() by A1, GLIBPRE0:90;
v2.inDegree() c= (F_V/.v1).inDegree() by A4;
hence G2.minInDegree() c= G1.minInDegree() by A2, A3, A5, XBOOLE_1:1;
consider v3 being Vertex of G1 such that
A6: v3.outDegree() = G1.minOutDegree() and
for w3 being Vertex of G1 holds v3.outDegree() c= w3.outDegree() by Th38;
consider v4 being Vertex of G2 such that
A7: v4.outDegree() = G2.minOutDegree() and
A8: for w4 being Vertex of G2 holds v4.outDegree()c=w4.outDegree() by Th38;
A9: (F_V/.v3).outDegree() c= v3.outDegree() by A1, GLIBPRE0:90;
v4.outDegree() c= (F_V/.v3).outDegree() by A8;
hence G2.minOutDegree() c= G1.minOutDegree() by A6, A7, A9, XBOOLE_1:1;
end;
theorem Th60:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Disomorphism holds
G1.supInDegree() = G2.supInDegree() &
G1.supOutDegree() = G2.supOutDegree() &
G1.minInDegree() = G2.minInDegree() &
G1.minOutDegree() = G2.minOutDegree()
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is Disomorphism;
then A2: dom F_V = the_Vertices_of G1 & rng F_V = the_Vertices_of G2
by GLIB_010:def 11, GLIB_010:def 12;
A3: G1.supInDegree() c= G2.supInDegree() &
G1.supOutDegree() c= G2.supOutDegree() by A1, Th56;
A4: G1.minInDegree() c= G2.minInDegree() &
G1.minOutDegree() c= G2.minOutDegree() by A1, A2, Th57;
A5: G2.supInDegree() c= G1.supInDegree() &
G2.supOutDegree() c= G1.supOutDegree() by A1, Th58;
A6: G2.minInDegree() c= G1.minInDegree() &
G2.minOutDegree() c= G1.minOutDegree() by A1, A2, Th59;
thus thesis by A3, A4, A5, A6, XBOOLE_0:def 10;
end;
theorem
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1.supDegree() = G2.supDegree() & G1.minDegree() = G2.minDegree()
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
set S1 = the set of all v.degree() where v is Vertex of G1;
set S2 = the set of all v.degree() where v is Vertex of G2;
now
let x be object;
hereby
assume x in S1;
then consider v1 being Vertex of G1 such that
A1: x = v1.degree();
reconsider v2 = v1 as Vertex of G2 by GLIB_007:4;
x = v2.degree() by A1, GLIBPRE0:54;
hence x in S2;
end;
assume x in S2;
then consider v2 being Vertex of G2 such that
A2: x = v2.degree();
reconsider v1 = v2 as Vertex of G1 by GLIB_007:4;
x = v1.degree() by A2, GLIBPRE0:54;
hence x in S1;
end;
hence thesis by TARSKI:2;
end;
theorem Th62:
for G1, G2 being _Graph st G1 == G2 holds
G1.supDegree() = G2.supDegree() &
G1.minDegree() = G2.minDegree() &
G1.supInDegree() = G2.supInDegree() &
G1.minInDegree() = G2.minInDegree() &
G1.supOutDegree() = G2.supOutDegree() &
G1.minOutDegree() = G2.minOutDegree()
proof
let G1, G2 be _Graph;
assume A1: G1 == G2;
set S1 = the set of all v.degree() where v is Vertex of G1;
set S2 = the set of all v.degree() where v is Vertex of G2;
now
let x be object;
hereby
assume x in S1;
then consider v1 being Vertex of G1 such that
A2: x = v1.degree();
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = v2.degree() by A1, A2, GLIB_000:96;
hence x in S2;
end;
assume x in S2;
then consider v2 being Vertex of G2 such that
A3: x = v2.degree();
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = v1.degree() by A1, A3, GLIB_000:96;
hence x in S1;
end;
hence G1.supDegree() = G2.supDegree() &
G1.minDegree() = G2.minDegree() by TARSKI:2;
set S3 = the set of all v.inDegree() where v is Vertex of G1;
set S4 = the set of all v.inDegree() where v is Vertex of G2;
now
let x be object;
hereby
assume x in S3;
then consider v1 being Vertex of G1 such that
A4: x = v1.inDegree();
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = v2.inDegree() by A1, A4, GLIB_000:96;
hence x in S4;
end;
assume x in S4;
then consider v2 being Vertex of G2 such that
A5: x = v2.inDegree();
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = v1.inDegree() by A1, A5, GLIB_000:96;
hence x in S3;
end;
hence G1.supInDegree() = G2.supInDegree() &
G1.minInDegree() = G2.minInDegree() by TARSKI:2;
set S5 = the set of all v.outDegree() where v is Vertex of G1;
set S6 = the set of all v.outDegree() where v is Vertex of G2;
now
let x be object;
hereby
assume x in S5;
then consider v1 being Vertex of G1 such that
A6: x = v1.outDegree();
reconsider v2 = v1 as Vertex of G2 by A1, GLIB_000:def 34;
x = v2.outDegree() by A1, A6, GLIB_000:96;
hence x in S6;
end;
assume x in S6;
then consider v2 being Vertex of G2 such that
A7: x = v2.outDegree();
reconsider v1 = v2 as Vertex of G1 by A1, GLIB_000:def 34;
x = v1.outDegree() by A1, A7, GLIB_000:96;
hence x in S5;
end;
hence G1.supOutDegree() = G2.supOutDegree() &
G1.minOutDegree() = G2.minOutDegree() by TARSKI:2;
end;
theorem Th63:
for G1 being _Graph, G2 being Subgraph of G1 holds
G2.supDegree() c= G1.supDegree() &
G2.supInDegree() c= G1.supInDegree() &
G2.supOutDegree() c= G1.supOutDegree()
proof
let G1 be _Graph, G2 be Subgraph of G1;
set F = (id G1) | G2;
F is directed weak_SG-embedding by GLIB_010:57;
hence thesis by Th51, Th56;
end;
theorem
for G1 being _Graph, G2 being spanning Subgraph of G1 holds
G2.minDegree() c= G1.minDegree() &
G2.minInDegree() c= G1.minInDegree() &
G2.minOutDegree() c= G1.minOutDegree()
proof
let G1 be _Graph, G2 be spanning Subgraph of G1;
set F = (id G1) | G2;
A1: F is directed weak_SG-embedding by GLIB_010:57;
rng F_V = rng ((id G1)_V | the_Vertices_of G1) by GLIB_000:def 33
.= the_Vertices_of G1;
hence thesis by A1, Th52, Th57;
end;
theorem
for G2 being _Graph, V being set, G1 being addVertices of G2, V
holds
G1.supDegree() = G2.supDegree() &
G1.supInDegree() = G2.supInDegree() &
G1.supOutDegree() = G2.supOutDegree()
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
G2 is Subgraph of G1 by GLIB_006:57;
then A1: G2.supDegree() c= G1.supDegree() &
G2.supInDegree() c= G1.supInDegree() &
G2.supOutDegree() c= G1.supOutDegree() by Th63;
A2: the_Vertices_of G1 = the_Vertices_of G2 \/ V by GLIB_006:def 10;
set D1 = the set of all v.degree() where v is Vertex of G1;
set D2 = the set of all v.degree() where v is Vertex of G2;
now
let x be object;
assume x in G1.supDegree();
then consider d1 being set such that
A3: x in d1 & d1 in D1 by TARSKI:def 4;
consider v1 being Vertex of G1 such that
A4: d1 = v1.degree() by A3;
not v1 in V \ the_Vertices_of G2 by A3, A4, GLIB_000:157, GLIB_006:88;
then v1 in the_Vertices_of G2 or not v1 in V by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
d1 = v2.degree() & v2.degree() in D2 by A4, GLIBPRE0:45;
hence x in G2.supDegree() by A3, TARSKI:def 4;
end;
then G1.supDegree() c= G2.supDegree() by TARSKI:def 3;
hence G1.supDegree() = G2.supDegree() by A1, XBOOLE_0:def 10;
set D3 = the set of all v.inDegree() where v is Vertex of G1;
set D4 = the set of all v.inDegree() where v is Vertex of G2;
now
let x be object;
assume x in G1.supInDegree();
then consider d1 being set such that
A5: x in d1 & d1 in D3 by TARSKI:def 4;
consider v1 being Vertex of G1 such that
A6: d1 = v1.inDegree() by A5;
v1 is non isolated by A5, A6, GLIB_000:156;
then not v1 in V \ the_Vertices_of G2 by GLIB_006:88;
then v1 in the_Vertices_of G2 or not v1 in V by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
d1 = v2.inDegree() & v2.inDegree() in D4 by A6, GLIBPRE0:45;
hence x in G2.supInDegree() by A5, TARSKI:def 4;
end;
then G1.supInDegree() c= G2.supInDegree() by TARSKI:def 3;
hence G1.supInDegree() = G2.supInDegree() by A1, XBOOLE_0:def 10;
set D5 = the set of all v.outDegree() where v is Vertex of G1;
set D6 = the set of all v.outDegree() where v is Vertex of G2;
now
let x be object;
assume x in G1.supOutDegree();
then consider d1 being set such that
A7: x in d1 & d1 in D5 by TARSKI:def 4;
consider v1 being Vertex of G1 such that
A8: d1 = v1.outDegree() by A7;
v1 is non isolated by A7, A8, GLIB_000:156;
then not v1 in V \ the_Vertices_of G2 by GLIB_006:88;
then v1 in the_Vertices_of G2 or not v1 in V by XBOOLE_0:def 5;
then reconsider v2 = v1 as Vertex of G2 by A2, XBOOLE_0:def 3;
d1 = v2.outDegree() & v2.outDegree() in D6 by A8, GLIBPRE0:45;
hence x in G2.supOutDegree() by A7, TARSKI:def 4;
end;
then G1.supOutDegree() c= G2.supOutDegree() by TARSKI:def 3;
hence G1.supOutDegree() = G2.supOutDegree() by A1, XBOOLE_0:def 10;
end;
theorem
for G2 being _Graph, V being set, G1 being addVertices of G2, V
st V \ the_Vertices_of G2 <> {}
holds G1.minDegree() = 0 & G1.minInDegree() = 0 & G1.minOutDegree() = 0
proof
let G2 be _Graph, V be set, G1 be addVertices of G2, V;
assume V \ the_Vertices_of G2 <> {};
then consider v being object such that
A1: v in V \ the_Vertices_of G2 by XBOOLE_0:def 1;
reconsider v as Vertex of G1 by A1, GLIB_006:86;
v is isolated by A1, GLIB_006:88;
hence thesis by Th46;
end;
registration
let G be non edgeless _Graph;
cluster G.supDegree() -> non empty;
coherence
proof
consider e being object such that
A1: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
reconsider v as Vertex of G by A1, FUNCT_2:5;
e in v.edgesOut() by A1, GLIB_000:58;
then v.outDegree() <> 0 & 0 c= v.outDegree() by XBOOLE_1:2;
then 0 in v.outDegree() by XBOOLE_0:def 8, ORDINAL1:11;
then A2: 0 in v.degree() by CARD_2:94, TARSKI:def 3;
v.degree() in the set of all u.degree() where u is Vertex of G;
then v.degree() c= G.supDegree() by ZFMISC_1:74;
hence thesis by A2;
end;
cluster G.supInDegree() -> non empty;
coherence
proof
consider e being object such that
A3: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
reconsider w as Vertex of G by A3, FUNCT_2:5;
e in w.edgesIn() by A3, GLIB_000:56;
then w.inDegree() <> 0 & 0 c= w.inDegree() by XBOOLE_1:2;
then A4: 0 in w.inDegree() by XBOOLE_0:def 8, ORDINAL1:11;
w.inDegree() in the set of all u.inDegree() where u is Vertex of G;
then w.inDegree() c= G.supInDegree() by ZFMISC_1:74;
hence thesis by A4;
end;
cluster G.supOutDegree() -> non empty;
coherence
proof
consider e being object such that
A5: e in the_Edges_of G by XBOOLE_0:def 1;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
reconsider v as Vertex of G by A5, FUNCT_2:5;
e in v.edgesOut() by A5, GLIB_000:58;
then v.outDegree() <> 0 & 0 c= v.outDegree() by XBOOLE_1:2;
then A6: 0 in v.outDegree() by XBOOLE_0:def 8, ORDINAL1:11;
v.outDegree() in the set of all u.outDegree() where u is Vertex of G;
then v.outDegree() c= G.supOutDegree() by ZFMISC_1:74;
hence thesis by A6;
end;
end;
:: better version
:: non trivial connected or loopfull <=> without_isolated_vertices
:: registration
:: let G be non trivial connected _Graph;
:: cluster G.minDegree() -> non empty;
:: coherence;
:: cluster G.minInDegree() -> non empty;
:: coherence;
:: cluster G.minOutDegree() -> non empty;
:: coherence;
:: end;
::
:: registration
:: let G be loopfull _Graph;
:: cluster G.minDegree() -> non empty;
:: coherence;
:: cluster G.minInDegree() -> non empty;
:: coherence;
:: cluster G.minOutDegree() -> non empty;
:: coherence;
:: end;
registration
let G be locally-finite _Graph;
cluster G.minDegree() -> natural;
coherence
proof
consider v being Vertex of G such that
A1: v.degree() = G.minDegree() and
for w being Vertex of G holds v.degree() c= w.degree() by Th36;
thus thesis by A1;
end;
cluster G.minInDegree() -> natural;
coherence
proof
consider v being Vertex of G such that
A2: v.inDegree() = G.minInDegree() and
for w being Vertex of G holds v.inDegree() c= w.inDegree() by Th37;
thus thesis by A2;
end;
cluster G.minOutDegree() -> natural;
coherence
proof
consider v being Vertex of G such that
A3: v.outDegree() = G.minOutDegree() and
for w being Vertex of G holds v.outDegree() c= w.outDegree() by Th38;
thus thesis by A3;
end;
end;
definition
let G be locally-finite _Graph;
redefine func G.minDegree() -> Nat; :: redefines .minDegree() (GLIB_013, definition)
coherence;
redefine func G.minInDegree() -> Nat; :: redefines .minInDegree() (GLIB_013, definition)
coherence;
redefine func G.minOutDegree() -> Nat; :: redefines .minOutDegree() (GLIB_013, definition)
coherence;
end;
theorem
for G being locally-finite _Graph, n being Nat
holds G.minDegree() = n iff
ex v being Vertex of G st v.degree() = n &
for w being Vertex of G holds v.degree() <= w.degree()
proof
let G be locally-finite _Graph, n be Nat;
hereby
assume G.minDegree() = n;
then consider v being Vertex of G such that
A1: v.degree() = n and
A2: for w being Vertex of G holds v.degree() c= w.degree() by Th36;
take v;
thus v.degree() = n by A1;
let w be Vertex of G;
Segm v.degree() c= Segm w.degree() by A2;
hence v.degree() <= w.degree() by NAT_1:39;
end;
given v being Vertex of G such that
A3: v.degree() = n and
A4: for w being Vertex of G holds v.degree() <= w.degree();
now
let w be Vertex of G;
Segm v.degree() c= Segm w.degree() by A4, NAT_1:39;
hence v.degree() c= w.degree();
end;
hence thesis by A3, Th36;
end;
theorem
for G being locally-finite _Graph, n being Nat
holds G.minInDegree() = n iff
ex v being Vertex of G st v.inDegree() = n &
for w being Vertex of G holds v.inDegree() <= w.inDegree()
proof
let G be locally-finite _Graph, n be Nat;
hereby
assume G.minInDegree() = n;
then consider v being Vertex of G such that
A1: v.inDegree() = n and
A2: for w being Vertex of G holds v.inDegree() c= w.inDegree() by Th37;
take v;
thus v.inDegree() = n by A1;
let w be Vertex of G;
Segm v.inDegree() c= Segm w.inDegree() by A2;
hence v.inDegree() <= w.inDegree() by NAT_1:39;
end;
given v being Vertex of G such that
A3: v.inDegree() = n and
A4: for w being Vertex of G holds v.inDegree() <= w.inDegree();
now
let w be Vertex of G;
Segm v.inDegree() c= Segm w.inDegree() by A4, NAT_1:39;
hence v.inDegree() c= w.inDegree();
end;
hence thesis by A3, Th37;
end;
theorem
for G being locally-finite _Graph, n being Nat
holds G.minOutDegree() = n iff
ex v being Vertex of G st v.outDegree() = n &
for w being Vertex of G holds v.outDegree() <= w.outDegree()
proof
let G be locally-finite _Graph, n be Nat;
hereby
assume G.minOutDegree() = n;
then consider v being Vertex of G such that
A1: v.outDegree() = n and
A2: for w being Vertex of G holds v.outDegree() c= w.outDegree() by Th38;
take v;
thus v.outDegree() = n by A1;
let w be Vertex of G;
Segm v.outDegree() c= Segm w.outDegree() by A2;
hence v.outDegree() <= w.outDegree() by NAT_1:39;
end;
given v being Vertex of G such that
A3: v.outDegree() = n and
A4: for w being Vertex of G holds v.outDegree() <= w.outDegree();
now
let w be Vertex of G;
Segm v.outDegree() c= Segm w.outDegree() by A4, NAT_1:39;
hence v.outDegree() c= w.outDegree();
end;
hence thesis by A3, Th38;
end;
Lm1: for a,b being Cardinal st a c= b & a <> b holds a+`1 c= b
proof
let a, b be Cardinal;
assume A1: a c= b & a <> b;
then a c< b by XBOOLE_0:def 8;
then A2: succ a c= b by ORDINAL1:11, ORDINAL1:21;
per cases;
suppose a is finite;
then reconsider n = a as Nat;
a+`1 = n+`1 .= Segm(n+1)
.= succ Segm n by NAT_1:38 .= succ a;
hence thesis by A2;
end;
suppose A3: a is infinite;
then 1 c= a;
hence thesis by A1, A3, CARD_2:76;
end;
end;
theorem Th70:
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minDegree() = G2.minDegree() or
G1.minDegree() = (v.degree() /\ w.degree()) +` 1
proof
let G2 be _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w;
assume A1: v <> w;
per cases;
suppose A2: not e in the_Edges_of G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:def 11;
then reconsider v9 = v, w9 = w as Vertex of G1;
consider v1 being Vertex of G1 such that
A4: v1.degree() = G1.minDegree() and
A5: for w1 being Vertex of G1 holds v1.degree() c= w1.degree() by Th36;
reconsider v4 = v1 as Vertex of G2 by A3;
consider v2 being Vertex of G2 such that
A6: v2.degree() = G2.minDegree() and
A7: for w2 being Vertex of G2 holds v2.degree() c= w2.degree() by Th36;
reconsider v3 = v2 as Vertex of G1 by A3;
A8: v2.degree() c= v4.degree() & v1.degree() c= v3.degree() by A5, A7;
A9: G2 is Subgraph of G1 by GLIB_006:57;
then A10: v4.inDegree() c= v1.inDegree() & v2.inDegree() c= v3.inDegree()
by GLIB_000:78, CARD_1:11;
v4.outDegree() c= v1.outDegree() & v2.outDegree() c= v3.outDegree()
by A9, GLIB_000:78, CARD_1:11;
then v4.degree() c= v1.degree() & v2.degree() c= v3.degree()
by A10, CARD_2:83;
then A11: v2.degree() c= v1.degree() & v4.degree() c= v3.degree()
by A8, XBOOLE_1:1;
assume G1.minDegree() <> G2.minDegree();
then A12: v1.degree() <> v2.degree() by A4, A6;
then A13: v2.degree() +` 1 c= v1.degree() by A11, Lm1;
A14: v2 = v or v2 = w
proof
assume v2 <> v & v2 <> w;
then A15: v2.degree() = v3.degree() by GLIBPRE0:46;
then A16: v3.degree() +` 1 c= v3.degree() by A8, A13, XBOOLE_1:1;
v3.degree() c= v3.degree() +` 1 by CARD_2:94;
then v3.degree() = v3.degree() +` 1 by A16, XBOOLE_0:def 10;
hence contradiction by A8, A12, A13, A15, XBOOLE_0:def 10;
end;
then v3.degree() = v2.degree() +` 1 by A1, A2, GLIBPRE0:48,47;
then v1.degree() = v2.degree() +` 1 by A8, A13, XBOOLE_0:def 10;
hence thesis by A4, A7, A14, XBOOLE_1:28;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by Th62;
end;
end;
theorem Th71:
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minInDegree() = G2.minInDegree() or
G1.minInDegree() = w.inDegree() +` 1
proof
let G2 be _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w;
assume A1: v <> w;
per cases;
suppose A2: not e in the_Edges_of G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:def 11;
then reconsider v9 = v, w9 = w as Vertex of G1;
consider v1 being Vertex of G1 such that
A4: v1.inDegree() = G1.minInDegree() and
A5: for w1 being Vertex of G1 holds v1.inDegree() c= w1.inDegree()
by Th37;
reconsider v4 = v1 as Vertex of G2 by A3;
consider v2 being Vertex of G2 such that
A6: v2.inDegree() = G2.minInDegree() and
A7: for w2 being Vertex of G2 holds v2.inDegree() c= w2.inDegree()
by Th37;
reconsider v3 = v2 as Vertex of G1 by A3;
A8: v2.inDegree() c= v4.inDegree() & v1.inDegree() c= v3.inDegree()
by A5, A7;
G2 is Subgraph of G1 by GLIB_006:57;
then v4.inDegree() c= v1.inDegree() & v2.inDegree() c= v3.inDegree()
by CARD_1:11, GLIB_000:78;
then A9: v2.inDegree() c= v1.inDegree() & v4.inDegree() c= v3.inDegree()
by A8, XBOOLE_1:1;
assume G1.minInDegree() <> G2.minInDegree();
then A10: v1.inDegree() <> v2.inDegree() by A4, A6;
then A11: v2.inDegree() +` 1 c= v1.inDegree() by A9, Lm1;
A12: v2 = w
proof
assume A13: v2 <> w;
A14: v2.inDegree() = v3.inDegree()
proof
per cases;
suppose v2 = v;
hence thesis by A1, A2, GLIBPRE0:47;
end;
suppose v2 <> v;
hence thesis by A13, GLIBPRE0:46;
end;
end;
then A15: v3.inDegree() +` 1 c= v3.inDegree() by A8, A11, XBOOLE_1:1;
v3.inDegree() c= v3.inDegree() +` 1 by CARD_2:94;
then v3.inDegree() = v3.inDegree() +` 1 by A15, XBOOLE_0:def 10;
hence contradiction by A8, A10, A11, A14, XBOOLE_0:def 10;
end;
then v3.inDegree() = v2.inDegree() +` 1 by A1, A2, GLIBPRE0:48;
hence thesis by A4, A8, A11, A12, XBOOLE_0:def 10;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by Th62;
end;
end;
theorem Th72:
for G2 being _Graph, v,w being Vertex of G2, e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minOutDegree() = G2.minOutDegree() or
G1.minOutDegree() = v.outDegree() +` 1
proof
let G2 be _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w;
assume A1: v <> w;
per cases;
suppose A2: not e in the_Edges_of G2;
then A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:def 11;
then reconsider v9 = v, w9 = w as Vertex of G1;
consider v1 being Vertex of G1 such that
A4: v1.outDegree() = G1.minOutDegree() and
A5: for w1 being Vertex of G1 holds v1.outDegree() c= w1.outDegree()
by Th38;
reconsider v4 = v1 as Vertex of G2 by A3;
consider v2 being Vertex of G2 such that
A6: v2.outDegree() = G2.minOutDegree() and
A7: for w2 being Vertex of G2 holds v2.outDegree() c= w2.outDegree()
by Th38;
reconsider v3 = v2 as Vertex of G1 by A3;
A8: v2.outDegree() c= v4.outDegree() & v1.outDegree() c= v3.outDegree()
by A5, A7;
G2 is Subgraph of G1 by GLIB_006:57;
then v4.outDegree() c= v1.outDegree() & v2.outDegree()c= v3.outDegree()
by CARD_1:11, GLIB_000:78;
then A9: v2.outDegree() c= v1.outDegree() & v4.outDegree()c= v3.outDegree()
by A8, XBOOLE_1:1;
assume G1.minOutDegree() <> G2.minOutDegree();
then A10: v1.outDegree() <> v2.outDegree() by A4, A6;
then A11: v2.outDegree() +` 1 c= v1.outDegree() by A9, Lm1;
A12: v2 = v
proof
assume A13: v2 <> v;
A14: v2.outDegree() = v3.outDegree()
proof
per cases;
suppose v2 = w;
hence thesis by A1, A2, GLIBPRE0:48;
end;
suppose v2 <> w;
hence thesis by A13, GLIBPRE0:46;
end;
end;
then A15: v3.outDegree() +` 1 c= v3.outDegree() by A8, A11, XBOOLE_1:1;
v3.outDegree() c= v3.outDegree() +` 1 by CARD_2:94;
then v3.outDegree() = v3.outDegree() +` 1 by A15, XBOOLE_0:def 10;
hence contradiction by A8, A10, A11, A14, XBOOLE_0:def 10;
end;
then v3.outDegree() = v2.outDegree() +` 1 by A1, A2, GLIBPRE0:47;
hence thesis by A4, A8, A11, A12, XBOOLE_0:def 10;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by Th62;
end;
end;
theorem
for G2 being locally-finite _Graph, v,w being Vertex of G2,e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minDegree() = G2.minDegree() or
G1.minDegree() = min(v.degree(),w.degree()) + 1
proof
let G2 be locally-finite _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w;
min(v.degree(),w.degree()) + 1 = (v.degree() /\ w.degree()) +` 1;
hence thesis by Th70;
end;
theorem
for G2 being locally-finite _Graph, v,w being Vertex of G2,e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minInDegree() = G2.minInDegree() or
G1.minInDegree() = w.inDegree() + 1
proof
let G2 be locally-finite _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w;
w.inDegree() +` 1 = w.inDegree() +` 1;
hence thesis by Th71;
end;
theorem
for G2 being locally-finite _Graph, v,w being Vertex of G2,e being object
for G1 being addEdge of G2,v,e,w st v <> w holds
G1.minOutDegree() = G2.minOutDegree() or
G1.minOutDegree() = v.outDegree() + 1
proof
let G2 be locally-finite _Graph, v,w be Vertex of G2, e be object;
let G1 be addEdge of G2,v,e,w;
v.outDegree() +` 1 = v.outDegree() +` 1;
hence thesis by Th72;
end;
:: :: better in combination with_isolated_vertices
:: theorem
:: 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.minDegree() = {1} /\ G2.minDegree();
::
:: theorem
:: 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.minDegree() = {1} /\ G2.minDegree();
::
:: theorem
:: for G2 being locally-finite _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.minDegree() = min(1,G2.minDegree());
::
:: theorem
:: for G2 being locally-finite _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.minDegree() = min(1,G2.minDegree());
theorem Th76:
for G2 being _Graph, v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2
holds G1.minDegree() = (G2.minDegree() +` 1) /\ G2.order()
proof
let G2 be _Graph, v be object;
let G1 be addAdjVertexAll of G2, v;
assume A1: not v in the_Vertices_of G2;
then reconsider v9 = v as Vertex of G1 by GLIB_007:50;
consider v0 being Vertex of G2 such that
A2: G2.minDegree() = v0.degree() and
A3: for w0 being Vertex of G2 holds v0.degree() c= w0.degree() by Th36;
A4: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A1, GLIB_007:def 4;
then reconsider v1 = v0 as Vertex of G1 by XBOOLE_0:def 3;
A5: the_Vertices_of G2 c= the_Vertices_of G2;
A6: v9.degree() = G2.order() by A1, GLIBPRE0:55;
A7: v1.degree() = v0.degree() +` 1 by A1, A5, GLIBPRE0:57;
per cases;
suppose A8: v0.degree() +` 1 c= v9.degree();
then A9: (G2.minDegree() +` 1) /\ G2.order() = v0.degree() +` 1
by A2, A6, XBOOLE_1:28;
now
let w be Vertex of G1;
per cases by A4, XBOOLE_0:def 3;
suppose w in the_Vertices_of G2;
then reconsider w0 = w as Vertex of G2;
v0.degree() c= w0.degree() & 1 c= 1 by A3;
then v1.degree() c= w0.degree() +` 1 by A7, CARD_2:83;
hence v1.degree() c= w.degree() by A1, A5, GLIBPRE0:57;
end;
suppose w in {v};
hence v1.degree() c= w.degree() by A7, A8, TARSKI:def 1;
end;
end;
hence thesis by A7, A9, Th36;
end;
suppose A10: v9.degree() c= v0.degree() +` 1;
then A11: (G2.minDegree() +` 1) /\ G2.order() = v9.degree()
by A2, A6, XBOOLE_1:28;
now
let w be Vertex of G1;
per cases by A4, XBOOLE_0:def 3;
suppose w in the_Vertices_of G2;
then reconsider w0 = w as Vertex of G2;
v0.degree() c= w0.degree() & 1 c= 1 by A3;
then v0.degree() +` 1 c= w0.degree() +` 1 by CARD_2:83;
then v9.degree() c= w0.degree() +` 1 by A10, XBOOLE_1:1;
hence v9.degree() c= w.degree() by A1, A5, GLIBPRE0:57;
end;
suppose w in {v};
hence v9.degree() c= w.degree() by TARSKI:def 1;
end;
end;
hence thesis by A11, Th36;
end;
end;
theorem
for G2 being _finite _Graph, v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2
holds G1.minDegree() = min(G2.minDegree() + 1, G2.order())
proof
let G2 be _finite _Graph, v be object;
let G1 be addAdjVertexAll of G2, v;
min(G2.minDegree() + 1, G2.order()) = (G2.minDegree() +` 1) /\ G2.order();
hence thesis by Th76;
end;
Lm2:
for a,b,c being Cardinal st c c= a & c c= b & a in c +` 2 & not a c= b
holds b = c
proof
let a,b,c be Cardinal;
assume A1: c c= a & c c= b & a in c +` 2 & not a c= b;
A2: a is finite
proof
assume A3: a is infinite;
a c= c +` 2 by A1, ORDINAL1:def 2;
then A4: c is infinite by A3;
then 2 c= c;
then c +` 2 = c by A4, CARD_2:76;
then a in a by A1;
hence contradiction;
end;
then reconsider k = a as Nat;
reconsider n = c as Nat by A1, A2;
A5: b in a by A1, ORDINAL1:16;
then b c= a by ORDINAL1:def 2;
then reconsider m = b as Nat by A2;
Segm c c= Segm b by A1;
then A6: n <= m by NAT_1:39;
a in Segm(n+`2) by A1;
then A7: k < n+2 by NAT_1:44;
b in Segm a by A5;
then m < k by NAT_1:44;
then A8: m+1 <= k by NAT_1:13;
k < (n+1)+1 by A7;
then k <= n+1 by NAT_1:13;
then m+1 <= n+1 by A8, XXREAL_0:2;
then m <= n by XREAL_1:6;
hence thesis by A6, XXREAL_0:1;
end;
theorem
for G2 being _Graph, V being set, G1 being addLoops of G2, V
holds G1.minDegree() c= G2.minDegree() +` 2
proof
let G2 be _Graph, V be set, G1 be addLoops of G2, V;
per cases;
suppose A1: V c= the_Vertices_of G2;
consider v2 being Vertex of G2 such that
A2: G2.minDegree() = v2.degree() and
A3: for w2 being Vertex of G2 holds v2.degree() c= w2.degree() by Th36;
A4: the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_012:def 5;
then reconsider v1 = v2 as Vertex of G1;
per cases;
suppose not v2 in V;
then A5: v1.degree() = v2.degree() by A1, GLIB_012:44;
now
let w1 be Vertex of G1;
reconsider w2 = w1 as Vertex of G2 by A4;
per cases;
suppose w1 in V;
then A6: w1.degree() = w2.degree() +` 2 by A1, GLIB_012:43;
A7: v1.degree() c= w2.degree() by A3, A5;
w2.degree() c= w1.degree() by A6, CARD_2:94;
hence v1.degree() c= w1.degree() by A7, XBOOLE_1:1;
end;
suppose not w1 in V;
then w1.degree() = w2.degree() by A1, GLIB_012:44;
hence v1.degree() c= w1.degree() by A3, A5;
end;
end;
then G1.minDegree() = v1.degree() by Th36;
hence thesis by A2, A5, CARD_2:94;
end;
suppose A8: v2 in V & for w2 being Vertex of G2 st not w2 in V
holds v2.degree() +` 2 c= w2.degree();
then A9: v1.degree() = v2.degree() +` 2 by A1, GLIB_012:43;
now
let w1 be Vertex of G1;
reconsider w2 = w1 as Vertex of G2 by A4;
per cases;
suppose w1 in V;
then A10: w1.degree() = w2.degree() +` 2 by A1, GLIB_012:43;
v2.degree() c= w2.degree() & 2 c= 2 by A3;
hence v1.degree() c= w1.degree() by A9, A10, CARD_2:83;
end;
suppose A11: not w1 in V;
then w1.degree() = w2.degree() by A1, GLIB_012:44;
hence v1.degree() c= w1.degree() by A8, A9, A11;
end;
end;
hence thesis by A2, A9, Th36;
end;
suppose v2 in V & ex w2 being Vertex of G2 st not w2 in V
& not v2.degree() +` 2 c= w2.degree();
then consider w2 being Vertex of G2 such that
A12: not w2 in V & not v2.degree() +` 2 c= w2.degree();
A13: w2.degree() in v2.degree() +` 2 by A12, ORDINAL1:16;
reconsider w1 = w2 as Vertex of G1 by A4;
A14: w1.degree() = w2.degree() by A1, A12, GLIB_012:44;
per cases;
suppose A15: for u2 being Vertex of G2 holds not u2 in V implies
w2.degree() c= u2.degree();
now
let u1 be Vertex of G1;
reconsider u2 = u1 as Vertex of G2 by A4;
per cases;
suppose u1 in V;
then A16: u1.degree() = u2.degree() +` 2 by A1, GLIB_012:43;
v2.degree() c= u2.degree() & 2 c= 2 by A3;
then v2.degree() +` 2 c= u2.degree() +` 2 by CARD_2:83;
hence w1.degree() c= u1.degree() by A13, A14, A16, ORDINAL1:def 2;
end;
suppose not u1 in V;
then u1.degree() = u2.degree() & w2.degree() c= u2.degree()
by A1, A15, GLIB_012:44;
hence w1.degree() c= u1.degree() by A14;
end;
end;
then G1.minDegree() = w1.degree() by Th36;
hence thesis by A2, A13, A14, ORDINAL1:def 2;
end;
suppose ex u2 being Vertex of G2 st not u2 in V &
not w2.degree() c= u2.degree();
then consider u2 being Vertex of G2 such that
A17: not u2 in V & not w2.degree() c= u2.degree();
v2.degree() c= w2.degree() & v2.degree() c= u2.degree() by A3;
then A18: u2.degree() = v2.degree() by A13, A17, Lm2;
reconsider u1 = u2 as Vertex of G1 by A4;
A19: u1.degree() = u2.degree() by A1, A17, GLIB_012:44;
now
let x1 be Vertex of G1;
reconsider x2 = x1 as Vertex of G2 by A4;
A20: u1.degree() c= x2.degree() by A3, A18, A19;
per cases;
suppose x1 in V;
then x1.degree() = x2.degree() +` 2 by A1, GLIB_012:43;
then x2.degree() c= x1.degree() by CARD_2:94;
hence u1.degree() c= x1.degree() by A20, XBOOLE_1:1;
end;
suppose not x1 in V;
hence u1.degree() c= x1.degree() by A1, A20, GLIB_012:44;
end;
end;
then A21: G1.minDegree() = u1.degree() by Th36;
u1.degree() in w2.degree() by A17, A19, ORDINAL1:16;
hence thesis by A2, A13, A21;
end;
end;
end;
suppose not(V c= the_Vertices_of G2);
then G1 == G2 by GLIB_012:def 5;
then G1.minDegree() = G2.minDegree() by Th62;
hence thesis by CARD_2:94;
end;
end;
registration
let G be edge-finite _Graph;
cluster G.supDegree() -> natural;
coherence
proof
now
let d be set;
assume d in the set of all v.degree() where v is Vertex of G;
then consider v being Vertex of G such that
A1: d = v.degree();
card v.edgesIn() c= card the_Edges_of G &
card v.edgesOut() c= card the_Edges_of G by CARD_1:11;
hence d c= G.size() +` G.size() by A1, CARD_2:83;
end;
then G.supDegree() c= G.size() +` G.size() by ZFMISC_1:76;
hence thesis;
end;
cluster G.supInDegree() -> natural;
coherence
proof
now
let d be set;
assume d in the set of all v.inDegree() where v is Vertex of G;
then consider v being Vertex of G such that
A2: d = v.inDegree();
thus d c= G.size() by A2, CARD_1:11;
end;
then G.supInDegree() c= G.size() by ZFMISC_1:76;
hence thesis;
end;
cluster G.supOutDegree() -> natural;
coherence
proof
now
let d be set;
assume d in the set of all v.outDegree() where v is Vertex of G;
then consider v being Vertex of G such that
A3: d = v.outDegree();
thus d c= G.size() by A3, CARD_1:11;
end;
then G.supOutDegree() c= G.size() by ZFMISC_1:76;
hence thesis;
end;
end;
definition
let G be edge-finite _Graph;
redefine func G.supDegree() -> Nat; :: redefines .supDegree() (GLIB_013, definition)
coherence;
redefine func G.supInDegree() -> Nat; :: redefines .supInDegree() (GLIB_013, definition)
coherence;
redefine func G.supOutDegree() -> Nat; :: redefines .supOutDegree() (GLIB_013, definition)
coherence;
end;
definition
let G be _Graph;
attr G is with_max_degree means
:Def12:
ex v being Vertex of G
st for w being Vertex of G holds w.degree() c= v.degree();
attr G is with_max_in_degree means
:Def13:
ex v being Vertex of G
st for w being Vertex of G holds w.inDegree() c= v.inDegree();
attr G is with_max_out_degree means
:Def14:
ex v being Vertex of G
st for w being Vertex of G holds w.outDegree() c= v.outDegree();
end;
theorem Th79:
for G being _Graph st G is with_max_degree
holds ex v being Vertex of G st v.degree() = G.supDegree() &
for w being Vertex of G holds w.degree() c= v.degree()
proof
let G be _Graph;
assume G is with_max_degree;
then consider v being Vertex of G such that
A1: for w being Vertex of G holds w.degree() c= v.degree();
take v;
set D = the set of all w.degree() where w is Vertex of G;
now
let X be set;
assume X in D;
then consider w being Vertex of G such that
A2: X = w.degree();
thus X c= v.degree() by A1, A2;
end;
then A3: union D c= v.degree() by ZFMISC_1:76;
v.degree() c= G.supDegree() by Th35;
hence thesis by A1, A3, XBOOLE_0:def 10;
end;
theorem Th80:
for G being _Graph st G is with_max_in_degree
holds ex v being Vertex of G st v.inDegree() = G.supInDegree() &
for w being Vertex of G holds w.inDegree() c= v.inDegree()
proof
let G be _Graph;
assume G is with_max_in_degree;
then consider v being Vertex of G such that
A1: for w being Vertex of G holds w.inDegree() c= v.inDegree();
take v;
set D = the set of all w.inDegree() where w is Vertex of G;
now
let X be set;
assume X in D;
then consider w being Vertex of G such that
A2: X = w.inDegree();
thus X c= v.inDegree() by A1, A2;
end;
then A3: union D c= v.inDegree() by ZFMISC_1:76;
v.inDegree() c= G.supInDegree() by Th35;
hence thesis by A1, A3, XBOOLE_0:def 10;
end;
theorem Th81:
for G being _Graph st G is with_max_out_degree
holds ex v being Vertex of G st v.outDegree() = G.supOutDegree() &
for w being Vertex of G holds w.outDegree() c= v.outDegree()
proof
let G be _Graph;
assume G is with_max_out_degree;
then consider v being Vertex of G such that
A1: for w being Vertex of G holds w.outDegree() c= v.outDegree();
take v;
set D = the set of all w.outDegree() where w is Vertex of G;
now
let X be set;
assume X in D;
then consider w being Vertex of G such that
A2: X = w.outDegree();
thus X c= v.outDegree() by A1, A2;
end;
then A3: union D c= v.outDegree() by ZFMISC_1:76;
v.outDegree() c= G.supOutDegree() by Th35;
hence thesis by A1, A3, XBOOLE_0:def 10;
end;
Lm3:
for G being _Graph
st ex v being Vertex of G st v.degree() = G.supDegree()
holds G is with_max_degree
proof
let G be _Graph;
given v being Vertex of G such that
A1: v.degree() = G.supDegree();
for w being Vertex of G holds w.degree() c= v.degree() by A1, Th35;
hence thesis;
end;
Lm4:
for G being _Graph
st ex v being Vertex of G st v.inDegree() = G.supInDegree()
holds G is with_max_in_degree
proof
let G be _Graph;
given v being Vertex of G such that
A1: v.inDegree() = G.supInDegree();
for w being Vertex of G holds w.inDegree() c= v.inDegree() by A1, Th35;
hence thesis;
end;
Lm5:
for G being _Graph
st ex v being Vertex of G st v.outDegree() = G.supOutDegree()
holds G is with_max_out_degree
proof
let G be _Graph;
given v being Vertex of G such that
A1: v.outDegree() = G.supOutDegree();
for w being Vertex of G holds w.outDegree() c= v.outDegree() by A1, Th35;
hence thesis;
end;
notation
let G be _Graph;
antonym G is without_max_degree for G is with_max_degree;
antonym G is without_max_in_degree for G is with_max_in_degree;
antonym G is without_max_out_degree for G is with_max_out_degree;
end;
registration
cluster with_max_in_degree with_max_out_degree -> with_max_degree
for _Graph;
coherence
proof
let G be _Graph;
assume G is with_max_in_degree;
then consider v being Vertex of G such that
A1: v.inDegree() = G.supInDegree() and
A2: for u being Vertex of G holds u.inDegree() c= v.inDegree()
by Th80;
assume G is with_max_out_degree;
then consider w being Vertex of G such that
A3: w.outDegree() = G.supOutDegree() and
A4: for u being Vertex of G holds u.outDegree() c= w.outDegree()
by Th81;
set c = G.supInDegree(), d = G.supOutDegree();
per cases;
suppose A5: d is infinite & c c= d;
w.inDegree() c= c by A1, A2;
then w.inDegree() +` w.outDegree() c= c +` w.outDegree() by CARD_2:83;
then A6: w.degree() c= d by A3, A5, CARD_2:76;
d c= w.degree() by A3, CARD_2:94;
then A7: w.degree() = d by A6, XBOOLE_0:def 10;
now
let u be Vertex of G;
u.inDegree() c= v.inDegree() by A2;
then A8: u.inDegree() c= d by A1, A5, XBOOLE_1:1;
u.outDegree() c= d by A3, A4;
then u.degree() c= d +` d by A8, CARD_2:83;
hence u.degree() c= w.degree() by A5, A7, CARD_2:75;
end;
hence thesis;
end;
suppose A9: c is infinite & d c= c;
v.outDegree() c= d by A3, A4;
then v.inDegree() +` v.outDegree() c= d +` v.inDegree() by CARD_2:83;
then A10: v.degree() c= c by A1, A9, CARD_2:76;
c c= v.degree() by A1, CARD_2:94;
then A11: v.degree() = c by A10, XBOOLE_0:def 10;
now
let u be Vertex of G;
A12: u.inDegree() c= v.inDegree() by A2;
u.outDegree() c= d by A3, A4;
then u.outDegree() c= c by A9, XBOOLE_1:1;
then u.degree() c= c +` c by A1, A12, CARD_2:83;
hence u.degree() c= v.degree() by A9, A11, CARD_2:75;
end;
hence thesis;
end;
suppose c is finite & d is finite;
then reconsider c, d as Nat;
defpred P[Nat] means ex u being Vertex of G st u.degree() = $1;
A13: for k being Nat st P[k] holds k <= c+d
proof
let k be Nat;
given u being Vertex of G such that
A14: u.degree() = k;
u.inDegree() c= c & u.outDegree() c= d by A1, A2, A3, A4;
then u.degree() c= c +` d by CARD_2:83;
then Segm u.degree() c= Segm(c+d);
hence thesis by A14, NAT_1:39;
end;
A15: ex k being Nat st P[k]
proof
w.inDegree() c= c by A1, A2;
then reconsider e = w.inDegree() as Nat;
take e+d, w;
thus w.degree() = e +` d by A3
.= e + d;
end;
consider k being Nat such that
A16: P[k] & for n being Nat st P[n] holds n <= k
from NAT_1:sch 6(A13,A15);
consider u being Vertex of G such that
A17: u.degree() = k by A16;
now
let u9 be Vertex of G;
u9.inDegree() c= c & u9.outDegree() c= d by A1, A2, A3, A4;
then reconsider n = u9.degree() as Nat;
Segm n c= Segm k by A16, NAT_1:39;
hence u9.degree() c= u.degree() by A17;
end;
hence thesis;
end;
end;
cluster vertex-finite -> with_max_degree with_max_in_degree
with_max_out_degree for _Graph;
coherence
proof
let G be _Graph;
assume A18: G is vertex-finite;
thus G is with_max_degree
proof
set D = the set of all v.degree() where v is Vertex of G;
deffunc F(object) = In($1, the_Vertices_of G).degree();
consider f being Function such that
A19: dom f = the_Vertices_of G and
A20: for x being object st x in the_Vertices_of G holds f.x = F(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A21: x in dom f & f.x = y by FUNCT_1:def 3;
reconsider v = x as Vertex of G by A19, A21;
y = In(x, the_Vertices_of G).degree() by A19, A20, A21
.= v.degree() by SUBSET_1:def 8;
hence y in D;
end;
assume y in D;
then consider v being Vertex of G such that
A22: y = v.degree();
y = In(v,the_Vertices_of G).degree() by A22, SUBSET_1:def 8
.= f.v by A20;
hence y in rng f by A19, FUNCT_1:3;
end;
then rng f = D by TARSKI:2;
then A23: D is finite by A18, A19, FINSET_1:8;
now
let x,y be set;
assume A24: x in D & y in D;
then consider v being Vertex of G such that
A25: x = v.degree();
consider w being Vertex of G such that
A26: y = w.degree() by A24;
thus x,y are_c=-comparable by A25, A26, ORDINAL1:15;
end;
then A27: D is finite c=-linear by A23, ORDINAL1:def 8;
then A28: InclPoset D is connected transitive;
set B = [#]InclPoset D;
(the Vertex of G).degree() in D;
then A29: B is non empty finite by A27;
then consider x being Element of InclPoset D such that
x in B and
A30: for y being Element of InclPoset D st y in B & x <> y holds y <= x
by A28, ORDERS_5:25;
A31: x in D by A29;
then consider v being Vertex of G such that
A32: x = v.degree();
now
let w be Vertex of G;
w.degree() in the carrier of InclPoset D;
then reconsider y = w.degree() as Element of InclPoset D;
per cases;
suppose A33: x <> y;
y in B;
then [y,x] in RelIncl D by A30, A33, ORDERS_2:def 5;
hence w.degree() c= v.degree() by A31, A32, WELLORD2:def 1;
end;
suppose x = y;
hence w.degree() c= v.degree() by A32;
end;
end;
hence G is with_max_degree;
end;
thus G is with_max_in_degree
proof
set D = the set of all v.inDegree() where v is Vertex of G;
deffunc F(object) = In($1, the_Vertices_of G).inDegree();
consider f being Function such that
A34: dom f = the_Vertices_of G and
A35: for x being object st x in the_Vertices_of G holds f.x = F(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A36: x in dom f & f.x = y by FUNCT_1:def 3;
reconsider v = x as Vertex of G by A34, A36;
y = In(x, the_Vertices_of G).inDegree() by A34, A35, A36
.= v.inDegree() by SUBSET_1:def 8;
hence y in D;
end;
assume y in D;
then consider v being Vertex of G such that
A37: y = v.inDegree();
y = In(v,the_Vertices_of G).inDegree() by A37, SUBSET_1:def 8
.= f.v by A35;
hence y in rng f by A34, FUNCT_1:3;
end;
then rng f = D by TARSKI:2;
then A38: D is finite by A18, A34, FINSET_1:8;
now
let x,y be set;
assume A39: x in D & y in D;
then consider v being Vertex of G such that
A40: x = v.inDegree();
consider w being Vertex of G such that
A41: y = w.inDegree() by A39;
thus x,y are_c=-comparable by A40, A41, ORDINAL1:15;
end;
then A42: D is finite c=-linear by A38, ORDINAL1:def 8;
then A43: InclPoset D is connected transitive;
set B = [#]InclPoset D;
(the Vertex of G).inDegree() in D;
then A44: B is non empty finite by A42;
then consider x being Element of InclPoset D such that
x in B and
A45: for y being Element of InclPoset D st y in B & x <> y holds y <= x
by A43, ORDERS_5:25;
A46: x in D by A44;
then consider v being Vertex of G such that
A47: x = v.inDegree();
now
let w be Vertex of G;
w.inDegree() in the carrier of InclPoset D;
then reconsider y = w.inDegree() as Element of InclPoset D;
per cases;
suppose A48: x <> y;
y in B;
then [y,x] in RelIncl D by A45, A48, ORDERS_2:def 5;
hence w.inDegree() c= v.inDegree() by A46, A47, WELLORD2:def 1;
end;
suppose x = y;
hence w.inDegree() c= v.inDegree() by A47;
end;
end;
hence G is with_max_in_degree;
end;
thus G is with_max_out_degree
proof
set D = the set of all v.outDegree() where v is Vertex of G;
deffunc F(object) = In($1, the_Vertices_of G).outDegree();
consider f being Function such that
A49: dom f = the_Vertices_of G and
A50: for x being object st x in the_Vertices_of G holds f.x = F(x)
from FUNCT_1:sch 3;
now
let y be object;
hereby
assume y in rng f;
then consider x being object such that
A51: x in dom f & f.x = y by FUNCT_1:def 3;
reconsider v = x as Vertex of G by A49, A51;
y = In(x, the_Vertices_of G).outDegree() by A49, A50, A51
.= v.outDegree() by SUBSET_1:def 8;
hence y in D;
end;
assume y in D;
then consider v being Vertex of G such that
A52: y = v.outDegree();
y = In(v,the_Vertices_of G).outDegree() by A52, SUBSET_1:def 8
.= f.v by A50;
hence y in rng f by A49, FUNCT_1:3;
end;
then rng f = D by TARSKI:2;
then A53: D is finite by A18, A49, FINSET_1:8;
now
let x,y be set;
assume A54: x in D & y in D;
then consider v being Vertex of G such that
A55: x = v.outDegree();
consider w being Vertex of G such that
A56: y = w.outDegree() by A54;
thus x,y are_c=-comparable by A55, A56, ORDINAL1:15;
end;
then A57: D is finite c=-linear by A53, ORDINAL1:def 8;
then A58: InclPoset D is connected transitive;
set B = [#]InclPoset D;
(the Vertex of G).outDegree() in D;
then A59: B is non empty finite by A57;
then consider x being Element of InclPoset D such that
x in B and
A60: for y being Element of InclPoset D st y in B & x <> y holds y <= x
by A58, ORDERS_5:25;
A61: x in D by A59;
then consider v being Vertex of G such that
A62: x = v.outDegree();
now
let w be Vertex of G;
w.outDegree() in the carrier of InclPoset D;
then reconsider y = w.outDegree() as Element of InclPoset D;
per cases;
suppose A63: x <> y;
y in B;
then [y,x] in RelIncl D by A60, A63, ORDERS_2:def 5;
hence w.outDegree() c= v.outDegree() by A61, A62, WELLORD2:def 1;
end;
suppose x = y;
hence w.outDegree() c= v.outDegree() by A62;
end;
end;
hence G is with_max_out_degree;
end;
end;
cluster edge-finite -> with_max_degree with_max_in_degree
with_max_out_degree for _Graph;
coherence
proof
let G be _Graph;
assume A64: G is edge-finite;
then reconsider m = G.size() as Nat;
now
defpred P[Nat] means ex u being Vertex of G st u.degree() = $1;
A65: for k being Nat st P[k] holds k <= 2*m
proof
let k be Nat;
given u being Vertex of G such that
A66: u.degree() = k;
u.inDegree() c= G.size() & u.outDegree() c= G.size() by CARD_1:11;
then Segm u.degree() c= m+`m by CARD_2:83;
then Segm u.degree() c= Segm(2*m);
hence thesis by A66, NAT_1:39;
end;
A67: ex k being Nat st P[k]
proof
set v = the Vertex of G;
reconsider d = v.degree() as Nat by A64;
take d, v;
thus thesis;
end;
consider k being Nat such that
A68: P[k] & for n being Nat st P[n] holds n <= k
from NAT_1:sch 6(A65,A67);
consider u being Vertex of G such that
A69: u.degree() = k by A68;
take u;
let w be Vertex of G;
reconsider d = w.degree() as Nat by A64;
Segm d c= Segm k by A68, NAT_1:39;
hence w.degree() c= u.degree() by A69;
end;
hence G is with_max_degree;
now
defpred P[Nat] means ex u being Vertex of G st u.inDegree() = $1;
A70: for k being Nat st P[k] holds k <= m
proof
let k be Nat;
given u being Vertex of G such that
A71: u.inDegree() = k;
Segm u.inDegree() c= Segm(m) by CARD_1:11;
hence thesis by A71, NAT_1:39;
end;
A72: ex k being Nat st P[k]
proof
set v = the Vertex of G;
reconsider d = v.inDegree() as Nat by A64;
take d, v;
thus thesis;
end;
consider k being Nat such that
A73: P[k] & for n being Nat st P[n] holds n <= k
from NAT_1:sch 6(A70,A72);
consider u being Vertex of G such that
A74: u.inDegree() = k by A73;
take u;
let w be Vertex of G;
reconsider d = w.inDegree() as Nat by A64;
Segm d c= Segm k by A73, NAT_1:39;
hence w.inDegree() c= u.inDegree() by A74;
end;
hence G is with_max_in_degree;
now
defpred P[Nat] means ex u being Vertex of G st u.outDegree() = $1;
A75: for k being Nat st P[k] holds k <= m
proof
let k be Nat;
given u being Vertex of G such that
A76: u.outDegree() = k;
Segm u.outDegree() c= Segm(m) by CARD_1:11;
hence thesis by A76, NAT_1:39;
end;
A77: ex k being Nat st P[k]
proof
set v = the Vertex of G;
reconsider d = v.outDegree() as Nat by A64;
take d, v;
thus thesis;
end;
consider k being Nat such that
A78: P[k] & for n being Nat st P[n] holds n <= k
from NAT_1:sch 6(A75,A77);
consider u being Vertex of G such that
A79: u.outDegree() = k by A78;
take u;
let w be Vertex of G;
reconsider d = w.outDegree() as Nat by A64;
Segm d c= Segm k by A78, NAT_1:39;
hence w.outDegree() c= u.outDegree() by A79;
end;
hence G is with_max_out_degree;
end;
:: will be clustered after construction of graphs by relations is formalized
::cluster without_max_degree without_max_in_degree
:: without_max_out_degree for _Graph;
::existence;
end;
theorem
for G being with_max_degree _Graph
holds G is with_max_in_degree or G is with_max_out_degree
proof
let G be with_max_degree _Graph;
consider v being Vertex of G such that
A1: v.degree() = G.supDegree() and
for w being Vertex of G holds w.degree() c= v.degree() by Th79;
set a = v.inDegree(), b = v.outDegree();
per cases;
suppose a c= b & b is infinite;
then v.degree() = b by CARD_2:76;
then A2: G.supOutDegree() c= v.outDegree() by A1, Th40;
v.outDegree() c= G.supOutDegree() by Th35;
hence thesis by A2, Lm5, XBOOLE_0:def 10;
end;
suppose b c= a & a is infinite;
then v.degree() = a by CARD_2:76;
then A3: G.supInDegree() c= v.inDegree() by A1, Th39;
v.inDegree() c= G.supInDegree() by Th35;
hence thesis by A3, Lm4, XBOOLE_0:def 10;
end;
suppose a is finite & b is finite;
then reconsider a, b as Nat;
now
defpred P[Nat] means ex u being Vertex of G st u.inDegree() = $1;
A4: for k being Nat st P[k] holds k <= a+b
proof
let k be Nat;
given u being Vertex of G such that
A5: u.inDegree() = k;
A6: u.inDegree() c= G.supInDegree() by Th35;
G.supInDegree() c= G.supDegree() by Th39;
then Segm u.inDegree() c= Segm(a+`b) by A1, A6, XBOOLE_1:1;
hence thesis by A5, NAT_1:39;
end;
A7: ex k being Nat st P[k]
proof
take a, v;
thus thesis;
end;
consider k being Nat such that
A8: P[k] & for n being Nat st P[n] holds n <= k
from NAT_1:sch 6(A4,A7);
consider u being Vertex of G such that
A9: u.inDegree() = k by A8;
take u;
let w be Vertex of G;
A10: w.inDegree() c= G.supInDegree() by Th35;
G.supInDegree() c= G.supDegree() by Th39;
then w.inDegree() c= a+`b by A1, A10, XBOOLE_1:1;
then reconsider d = w.inDegree() as Nat;
Segm d c= Segm k by A8, NAT_1:39;
hence w.inDegree() c= u.inDegree() by A9;
end;
hence thesis;
end;
end;
notation
let G be with_max_degree _Graph;
synonym G.maxDegree() for G.supDegree();
end;
notation
let G be with_max_in_degree _Graph;
synonym G.maxInDegree() for G.supInDegree();
end;
notation
let G be with_max_out_degree _Graph;
synonym G.maxOutDegree() for G.supOutDegree();
end;
registration
let G be locally-finite with_max_degree _Graph;
cluster G.maxDegree() -> natural;
coherence
proof
consider v being Vertex of G such that
A1: v.degree() = G.supDegree() and
for w being Vertex of G holds w.degree() c= v.degree() by Th79;
thus thesis by A1;
end;
end;
definition
let G be locally-finite with_max_degree _Graph;
redefine func G.maxDegree() -> Nat; :: redefines .maxDegree() (GLIB_013, synonym) → .supDegree() (GLIB_013, definition)
coherence;
end;
registration
let G be locally-finite with_max_in_degree _Graph;
cluster G.maxInDegree() -> natural;
coherence
proof
consider v being Vertex of G such that
A1: v.inDegree() = G.supInDegree() and
for w being Vertex of G holds w.inDegree() c= v.inDegree() by Th80;
thus thesis by A1;
end;
end;
definition
let G be locally-finite with_max_in_degree _Graph;
redefine func G.maxInDegree() -> Nat; :: redefines .maxInDegree() (GLIB_013, synonym) → .supInDegree() (GLIB_013, definition)
coherence;
end;
registration
let G be locally-finite with_max_out_degree _Graph;
cluster G.maxOutDegree() -> natural;
coherence
proof
consider v being Vertex of G such that
A1: v.outDegree() = G.supOutDegree() and
for w being Vertex of G holds w.outDegree() c= v.outDegree() by Th81;
thus thesis by A1;
end;
end;
definition
let G be locally-finite with_max_out_degree _Graph;
redefine func G.maxOutDegree() -> Nat; :: redefines .maxOutDegree() (GLIB_013, synonym) → .supOutDegree() (GLIB_013, definition)
coherence;
end;
theorem Th83:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is with_max_degree iff G2 is with_max_degree
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
hereby
assume G1 is with_max_degree;
then consider v being Vertex of G1 such that
A2: v.degree() = G1.supDegree() and
for w being Vertex of G1 holds w.degree() c= v.degree() by Th79;
v.degree() = (F_V/.v).degree() by A1, GLIBPRE0:93;
then (F_V/.v).degree() = G2.supDegree() by A1, A2, Th55;
hence G2 is with_max_degree by Lm3;
end;
assume G2 is with_max_degree;
then consider v being Vertex of G2 such that
A3: v.degree() = G2.supDegree() and
for w being Vertex of G2 holds w.degree() c= v.degree() by Th79;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A4: v0 in dom F_V & F_V.v0 = v by FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A4;
F_V/.v0 = v by A4, PARTFUN1:def 6;
then v.degree() = v0.degree() by A1, GLIBPRE0:93;
then v0.degree() = G1.supDegree() by A1, A3, Th55;
hence thesis by Lm3;
end;
theorem Th84:
for G1, G2 being _Graph, F being PGraphMapping of G1, G2
st F is Disomorphism holds
(G1 is with_max_in_degree iff G2 is with_max_in_degree) &
(G1 is with_max_out_degree iff G2 is with_max_out_degree)
proof
let G1, G2 be _Graph, F be PGraphMapping of G1, G2;
assume A1: F is Disomorphism;
hereby
assume G1 is with_max_in_degree;
then consider v being Vertex of G1 such that
A2: v.inDegree() = G1.supInDegree() and
for w being Vertex of G1 holds w.inDegree() c= v.inDegree() by Th80;
v.inDegree() = (F_V/.v).inDegree() by A1, GLIBPRE0:92;
then (F_V/.v).inDegree() = G2.supInDegree() by A1, A2, Th60;
hence G2 is with_max_in_degree by Lm4;
end;
hereby
assume G2 is with_max_in_degree;
then consider v being Vertex of G2 such that
A3: v.inDegree() = G2.supInDegree() and
for w being Vertex of G2 holds w.inDegree() c= v.inDegree() by Th80;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A4: v0 in dom F_V & F_V.v0 = v by FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A4;
F_V/.v0 = v by A4, PARTFUN1:def 6;
then v.inDegree() = v0.inDegree() by A1, GLIBPRE0:92;
then v0.inDegree() = G1.supInDegree() by A1, A3, Th60;
hence G1 is with_max_in_degree by Lm4;
end;
hereby
assume G1 is with_max_out_degree;
then consider v being Vertex of G1 such that
A5: v.outDegree() = G1.supOutDegree() and
for w being Vertex of G1 holds w.outDegree() c= v.outDegree() by Th81;
v.outDegree() = (F_V/.v).outDegree() by A1,GLIBPRE0:92;
then (F_V/.v).outDegree() = G2.supOutDegree() by A1, A5, Th60;
hence G2 is with_max_out_degree by Lm5;
end;
hereby
assume G2 is with_max_out_degree;
then consider v being Vertex of G2 such that
A6: v.outDegree() = G2.supOutDegree() and
for w being Vertex of G2 holds w.outDegree() c= v.outDegree() by Th81;
rng F_V = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A7: v0 in dom F_V & F_V.v0 = v by FUNCT_1:def 3;
reconsider v0 as Vertex of G1 by A7;
F_V/.v0 = v by A7, PARTFUN1:def 6;
then v.outDegree() = v0.outDegree() by A1,GLIBPRE0:92;
then v0.outDegree() = G1.supOutDegree() by A1, A6, Th60;
hence G1 is with_max_out_degree by Lm5;
end;
end;
theorem Th85:
for G1, G2 being _Graph st G1 == G2 holds
(G1 is with_max_degree implies G2 is with_max_degree) &
(G1 is with_max_in_degree implies G2 is with_max_in_degree) &
(G1 is with_max_out_degree implies G2 is with_max_out_degree)
proof
let G1, G2 be _Graph;
assume G1 == G2;
then consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is Disomorphism by GLIBPRE0:75;
thus thesis by A1, Th83, Th84;
end;
theorem Th86:
for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
holds G1 is with_max_degree iff G2 is with_max_degree
proof
let G1 be _Graph, E be set, G2 be reverseEdgeDirections of G1, E;
consider F being PGraphMapping of G1, G2 such that
A1: F = id G1 & F is isomorphism by GLIBPRE0:77;
thus thesis by A1, Th83;
end;
registration
let G be with_max_degree _Graph, E be set;
cluster -> with_max_degree for reverseEdgeDirections of G, E;
coherence by Th86;
end;
Lm6:
for a,b,c being Cardinal st a c= c & b c= c & c c< a +` 2 & not b c= a
holds b = c
proof
let a,b,c be Cardinal;
assume A1: a c= c & b c= c & c c< a +` 2 & not b c= a;
A2: c is finite
proof
assume c is infinite;
then A3: a is infinite by A1, XBOOLE_0:def 8, FINSET_1:1;
then 2 c= a;
then a +` 2 = a by A3, CARD_2:76;
then c in a by A1, ORDINAL1:11;
then c in c by A1;
hence contradiction;
end;
then reconsider n = c as Nat;
reconsider k = a as Nat by A1, A2;
A4: a in b by A1, ORDINAL1:16;
reconsider m = b as Nat by A1, A2;
Segm b c= Segm c by A1;
then A5: m <= n by NAT_1:39;
c in Segm(k+`2) by A1, ORDINAL1:11;
then A6: n < k+2 by NAT_1:44;
a in Segm b by A4;
then k < m by NAT_1:44;
then A7: k+1 <= m by NAT_1:13;
n < (k+1)+1 by A6;
then n <= k+1 by NAT_1:13;
then n <= m by A7, XXREAL_0:2;
hence thesis by A5, XXREAL_0:1;
end;
registration
let G be with_max_degree _Graph, V be set;
cluster -> with_max_degree for addVertices of G, V;
coherence
proof
let H be addVertices of G, V;
consider v0 being Vertex of G such that
A1: for w0 being Vertex of G holds w0.degree() c= v0.degree() by Def12;
the_Vertices_of G c= the_Vertices_of H by GLIB_006:def 9;
then reconsider v = v0 as Vertex of H by TARSKI:def 3;
now
let w be Vertex of H;
per cases;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
w.degree() = w0.degree() & v.degree() = v0.degree() by GLIBPRE0:45;
hence w.degree() c= v.degree() by A1;
end;
suppose A2: not w in the_Vertices_of G;
the_Vertices_of H = the_Vertices_of G \/ V by GLIB_006:def 10;
then w in V by A2, XBOOLE_0:def 3;
then w in V \ the_Vertices_of G by A2, XBOOLE_0:def 5;
then w.degree() = 0 by GLIB_006:88, GLIB_000:157;
hence w.degree() c= v.degree() by XBOOLE_1:2;
end;
end;
hence thesis;
end;
cluster -> with_max_degree for addLoops of G, V;
coherence
proof
let H be addLoops of G, V;
per cases;
suppose A3: V c= the_Vertices_of G;
consider v0 being Vertex of G such that
A4: for w0 being Vertex of G holds w0.degree() c= v0.degree() by Def12;
A5: the_Vertices_of G = the_Vertices_of H by A3, GLIB_012:def 5;
then reconsider v = v0 as Vertex of H;
per cases;
suppose v0 in V;
then A6: v.degree() = v0.degree() +` 2 by A3, GLIB_012:43;
now
let w be Vertex of H;
reconsider w0 = w as Vertex of G by A5;
per cases;
suppose w0 in V;
then A7: w.degree() = w0.degree() +` 2 by A3, GLIB_012:43;
w0.degree() c= v0.degree() & 2 c= 2 by A4;
hence w.degree() c= v.degree() by A6, A7, CARD_2:83;
end;
suppose not w0 in V;
then A8: w.degree() = w0.degree() by A3, GLIB_012:44
.= w0.degree() +` 0 by CARD_2:18;
w0.degree() c= v0.degree() & 0 c= 2 by A4, XBOOLE_1:2;
hence w.degree() c= v.degree() by A6, A8, CARD_2:83;
end;
end;
hence thesis;
end;
suppose not v0 in V & ex w0 being Vertex of G
st w0 in V & v0.degree() c< w0.degree() +` 2;
then consider w0 being Vertex of G such that
A9: w0 in V & v0.degree() c< w0.degree() +` 2;
reconsider w = w0 as Vertex of H by A5;
A10: w.degree() = w0.degree() +` 2 by A3, A9, GLIB_012:43;
per cases;
suppose A11: for u0 being Vertex of G st u0 in V
holds u0.degree() c= w0.degree();
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A5;
per cases;
suppose A12: u0 in V;
then A13: u.degree() = u0.degree() +` 2 by A3, GLIB_012:43;
u0.degree() c= w0.degree() & 2 c= 2 by A11, A12;
hence u.degree() c= w.degree() by A10, A13, CARD_2:83;
end;
suppose not u0 in V;
then u0.degree() = u.degree() by A3, GLIB_012:44;
then u.degree() c= v0.degree() by A4;
hence u.degree() c= w.degree()
by A9, A10, XBOOLE_0:def 8, XBOOLE_1:1;
end;
end;
hence thesis;
end;
suppose ex u0 being Vertex of G
st u0 in V & not u0.degree() c= w0.degree();
then consider u0 being Vertex of G such that
A14: u0 in V & not u0.degree() c= w0.degree();
reconsider u = u0 as Vertex of H by A5;
A15: u.degree() = u0.degree() +` 2 by A3, A14, GLIB_012:43;
u0.degree() c= v0.degree() & w0.degree() c= v0.degree() by A4;
then A16: u0.degree() = v0.degree() by A9, A14, Lm6;
now
let x be Vertex of H;
reconsider x0 = x as Vertex of G by A5;
per cases;
suppose x0 in V;
then A17: x.degree() = x0.degree() +` 2 by A3, GLIB_012:43;
x0.degree() c= u0.degree() & 2 c= 2 by A4, A16;
hence x.degree() c= u.degree() by A15, A17, CARD_2:83;
end;
suppose not x0 in V;
then A18: x.degree() = x0.degree() by A3, GLIB_012:44
.= x0.degree() +` 0 by CARD_2:18;
x0.degree() c= u0.degree() & 0 c= 2 by A4, A16, XBOOLE_1:2;
hence x.degree() c= u.degree() by A15, A18, CARD_2:83;
end;
end;
hence thesis;
end;
end;
suppose A19: not v0 in V & for w0 being Vertex of G
holds not w0 in V or not v0.degree() c< w0.degree() +` 2;
then A20: v.degree() = v0.degree() by A3, GLIB_012:44;
now
let w be Vertex of H;
reconsider w0 = w as Vertex of G by A5;
per cases;
suppose A21: w0 in V;
then w.degree() = w0.degree() +` 2 by A3, GLIB_012:43;
hence w.degree() c= v.degree() by A19, A20, A21, XBOOLE_0:def 8;
end;
suppose not w0 in V;
then w.degree() = w0.degree() by A3, GLIB_012:44;
hence w.degree() c= v.degree() by A4, A20;
end;
end;
hence thesis;
end;
end;
suppose not V c= the_Vertices_of G;
then G == H by GLIB_012:def 5;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_degree _Graph, v,e,w be object;
cluster -> with_max_degree for addEdge of G,v,e,w;
coherence
proof
let H be addEdge of G,v,e,w;
per cases;
suppose A1: v is Vertex of G & w is Vertex of G & not e in the_Edges_of G;
then reconsider v1 = v, w1 = w as Vertex of G;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0.degree() c= v0.degree() by Def12;
A3: the_Vertices_of G = the_Vertices_of H by A1, GLIB_006:def 11;
then reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H;
per cases;
suppose A4: v <> w & v0.degree() = v1.degree();
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = v;
hence u.degree() c= v2.degree();
end;
suppose u0 = w;
then A5: u.degree() = w1.degree() +`1 by A1, A4, GLIBPRE0:48;
w1.degree() c= v1.degree() & 1 c= 1 by A2, A4;
then w1.degree() +`1 c= v1.degree() +`1 by CARD_2:83;
hence u.degree() c= v2.degree() by A1, A4, A5, GLIBPRE0:47;
end;
suppose u0 <> v & u0 <> w;
then A6: u.degree() = u0.degree() by GLIBPRE0:46;
u0.degree() c= v1.degree() & 0 c= 1 by A2, A4, XBOOLE_1:2;
then u0.degree() +`0 c= v1.degree() +`1 by CARD_2:83;
then u.degree() c= v1.degree() +`1 by A6, CARD_2:18;
hence u.degree() c= v2.degree() by A1, A4, GLIBPRE0:47;
end;
end;
hence thesis;
end;
suppose A7: v <> w & v0.degree() = w1.degree();
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = w;
hence u.degree() c= w2.degree();
end;
suppose u0 = v;
then A8: u.degree() = v1.degree() +`1 by A1, A7, GLIBPRE0:47;
v1.degree() c= w1.degree() & 1 c= 1 by A2, A7;
then v1.degree() +`1 c= w1.degree() +`1 by CARD_2:83;
hence u.degree() c= w2.degree() by A1, A7, A8, GLIBPRE0:48;
end;
suppose u0 <> v & u0 <> w;
then A9: u.degree() = u0.degree() by GLIBPRE0:46;
u0.degree() c= w1.degree() & 0 c= 1 by A2, A7, XBOOLE_1:2;
then u0.degree() +`0 c= w1.degree() +`1 by CARD_2:83;
then u.degree() c= w1.degree() +`1 by A9, CARD_2:18;
hence u.degree() c= w2.degree() by A1, A7, GLIBPRE0:48;
end;
end;
hence thesis;
end;
suppose A10: v<>w & v0.degree()<>v1.degree() & v0.degree()<>w1.degree();
then v1.degree() +`1 c= v0.degree() & w1.degree() +`1 c= v0.degree()
by A2, Lm1;
then A11
: v1.degree()+`1 c= v9.degree() & w1.degree() +`1 c= v9.degree()
by A10, GLIBPRE0:46;
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = v;
hence u.degree() c= v9.degree() by A1, A10, A11, GLIBPRE0:47;
end;
suppose u0 = w;
hence u.degree() c= v9.degree() by A1, A10, A11, GLIBPRE0:48;
end;
suppose u0 <> v & u0 <> w;
then A12: u.degree() = u0.degree() by GLIBPRE0:46;
u0.degree() c= v0.degree() by A2;
hence u.degree() c= v9.degree() by A10, A12, GLIBPRE0:46;
end;
end;
hence thesis;
end;
suppose v = w;
then H is addLoops of G, {v1} by A1, GLIB_012:27;
hence thesis;
end;
end;
suppose not(v is Vertex of G & w is Vertex of G & not e in the_Edges_of G);
then G == H by GLIB_006:def 11;
hence thesis by Th85;
end;
end;
cluster -> with_max_degree for addAdjVertex of G,v,e,w;
coherence
proof
let H be addAdjVertex of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G;
then consider G9 being addVertex of G, w such that
A13: H is addEdge of G9,v,e,w by GLIB_006:125;
thus thesis by A13;
end;
suppose not v in the_Vertices_of G & not e in the_Edges_of G &
w in the_Vertices_of G;
then consider G9 being addVertex of G, v such that
A14: H is addEdge of G9,v,e,w by GLIB_006:126;
thus thesis by A14;
end;
suppose not((v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G)or(not v in the_Vertices_of G &
not e in the_Edges_of G & w in the_Vertices_of G));
then G == H by GLIB_006:def 12;
hence thesis by Th85;
end;
end;
end;
Lm7: for a, b being Cardinal st a in b+`1 holds a c= b
proof
let a,b be Cardinal;
assume A1: a in b+`1;
per cases;
suppose A2: b is infinite;
then 1 c= b;
then b+`1 = b by A2, CARD_2:76;
hence thesis by A1, ORDINAL1:def 2;
end;
suppose A3: b is finite;
then reconsider m = b as Nat;
b+`1 is finite & a c= b+`1 by A1, A3, ORDINAL1:def 2;
then reconsider n = a as Nat;
a in Segm(m+`1) by A1;
then n < m+1 by NAT_1:44;
then n <= m by NAT_1:13;
then Segm n c= Segm m by NAT_1:39;
hence thesis;
end;
end;
registration
let G be with_max_degree _Graph, v be object, V be set;
cluster -> with_max_degree for addAdjVertexAll of G,v,V;
coherence
proof
let H be addAdjVertexAll of G,v,V;
per cases;
suppose A1: not v in the_Vertices_of G & V c= the_Vertices_of G;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0.degree() c= v0.degree()
by Def12;
A3: the_Vertices_of H = the_Vertices_of G \/ {v} by A1, GLIB_007:def 4;
then reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;
reconsider v1 = v as Vertex of H by A1, GLIB_007:50;
A4: for w being Vertex of H, w0 being Vertex of G st w = w0 &
w.degree() <> w0.degree()+`1 holds w.degree()=w0.degree()
proof
let w be Vertex of H, w0 be Vertex of G;
assume A5: w = w0;
assume A6: w.degree() <> w0.degree()+`1;
A7: w.degree() c= w0.degree()+`1 by A5, GLIBPRE0:58;
then A8: w.degree()+`1 c= w0.degree()+`1 by A6, Lm1;
G is Subgraph of H by GLIB_006:57;
then w0.inDegree() c= w.inDegree() & w0.outDegree() c= w.outDegree()
by A5, GLIB_000:78, CARD_1:11;
then A9: w0.degree() c= w.degree() by CARD_2:83;
then w0.degree()+`1 c= w.degree()+`1 by CARD_2:83;
then A10: w.degree()+`1 = w0.degree()+`1 by A8, XBOOLE_0:def 10;
per cases by A7;
suppose A11: w0.degree() is infinite;
then A12: w.degree() is infinite by A9;
then 1 c= w.degree();
then A13: w.degree()+`1 = w.degree() by A12, CARD_2:76;
1 c= w0.degree() by A11;
hence thesis by A10, A11, A13, CARD_2:76;
end;
suppose w.degree() is finite;
then reconsider m = w0.degree(), n = w.degree() as Nat by A9;
m + 1 = m +` 1 .= n +` 1 by A10 .= n + 1;
hence thesis;
end;
end;
per cases by ORDINAL1:16;
suppose A14: v0.degree() +`1 c= v1.degree();
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
A15: w.degree() c= w0.degree() +`1 by GLIBPRE0:58;
w0.degree() c= v0.degree() & 1 c= 1 by A2;
then w0.degree() +`1 c= v0.degree() +`1 by CARD_2:83;
then w.degree() c= v0.degree() +`1 by A15, XBOOLE_1:1;
hence w.degree() c= v1.degree() by A14, XBOOLE_1:1;
end;
suppose w in {v};
hence w.degree() c= v1.degree() by TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose A16: v1.degree() in v0.degree() +`1 &
v9.degree() = v0.degree() +`1;
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
A17: w.degree() c= w0.degree() +`1 by GLIBPRE0:58;
w0.degree() c= v0.degree() & 1 c= 1 by A2;
then w0.degree() +`1 c= v0.degree() +`1 by CARD_2:83;
hence w.degree() c= v9.degree() by A16, A17, XBOOLE_1:1;
end;
suppose w in {v};
then w = v1 by TARSKI:def 1;
hence w.degree() c= v9.degree() by A16, ORDINAL1:def 2;
end;
end;
hence thesis;
end;
suppose A18: v1.degree() in v0.degree() +`1 &
v9.degree() <> v0.degree() +`1 &
for w0 being Vertex of G, w being Vertex of H st w0 = w &
w.degree() = w0.degree() +`1
holds w0.degree() +`1 c= v0.degree();
then A19: v9.degree() = v0.degree() by A4;
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
per cases;
suppose w.degree() = w0.degree() +`1;
hence w.degree() c= v9.degree() by A18, A19;
end;
suppose w.degree() <> w0.degree() +`1;
then w.degree() = w0.degree() by A4;
hence w.degree() c= v9.degree() by A2, A19;
end;
end;
suppose w in {v};
then w = v1 by TARSKI:def 1;
hence w.degree() c= v9.degree() by A18, A19, Lm7;
end;
end;
hence thesis;
end;
suppose A20: v1.degree() c= v0.degree() +`1 &
v9.degree() <> v0.degree() +`1 &
not for w0 being Vertex of G, w being Vertex of H st w0 = w &
w.degree() = w0.degree() +`1
holds w.degree() = w0.degree() +`1 &
w0.degree() +`1 c= v0.degree();
consider w0 being Vertex of G, w being Vertex of H such that
A21: w0 = w & w.degree() = w0.degree() +`1 and
A22: not w0.degree() +`1 c= v0.degree() by A20;
v0.degree() in w.degree() by A21, A22, ORDINAL1:16;
then v0.degree() c= w.degree() & v0.degree() <> w.degree()
by ORDINAL1:16;
then A23: v0.degree()+`1 c= w.degree() by Lm1;
now
let u be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose u in the_Vertices_of G;
then reconsider u0 = u as Vertex of G;
A24: u.degree() c= u0.degree()+`1 by GLIBPRE0:58;
u0.degree() c= v0.degree() & 1 c= 1 by A2;
then u0.degree()+`1 c= v0.degree()+`1 by CARD_2:83;
then u0.degree()+`1 c= w.degree() by A23, XBOOLE_1:1;
hence u.degree() c= w.degree() by A24, XBOOLE_1:1;
end;
suppose u in {v};
then u = v1 by TARSKI:def 1;
hence u.degree() c= w.degree() by A20, A23, XBOOLE_1:1;
end;
end;
hence thesis;
end;
end;
suppose not(not v in the_Vertices_of G & V c= the_Vertices_of G);
then G == H by GLIB_007:def 4;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_in_degree _Graph;
cluster -> with_max_out_degree for reverseEdgeDirections of G;
coherence
proof
let H be reverseEdgeDirections of G;
consider v1 be Vertex of G such that
A1: for w1 being Vertex of G holds w1.inDegree() c= v1.inDegree()
by Def13;
A2: the_Vertices_of G = the_Vertices_of H by GLIB_007:def 1;
then reconsider v2 = v1 as Vertex of H;
now
let w2 be Vertex of H;
reconsider w1 = w2 as Vertex of G by A2;
w1.inDegree() c= v1.inDegree() by A1;
then w1.inDegree() c= v2.outDegree() by GLIBPRE0:53;
hence w2.outDegree() c= v2.outDegree() by GLIBPRE0:53;
end;
hence thesis;
end;
end;
registration
let G be with_max_in_degree _Graph, V be set;
cluster -> with_max_in_degree for addVertices of G, V;
coherence
proof
let H be addVertices of G, V;
consider v0 being Vertex of G such that
A1: for w0 being Vertex of G holds w0.inDegree() c= v0.inDegree()
by Def13;
the_Vertices_of G c= the_Vertices_of H by GLIB_006:def 9;
then reconsider v = v0 as Vertex of H by TARSKI:def 3;
now
let w be Vertex of H;
per cases;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
w.inDegree() = w0.inDegree() & v.inDegree() = v0.inDegree()
by GLIBPRE0:45;
hence w.inDegree() c= v.inDegree() by A1;
end;
suppose A2: not w in the_Vertices_of G;
the_Vertices_of H = the_Vertices_of G \/ V by GLIB_006:def 10;
then w in V by A2, XBOOLE_0:def 3;
then w in V \ the_Vertices_of G by A2, XBOOLE_0:def 5;
then w is isolated by GLIB_006:88;
then w.inDegree() = 0 by GLIB_000:156;
hence w.inDegree() c= v.inDegree() by XBOOLE_1:2;
end;
end;
hence thesis;
end;
cluster -> with_max_in_degree for addLoops of G, V;
coherence
proof
let H be addLoops of G, V;
per cases;
suppose A3: V c= the_Vertices_of G;
consider v0 being Vertex of G such that
A4: for w0 being Vertex of G holds w0.inDegree() c= v0.inDegree()
by Def13;
A5: the_Vertices_of G = the_Vertices_of H by A3, GLIB_012:def 5;
then reconsider v = v0 as Vertex of H;
per cases;
suppose v0 in V;
then A6: v.inDegree() = v0.inDegree() +` 1 by A3, GLIB_012:43;
now
let w be Vertex of H;
reconsider w0 = w as Vertex of G by A5;
per cases;
suppose w0 in V;
then A7: w.inDegree() = w0.inDegree() +` 1 by A3, GLIB_012:43;
w0.inDegree() c= v0.inDegree() & 1 c= 1 by A4;
hence w.inDegree() c= v.inDegree() by A6, A7, CARD_2:83;
end;
suppose not w0 in V;
then A8: w.inDegree() = w0.inDegree() by A3, GLIB_012:44
.= w0.inDegree() +` 0 by CARD_2:18;
w0.inDegree() c= v0.inDegree() & 0 c= 1 by A4, XBOOLE_1:2;
hence w.inDegree() c= v.inDegree() by A6, A8, CARD_2:83;
end;
end;
hence thesis;
end;
suppose not v0 in V & ex w0 being Vertex of G
st w0 in V & v0.inDegree() c< w0.inDegree() +` 1;
then consider w0 being Vertex of G such that
A9: w0 in V & v0.inDegree() c< w0.inDegree() +` 1;
reconsider w = w0 as Vertex of H by A5;
A10: w.inDegree() = w0.inDegree() +` 1 by A3, A9, GLIB_012:43;
not w0.inDegree() +` 1 c= v0.inDegree() by A9, XBOOLE_0:def 8;
then A11: w0.inDegree() = v0.inDegree() by A4, Lm1;
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A5;
per cases;
suppose u0 in V;
then A12: u.inDegree() = u0.inDegree() +` 1 by A3, GLIB_012:43;
u0.inDegree() c= w0.inDegree() & 1 c= 1 by A4, A11;
hence u.inDegree() c= w.inDegree() by A10, A12, CARD_2:83;
end;
suppose not u0 in V;
then A13: u.inDegree() = u0.inDegree() by A3, GLIB_012:44
.= u0.inDegree() +` 0 by CARD_2:18;
u0.inDegree() c= w0.inDegree() & 0 c= 1 by A4, A11, XBOOLE_1:2;
hence u.inDegree() c= w.inDegree() by A10, A13, CARD_2:83;
end;
end;
hence thesis;
end;
suppose A14: not v0 in V & for w0 being Vertex of G
holds not w0 in V or not v0.inDegree() c< w0.inDegree() +` 1;
then A15: v.inDegree() = v0.inDegree() by A3, GLIB_012:44;
now
let w be Vertex of H;
reconsider w0 = w as Vertex of G by A5;
per cases;
suppose A16: w0 in V;
then w.inDegree() = w0.inDegree() +` 1 by A3, GLIB_012:43;
hence w.inDegree()c= v.inDegree() by A14, A15, A16, XBOOLE_0:def 8;
end;
suppose not w0 in V;
then w.inDegree() = w0.inDegree() by A3, GLIB_012:44;
hence w.inDegree() c= v.inDegree() by A4, A15;
end;
end;
hence thesis;
end;
end;
suppose not V c= the_Vertices_of G;
then G == H by GLIB_012:def 5;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_in_degree _Graph, v,e,w be object;
cluster -> with_max_in_degree for addEdge of G,v,e,w;
coherence
proof
let H be addEdge of G,v,e,w;
per cases;
suppose A1: v is Vertex of G & w is Vertex of G & not e in the_Edges_of G;
then reconsider v1 = v, w1 = w as Vertex of G;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0.inDegree() c= v0.inDegree()
by Def13;
A3: the_Vertices_of G = the_Vertices_of H by A1, GLIB_006:def 11;
then reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H;
per cases;
suppose A4: v <> w & v0.inDegree() = w1.inDegree();
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = w;
hence u.inDegree() c= w2.inDegree();
end;
suppose u0 = v;
then A5: u.inDegree() = v1.inDegree() by A1, A4, GLIBPRE0:47
.= v1.inDegree() +` 0 by CARD_2:18;
v1.inDegree() c= w1.inDegree() & 0 c= 1 by A2, A4, XBOOLE_1:2;
then v1.inDegree() +`0 c= w1.inDegree() +`1 by CARD_2:83;
hence u.inDegree() c= w2.inDegree() by A1, A4, A5, GLIBPRE0:48;
end;
suppose u0 <> v & u0 <> w;
then A6: u.inDegree() = u0.inDegree() by GLIBPRE0:46;
u0.inDegree() c= w1.inDegree() & 0 c= 1 by A2, A4, XBOOLE_1:2;
then u0.inDegree() +`0 c= w1.inDegree() +`1 by CARD_2:83;
then u.inDegree() c= w1.inDegree() +`1 by A6, CARD_2:18;
hence u.inDegree() c= w2.inDegree() by A1, A4, GLIBPRE0:48;
end;
end;
hence thesis;
end;
suppose A7: v <> w & v0.inDegree() <> w1.inDegree();
A8: v0.inDegree() = v9.inDegree()
proof
per cases;
suppose v0 <> v1;
hence thesis by A7, GLIBPRE0:46;
end;
suppose v0 = v1;
hence thesis by A1, A7, GLIBPRE0:47;
end;
end;
then A9: w1.inDegree() +`1 c= v9.inDegree() by A2, A7, Lm1;
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = v;
then u.inDegree() = v1.inDegree() by A1, A7, GLIBPRE0:47;
hence u.inDegree() c= v9.inDegree() by A2, A8;
end;
suppose u0 = w;
hence u.inDegree() c= v9.inDegree() by A1, A7, A9, GLIBPRE0:48;
end;
suppose u0 <> v & u0 <> w;
then u.inDegree() = u0.inDegree() by GLIBPRE0:46;
hence u.inDegree() c= v9.inDegree() by A2, A8;
end;
end;
hence thesis;
end;
suppose v = w;
then H is addLoops of G, {v1} by A1, GLIB_012:27;
hence thesis;
end;
end;
suppose not(v is Vertex of G & w is Vertex of G & not e in the_Edges_of G);
then G == H by GLIB_006:def 11;
hence thesis by Th85;
end;
end;
cluster -> with_max_in_degree for addAdjVertex of G,v,e,w;
coherence
proof
let H be addAdjVertex of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G;
then consider G9 being addVertex of G, w such that
A10: H is addEdge of G9,v,e,w by GLIB_006:125;
thus thesis by A10;
end;
suppose not v in the_Vertices_of G & not e in the_Edges_of G &
w in the_Vertices_of G;
then consider G9 being addVertex of G, v such that
A11: H is addEdge of G9,v,e,w by GLIB_006:126;
thus thesis by A11;
end;
suppose not((v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G)or(not v in the_Vertices_of G &
not e in the_Edges_of G & w in the_Vertices_of G));
then G == H by GLIB_006:def 12;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_in_degree _Graph, v be object, V be set;
cluster -> with_max_in_degree for addAdjVertexAll of G,v,V;
coherence
proof
let H be addAdjVertexAll of G,v,V;
per cases;
suppose A1: not v in the_Vertices_of G & V c= the_Vertices_of G;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0.inDegree() c= v0.inDegree()
by Def13;
A3: the_Vertices_of H = the_Vertices_of G \/ {v} by A1, GLIB_007:def 4;
then reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;
reconsider v1 = v as Vertex of H by A1, GLIB_007:50;
A4: for w being Vertex of H, w0 being Vertex of G st w = w0 &
w.inDegree() <> w0.inDegree()+`1 holds w.inDegree()=w0.inDegree()
proof
let w be Vertex of H, w0 be Vertex of G;
assume A5: w = w0;
assume A6: w.inDegree() <> w0.inDegree()+`1;
A7: w.inDegree() c= w0.inDegree()+`1 by A5, GLIBPRE0:58;
then A8: w.inDegree()+`1 c= w0.inDegree()+`1 by A6, Lm1;
G is Subgraph of H by GLIB_006:57;
then A9: w0.inDegree() c= w.inDegree() by A5, GLIB_000:78, CARD_1:11;
then w0.inDegree()+`1 c= w.inDegree()+`1 by CARD_2:83;
then A10: w.inDegree()+`1 = w0.inDegree()+`1 by A8, XBOOLE_0:def 10;
per cases by A7;
suppose A11: w0.inDegree() is infinite;
then A12: w.inDegree() is infinite by A9;
then 1 c= w.inDegree();
then A13: w.inDegree()+`1 = w.inDegree() by A12, CARD_2:76;
1 c= w0.inDegree() by A11;
hence thesis by A10, A11, A13, CARD_2:76;
end;
suppose w.inDegree() is finite;
then reconsider m = w0.inDegree(),n = w.inDegree() as Nat by A9;
m + 1 = m +` 1 .= n +` 1 by A10 .= n + 1;
hence thesis;
end;
end;
per cases by ORDINAL1:16;
suppose A14: v0.inDegree() +`1 c= v1.inDegree();
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
A15: w.inDegree() c= w0.inDegree() +`1 by GLIBPRE0:58;
w0.inDegree() c= v0.inDegree() & 1 c= 1 by A2;
then w0.inDegree() +`1 c= v0.inDegree() +`1 by CARD_2:83;
then w.inDegree() c= v0.inDegree() +`1 by A15, XBOOLE_1:1;
hence w.inDegree() c= v1.inDegree() by A14, XBOOLE_1:1;
end;
suppose w in {v};
hence w.inDegree() c= v1.inDegree() by TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose A16: v1.inDegree() in v0.inDegree() +`1 &
v9.inDegree() = v0.inDegree() +`1;
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
A17: w.inDegree() c= w0.inDegree() +`1 by GLIBPRE0:58;
w0.inDegree() c= v0.inDegree() & 1 c= 1 by A2;
then w0.inDegree() +`1 c= v0.inDegree() +`1 by CARD_2:83;
hence w.inDegree() c= v9.inDegree() by A16, A17, XBOOLE_1:1;
end;
suppose w in {v};
then w = v1 by TARSKI:def 1;
hence w.inDegree() c= v9.inDegree() by A16, ORDINAL1:def 2;
end;
end;
hence thesis;
end;
suppose A18: v1.inDegree() in v0.inDegree() +`1 &
v9.inDegree() <> v0.inDegree() +`1 &
for w0 being Vertex of G, w being Vertex of H st w0 = w &
w.inDegree() = w0.inDegree() +`1
holds w0.inDegree() +`1 c= v0.inDegree();
then A19: v9.inDegree() = v0.inDegree() by A4;
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
per cases;
suppose w.inDegree() = w0.inDegree() +`1;
hence w.inDegree() c= v9.inDegree() by A18, A19;
end;
suppose w.inDegree() <> w0.inDegree() +`1;
then w.inDegree() = w0.inDegree() by A4;
hence w.inDegree() c= v9.inDegree() by A2, A19;
end;
end;
suppose w in {v};
then w.inDegree() = v1.inDegree() by TARSKI:def 1;
hence w.inDegree() c= v9.inDegree() by A18, A19, Lm7;
end;
end;
hence thesis;
end;
suppose A20: v1.inDegree() c= v0.inDegree() +`1 &
v9.inDegree() <> v0.inDegree() +`1 &
not for w0 being Vertex of G, w being Vertex of H st w0 = w &
w.inDegree() = w0.inDegree() +`1
holds w.inDegree() = w0.inDegree() +`1 &
w0.inDegree() +`1 c= v0.inDegree();
consider w0 being Vertex of G, w being Vertex of H such that
A21: w0 = w & w.inDegree() = w0.inDegree() +`1 and
A22: not w0.inDegree() +`1 c= v0.inDegree() by A20;
v0.inDegree() in w.inDegree() by A21, A22, ORDINAL1:16;
then v0.inDegree() c= w.inDegree() & v0.inDegree() <> w.inDegree()
by ORDINAL1:16;
then A23: v0.inDegree()+`1 c= w.inDegree() by Lm1;
now
let u be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose u in the_Vertices_of G;
then reconsider u0 = u as Vertex of G;
A24: u.inDegree() c= u0.inDegree()+`1 by GLIBPRE0:58;
u0.inDegree() c= v0.inDegree() & 1 c= 1 by A2;
then u0.inDegree()+`1 c= v0.inDegree()+`1 by CARD_2:83;
then u0.inDegree()+`1 c= w.inDegree() by A23, XBOOLE_1:1;
hence u.inDegree() c= w.inDegree() by A24, XBOOLE_1:1;
end;
suppose u in {v};
then u = v1 by TARSKI:def 1;
hence u.inDegree() c= w.inDegree() by A20, A23, XBOOLE_1:1;
end;
end;
hence thesis;
end;
end;
suppose not(not v in the_Vertices_of G & V c= the_Vertices_of G);
then G == H by GLIB_007:def 4;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_out_degree _Graph;
cluster -> with_max_in_degree for reverseEdgeDirections of G ;
coherence
proof
let H be reverseEdgeDirections of G;
consider v1 be Vertex of G such that
A1: for w1 being Vertex of G holds w1.outDegree() c= v1.outDegree()
by Def14;
A2: the_Vertices_of G = the_Vertices_of H by GLIB_007:def 1;
then reconsider v2 = v1 as Vertex of H;
now
let w2 be Vertex of H;
reconsider w1 = w2 as Vertex of G by A2;
w1.outDegree() c= v1.outDegree() by A1;
then w1.outDegree() c= v2.inDegree() by GLIBPRE0:53;
hence w2.inDegree() c= v2.inDegree() by GLIBPRE0:53;
end;
hence thesis;
end;
end;
registration
let G be with_max_out_degree _Graph, V be set;
cluster -> with_max_out_degree for addVertices of G, V;
coherence
proof
let H be addVertices of G, V;
consider v0 being Vertex of G such that
A1: for w0 being Vertex of G holds w0.outDegree() c= v0.outDegree()
by Def14;
the_Vertices_of G c= the_Vertices_of H by GLIB_006:def 9;
then reconsider v = v0 as Vertex of H by TARSKI:def 3;
now
let w be Vertex of H;
per cases;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
w.outDegree()=w0.outDegree() & v.outDegree()=v0.outDegree()
by GLIBPRE0:45;
hence w.outDegree() c= v.outDegree() by A1;
end;
suppose A2: not w in the_Vertices_of G;
the_Vertices_of H = the_Vertices_of G \/ V by GLIB_006:def 10;
then w in V by A2, XBOOLE_0:def 3;
then w in V \ the_Vertices_of G by A2, XBOOLE_0:def 5;
then w is isolated by GLIB_006:88;
then w.outDegree() = 0 by GLIB_000:156;
hence w.outDegree() c= v.outDegree() by XBOOLE_1:2;
end;
end;
hence thesis;
end;
cluster -> with_max_out_degree for addLoops of G, V;
coherence
proof
let H be addLoops of G, V;
per cases;
suppose A3: V c= the_Vertices_of G;
consider v0 being Vertex of G such that
A4: for w0 being Vertex of G holds w0.outDegree() c= v0.outDegree()
by Def14;
A5: the_Vertices_of G = the_Vertices_of H by A3, GLIB_012:def 5;
then reconsider v = v0 as Vertex of H;
per cases;
suppose v0 in V;
then A6: v.outDegree() = v0.outDegree() +` 1 by A3, GLIB_012:43;
now
let w be Vertex of H;
reconsider w0 = w as Vertex of G by A5;
per cases;
suppose w0 in V;
then A7: w.outDegree() = w0.outDegree() +` 1 by A3, GLIB_012:43;
w0.outDegree() c= v0.outDegree() & 1 c= 1 by A4;
hence w.outDegree() c= v.outDegree() by A6, A7, CARD_2:83;
end;
suppose not w0 in V;
then A8: w.outDegree() = w0.outDegree() by A3, GLIB_012:44
.= w0.outDegree() +` 0 by CARD_2:18;
w0.outDegree() c= v0.outDegree() & 0 c= 1 by A4, XBOOLE_1:2;
hence w.outDegree() c= v.outDegree() by A6, A8, CARD_2:83;
end;
end;
hence thesis;
end;
suppose not v0 in V & ex w0 being Vertex of G
st w0 in V & v0.outDegree() c< w0.outDegree() +` 1;
then consider w0 being Vertex of G such that
A9: w0 in V & v0.outDegree() c< w0.outDegree() +` 1;
reconsider w = w0 as Vertex of H by A5;
A10: w.outDegree() = w0.outDegree() +` 1 by A3, A9, GLIB_012:43;
not w0.outDegree() +` 1 c= v0.outDegree() by A9, XBOOLE_0:def 8;
then A11: w0.outDegree() = v0.outDegree() by A4, Lm1;
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A5;
per cases;
suppose u0 in V;
then A12: u.outDegree() = u0.outDegree() +` 1 by A3, GLIB_012:43;
u0.outDegree() c= w0.outDegree() & 1 c= 1 by A4, A11;
hence u.outDegree() c= w.outDegree() by A10, A12, CARD_2:83;
end;
suppose not u0 in V;
then A13: u.outDegree() = u0.outDegree() by A3, GLIB_012:44
.= u0.outDegree() +` 0 by CARD_2:18;
u0.outDegree() c= w0.outDegree() & 0 c= 1 by A4, A11, XBOOLE_1:2;
hence u.outDegree() c= w.outDegree() by A10, A13, CARD_2:83;
end;
end;
hence thesis;
end;
suppose A14: not v0 in V & for w0 being Vertex of G
holds not w0 in V or not v0.outDegree() c< w0.outDegree() +` 1;
then A15: v.outDegree() = v0.outDegree() by A3, GLIB_012:44;
now
let w be Vertex of H;
reconsider w0 = w as Vertex of G by A5;
per cases;
suppose A16: w0 in V;
then w.outDegree() = w0.outDegree() +` 1 by A3, GLIB_012:43;
hence w.outDegree() c= v.outDegree()
by A14, A15, A16, XBOOLE_0:def 8;
end;
suppose not w0 in V;
then w.outDegree() = w0.outDegree() by A3, GLIB_012:44;
hence w.outDegree() c= v.outDegree() by A4, A15;
end;
end;
hence thesis;
end;
end;
suppose not V c= the_Vertices_of G;
then G == H by GLIB_012:def 5;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_out_degree _Graph, v,e,w be object;
cluster -> with_max_out_degree for addEdge of G,v,e,w;
coherence
proof
let H be addEdge of G,v,e,w;
per cases;
suppose A1: v is Vertex of G & w is Vertex of G & not e in the_Edges_of G;
then reconsider v1 = v, w1 = w as Vertex of G;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0.outDegree() c= v0.outDegree()
by Def14;
A3: the_Vertices_of G = the_Vertices_of H by A1, GLIB_006:def 11;
then reconsider v9 = v0, v2 = v1, w2 = w1 as Vertex of H;
per cases;
suppose A4: v <> w & v0.outDegree() = v1.outDegree();
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = v;
hence u.outDegree() c= v2.outDegree();
end;
suppose u0 = w;
then A5: u.outDegree() = w1.outDegree() by A1, A4, GLIBPRE0:48
.= w1.outDegree() +` 0 by CARD_2:18;
w1.outDegree() c= v1.outDegree() & 0 c= 1 by A2, A4, XBOOLE_1:2;
then w1.outDegree() +`0 c= v1.outDegree() +`1 by CARD_2:83;
hence u.outDegree() c= v2.outDegree() by A1, A4, A5, GLIBPRE0:47;
end;
suppose u0 <> v & u0 <> w;
then A6: u.outDegree() = u0.outDegree() by GLIBPRE0:46;
u0.outDegree() c= v1.outDegree() & 0 c= 1 by A2, A4, XBOOLE_1:2;
then u0.outDegree() +`0 c= v1.outDegree() +`1 by CARD_2:83;
then u.outDegree() c= v1.outDegree() +`1 by A6, CARD_2:18;
hence u.outDegree() c= v2.outDegree() by A1, A4, GLIBPRE0:47;
end;
end;
hence thesis;
end;
suppose A7: v <> w & v0.outDegree() <> v1.outDegree();
A8: v0.outDegree() = v9.outDegree()
proof
per cases;
suppose v0 <> w1;
hence thesis by A7, GLIBPRE0:46;
end;
suppose v0 = w1;
hence thesis by A1, A7, GLIBPRE0:48;
end;
end;
then A9: v1.outDegree() +`1 c= v9.outDegree() by A2, A7, Lm1;
now
let u be Vertex of H;
reconsider u0 = u as Vertex of G by A3;
per cases;
suppose u0 = w;
then u.outDegree() = w1.outDegree() by A1, A7, GLIBPRE0:48;
hence u.outDegree() c= v9.outDegree() by A2, A8;
end;
suppose u0 = v;
hence u.outDegree() c= v9.outDegree() by A1, A7, A9, GLIBPRE0:47;
end;
suppose u0 <> v & u0 <> w;
then u.outDegree() = u0.outDegree() by GLIBPRE0:46;
hence u.outDegree() c= v9.outDegree() by A2, A8;
end;
end;
hence thesis;
end;
suppose v = w;
then H is addLoops of G, {v1} by A1, GLIB_012:27;
hence thesis;
end;
end;
suppose not(v is Vertex of G & w is Vertex of G & not e in the_Edges_of G);
then G == H by GLIB_006:def 11;
hence thesis by Th85;
end;
end;
cluster -> with_max_out_degree for addAdjVertex of G,v,e,w;
coherence
proof
let H be addAdjVertex of G,v,e,w;
per cases;
suppose v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G;
then consider G9 being addVertex of G, w such that
A10: H is addEdge of G9,v,e,w by GLIB_006:125;
thus thesis by A10;
end;
suppose not v in the_Vertices_of G & not e in the_Edges_of G &
w in the_Vertices_of G;
then consider G9 being addVertex of G, v such that
A11: H is addEdge of G9,v,e,w by GLIB_006:126;
thus thesis by A11;
end;
suppose not((v in the_Vertices_of G & not e in the_Edges_of G &
not w in the_Vertices_of G)or(not v in the_Vertices_of G &
not e in the_Edges_of G & w in the_Vertices_of G));
then G == H by GLIB_006:def 12;
hence thesis by Th85;
end;
end;
end;
registration
let G be with_max_out_degree _Graph, v be object, V be set;
cluster -> with_max_out_degree for addAdjVertexAll of G,v,V;
coherence
proof
let H be addAdjVertexAll of G,v,V;
per cases;
suppose A1: not v in the_Vertices_of G & V c= the_Vertices_of G;
consider v0 being Vertex of G such that
A2: for w0 being Vertex of G holds w0.outDegree() c= v0.outDegree()
by Def14;
A3: the_Vertices_of H = the_Vertices_of G \/ {v} by A1, GLIB_007:def 4;
then reconsider v9 = v0 as Vertex of H by XBOOLE_0:def 3;
reconsider v1 = v as Vertex of H by A1, GLIB_007:50;
A4: for w being Vertex of H, w0 being Vertex of G st w = w0 &
w.outDegree() <> w0.outDegree()+`1 holds w.outDegree()=w0.outDegree()
proof
let w be Vertex of H, w0 be Vertex of G;
assume A5: w = w0;
assume A6: w.outDegree() <> w0.outDegree()+`1;
A7: w.outDegree() c= w0.outDegree()+`1 by A5, GLIBPRE0:58;
then A8: w.outDegree()+`1 c= w0.outDegree()+`1 by A6, Lm1;
G is Subgraph of H by GLIB_006:57;
then A9: w0.outDegree()c= w.outDegree() by A5, GLIB_000:78, CARD_1:11;
then w0.outDegree()+`1 c= w.outDegree()+`1 by CARD_2:83;
then A10: w.outDegree()+`1 = w0.outDegree()+`1 by A8, XBOOLE_0:def 10;
per cases by A7;
suppose A11: w0.outDegree() is infinite;
then A12: w.outDegree() is infinite by A9;
then 1 c= w.outDegree();
then A13: w.outDegree()+`1 = w.outDegree() by A12, CARD_2:76;
1 c= w0.outDegree() by A11;
hence thesis by A10, A11, A13, CARD_2:76;
end;
suppose w.outDegree() is finite;
then reconsider m=w0.outDegree(), n=w.outDegree() as Nat by A9;
m + 1 = m +` 1 .= n +` 1 by A10 .= n + 1;
hence thesis;
end;
end;
per cases by ORDINAL1:16;
suppose A14: v0.outDegree() +`1 c= v1.outDegree();
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
A15: w.outDegree() c= w0.outDegree() +`1 by GLIBPRE0:58;
w0.outDegree() c= v0.outDegree() & 1 c= 1 by A2;
then w0.outDegree() +`1 c= v0.outDegree() +`1 by CARD_2:83;
then w.outDegree() c= v0.outDegree() +`1 by A15, XBOOLE_1:1;
hence w.outDegree() c= v1.outDegree() by A14, XBOOLE_1:1;
end;
suppose w in {v};
hence w.outDegree() c= v1.outDegree() by TARSKI:def 1;
end;
end;
hence thesis;
end;
suppose A16: v1.outDegree() in v0.outDegree() +`1 &
v9.outDegree() = v0.outDegree() +`1;
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
A17: w.outDegree() c= w0.outDegree() +`1 by GLIBPRE0:58;
w0.outDegree() c= v0.outDegree() & 1 c= 1 by A2;
then w0.outDegree() +`1 c= v0.outDegree() +`1 by CARD_2:83;
hence w.outDegree() c= v9.outDegree() by A16, A17, XBOOLE_1:1;
end;
suppose w in {v};
then w = v1 by TARSKI:def 1;
hence w.outDegree() c= v9.outDegree() by A16, ORDINAL1:def 2;
end;
end;
hence thesis;
end;
suppose A18: v1.outDegree() in v0.outDegree() +`1 &
v9.outDegree() <> v0.outDegree() +`1 &
for w0 being Vertex of G, w being Vertex of H st w0 = w &
w.outDegree() = w0.outDegree() +`1
holds w0.outDegree() +`1 c= v0.outDegree();
then A19: v9.outDegree() = v0.outDegree() by A4;
now
let w be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose w in the_Vertices_of G;
then reconsider w0 = w as Vertex of G;
per cases;
suppose w.outDegree() = w0.outDegree() +`1;
hence w.outDegree() c= v9.outDegree() by A18, A19;
end;
suppose w.outDegree() <> w0.outDegree() +`1;
then w.outDegree() = w0.outDegree() by A4;
hence w.outDegree() c= v9.outDegree() by A2, A19;
end;
end;
suppose w in {v};
then w = v1 by TARSKI:def 1;
hence w.outDegree() c= v9.outDegree() by A18, A19, Lm7;
end;
end;
hence thesis;
end;
suppose A20: v1.outDegree() c= v0.outDegree() +`1 &
v9.outDegree() <> v0.outDegree() +`1 &
not for w0 being Vertex of G, w being Vertex of H st w0 = w &
w.outDegree() = w0.outDegree() +`1
holds w.outDegree() = w0.outDegree() +`1 &
w0.outDegree() +`1 c= v0.outDegree();
consider w0 being Vertex of G, w being Vertex of H such that
A21: w0 = w & w.outDegree() = w0.outDegree() +`1 and
A22: not w0.outDegree() +`1 c= v0.outDegree() by A20;
v0.outDegree() in w.outDegree() by A21, A22, ORDINAL1:16;
then v0.outDegree() c= w.outDegree() & v0.outDegree() <> w.outDegree()
by ORDINAL1:16;
then A23: v0.outDegree()+`1 c= w.outDegree() by Lm1;
now
let u be Vertex of H;
per cases by A3, XBOOLE_0:def 3;
suppose u in the_Vertices_of G;
then reconsider u0 = u as Vertex of G;
A24: u.outDegree() c= u0.outDegree()+`1 by GLIBPRE0:58;
u0.outDegree() c= v0.outDegree() & 1 c= 1 by A2;
then u0.outDegree()+`1 c= v0.outDegree()+`1 by CARD_2:83;
then u0.outDegree()+`1 c= w.outDegree() by A23, XBOOLE_1:1;
hence u.outDegree() c= w.outDegree() by A24, XBOOLE_1:1;
end;
suppose u in {v};
then u = v1 by TARSKI:def 1;
hence u.outDegree() c= w.outDegree() by A20, A23, XBOOLE_1:1;
end;
end;
hence thesis;
end;
end;
suppose not(not v in the_Vertices_of G & V c= the_Vertices_of G);
then G == H by GLIB_007:def 4;
hence thesis by Th85;
end;
end;
end;
:: registration
:: let G be without_max_degree _Graph, E be set;
:: cluster -> without_max_degree for reverseEdgeDirections of G, E;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_degree _Graph, V be set;
:: cluster -> without_max_degree for addVertices of G, V;
:: coherence;
:: cluster -> without_max_degree for addLoops of G, V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_degree _Graph, v,e,w be object;
:: cluster -> without_max_degree for addEdge of G,v,e,w;
:: coherence;
:: cluster -> without_max_degree for addAdjVertex of G,v,e,w;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_degree _Graph, v be object, V be set;
:: cluster -> without_max_degree for addAdjVertexAll of G,v,V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, E be set;
:: cluster -> without_max_in_degree for reverseEdgeDirections of G, E;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, V be set;
:: cluster -> without_max_in_degree for addVertices of G, V;
:: coherence;
:: cluster -> without_max_in_degree for addLoops of G, V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, v,e,w be object;
:: cluster -> without_max_in_degree for addEdge of G,v,e,w;
:: coherence;
:: cluster -> without_max_in_degree for addAdjVertex of G,v,e,w;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph, v be object, V be set;
:: cluster -> without_max_in_degree for addAdjVertexAll of G,v,V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, E be set;
:: cluster -> without_max_out_degree for reverseEdgeDirections of G, E;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, V be set;
:: cluster -> without_max_out_degree for addVertices of G, V;
:: coherence;
:: cluster -> without_max_out_degree for addLoops of G, V;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, v,e,w be object;
:: cluster -> without_max_out_degree for addEdge of G,v,e,w;
:: coherence;
:: cluster -> without_max_out_degree for addAdjVertex of G,v,e,w;
:: coherence;
:: end;
::
:: registration
:: let G be without_max_out_degree _Graph, v be object, V be set;
:: cluster -> without_max_out_degree for addAdjVertexAll of G,v,V;
:: coherence;
:: end;
theorem
for G being locally-finite with_max_degree _Graph, n being Nat
holds G.maxDegree() = n iff
ex v being Vertex of G st v.degree() = n &
for w being Vertex of G holds w.degree() <= v.degree()
proof
let G be locally-finite with_max_degree _Graph, n be Nat;
hereby
assume G.maxDegree() = n;
then consider v being Vertex of G such that
A1: v.degree() = n and
A2: for w being Vertex of G holds w.degree() c= v.degree() by Th79;
take v;
thus v.degree() = n by A1;
let w be Vertex of G;
Segm w.degree() c= Segm v.degree() by A2;
hence w.degree() <= v.degree() by NAT_1:39;
end;
given v being Vertex of G such that
A3: v.degree() = n and
A4: for w being Vertex of G holds w.degree() <= v.degree();
now
let w be Vertex of G;
Segm w.degree() c= Segm v.degree() by A4, NAT_1:39;
hence w.degree() c= v.degree();
end;
hence thesis by A3, Th48;
end;
theorem
for G being locally-finite with_max_in_degree _Graph, n being Nat
holds G.maxInDegree() = n iff
ex v being Vertex of G st v.inDegree() = n &
for w being Vertex of G holds w.inDegree() <= v.inDegree()
proof
let G be locally-finite with_max_in_degree _Graph, n be Nat;
hereby
assume G.maxInDegree() = n;
then consider v being Vertex of G such that
A1: v.inDegree() = n and
A2: for w being Vertex of G holds w.inDegree() c= v.inDegree() by Th80;
take v;
thus v.inDegree() = n by A1;
let w be Vertex of G;
Segm w.inDegree() c= Segm v.inDegree() by A2;
hence w.inDegree() <= v.inDegree() by NAT_1:39;
end;
given v being Vertex of G such that
A3: v.inDegree() = n and
A4: for w being Vertex of G holds w.inDegree() <= v.inDegree();
now
let w be Vertex of G;
Segm w.inDegree() c= Segm v.inDegree() by A4, NAT_1:39;
hence w.inDegree() c= v.inDegree();
end;
hence thesis by A3, Th49;
end;
theorem
for G being locally-finite with_max_out_degree _Graph, n being Nat
holds G.maxOutDegree() = n iff
ex v being Vertex of G st v.outDegree() = n &
for w being Vertex of G holds w.outDegree() <= v.outDegree()
proof
let G be locally-finite with_max_out_degree _Graph, n be Nat;
hereby
assume G.maxOutDegree() = n;
then consider v being Vertex of G such that
A1: v.outDegree() = n and
A2: for w being Vertex of G holds w.outDegree() c= v.outDegree()
by Th81;
take v;
thus v.outDegree() = n by A1;
let w be Vertex of G;
Segm w.outDegree() c= Segm v.outDegree() by A2;
hence w.outDegree() <= v.outDegree() by NAT_1:39;
end;
given v being Vertex of G such that
A3: v.outDegree() = n and
A4: for w being Vertex of G holds w.outDegree() <= v.outDegree();
now
let w be Vertex of G;
Segm w.outDegree() c= Segm v.outDegree() by A4, NAT_1:39;
hence w.outDegree() c= v.outDegree();
end;
hence thesis by A3, Th50;
end;
theorem
for c being Cardinal, G being _trivial c-edge _Graph holds
G.maxInDegree() = c & G.minInDegree() = c &
G.maxOutDegree() = c & G.minOutDegree() = c &
G.maxDegree() = c +` c & G.minDegree() = c +` c
proof
let c be Cardinal, G be _trivial c-edge _Graph;
set v = the Vertex of G;
now
let w be Vertex of G;
w.inDegree() = G.size() & v.inDegree() = G.size() by GLIB_000:149;
hence w.inDegree() c= v.inDegree();
end;
hence G.maxInDegree() = G.size() by Th49, GLIB_000:149
.= c by Def4;
now
let w be Vertex of G;
w.inDegree() = G.size() & v.inDegree() = G.size() by GLIB_000:149;
hence v.inDegree() c= w.inDegree();
end;
hence G.minInDegree() = G.size() by Th37, GLIB_000:149
.= c by Def4;
now
let w be Vertex of G;
w.outDegree() = G.size() & v.outDegree() = G.size() by GLIB_000:149;
hence w.outDegree() c= v.outDegree();
end;
hence G.maxOutDegree() = G.size() by Th50, GLIB_000:149
.= c by Def4;
now
let w be Vertex of G;
w.outDegree() = G.size() & v.outDegree() = G.size() by GLIB_000:149;
hence v.outDegree() c= w.outDegree();
end;
hence G.minOutDegree() = G.size() by Th38, GLIB_000:149
.= c by Def4;
now
let w be Vertex of G;
w.degree() = G.size()+`G.size() & v.degree() = G.size()+`G.size()
by GLIB_000:149;
hence w.degree() c= v.degree();
end;
hence G.maxDegree() = G.size()+`G.size() by Th48, GLIB_000:149
.= G.size() +` c by Def4
.= c +` c by Def4;
now
let w be Vertex of G;
w.degree() = G.size()+`G.size() & v.degree() = G.size()+`G.size()
by GLIB_000:149;
hence v.degree() c= w.degree();
end;
hence G.minDegree() = G.size()+`G.size() by Th36, GLIB_000:149
.= G.size() +` c by Def4
.= c +` c by Def4;
end;
definition
let G be _Graph, v be Vertex of G;
attr v is with_min_degree means
v.degree() = G.minDegree();
attr v is with_min_in_degree means
v.inDegree() = G.minInDegree();
attr v is with_min_out_degree means
v.outDegree() = G.minOutDegree();
attr v is with_max_degree means
v.degree() = G.supDegree();
attr v is with_max_in_degree means
v.inDegree() = G.supInDegree();
attr v is with_max_out_degree means
v.outDegree() = G.supOutDegree();
end;
theorem
for G being _Graph, v,w being Vertex of G st v is with_min_degree
holds v.degree() c= w.degree()
proof
let G be _Graph, v,w be Vertex of G;
assume v is with_min_degree;
then v.degree() = G.minDegree();
then consider v0 being Vertex of G such that
A1: v0.degree() = v.degree() and
A2: for u being Vertex of G holds v0.degree() c= u.degree() by Th36;
thus thesis by A1, A2;
end;
theorem Th92:
for G being _Graph, v,w being Vertex of G st v is with_min_in_degree
holds v.inDegree() c= w.inDegree()
proof
let G be _Graph, v,w be Vertex of G;
assume v is with_min_in_degree;
then v.inDegree() = G.minInDegree();
then consider v0 being Vertex of G such that
A1: v0.inDegree() = v.inDegree() and
A2: for u being Vertex of G holds v0.inDegree() c= u.inDegree() by Th37;
thus thesis by A1, A2;
end;
theorem Th93:
for G being _Graph, v,w being Vertex of G st v is with_min_out_degree
holds v.outDegree() c= w.outDegree()
proof
let G be _Graph, v,w be Vertex of G;
assume v is with_min_out_degree;
then v.outDegree() = G.minOutDegree();
then consider v0 being Vertex of G such that
A1: v0.outDegree() = v.outDegree() and
A2: for u being Vertex of G holds v0.outDegree() c= u.outDegree() by Th38;
thus thesis by A1, A2;
end;
theorem
for G being _Graph, v,w being Vertex of G st w is with_max_degree
holds v.degree() c= w.degree()
proof
let G be _Graph, v,w be Vertex of G;
assume w is with_max_degree;
then w.degree() = G.supDegree();
then consider v0 being Vertex of G such that
A1: v0.degree() = w.degree() and
A2: for u being Vertex of G holds u.degree() c= v0.degree()
by Th79, Lm3;
thus thesis by A1, A2;
end;
theorem Th95:
for G being _Graph, v,w being Vertex of G st w is with_max_in_degree
holds v.inDegree() c= w.inDegree()
proof
let G be _Graph, v,w be Vertex of G;
assume w is with_max_in_degree;
then w.inDegree() = G.supInDegree();
then consider v0 being Vertex of G such that
A1: v0.inDegree() = w.inDegree() and
A2: for u being Vertex of G holds u.inDegree() c= v0.inDegree()
by Th80, Lm4;
thus thesis by A1, A2;
end;
theorem Th96:
for G being _Graph, v,w being Vertex of G st w is with_max_out_degree
holds v.outDegree() c= w.outDegree()
proof
let G be _Graph, v,w be Vertex of G;
assume w is with_max_out_degree;
then w.outDegree() = G.supOutDegree();
then consider v0 being Vertex of G such that
A1: v0.outDegree() = w.outDegree() and
A2: for u being Vertex of G holds u.outDegree() c= v0.outDegree()
by Th81, Lm5;
thus thesis by A1, A2;
end;
registration
let G be _Graph;
cluster with_min_degree for Vertex of G;
existence
proof
consider v being Vertex of G such that
A1: v.degree() = G.minDegree() and
for w being Vertex of G holds v.degree() c= w.degree() by Th36;
take v;
thus thesis by A1;
end;
cluster with_min_in_degree for Vertex of G;
existence
proof
consider v being Vertex of G such that
A2: v.inDegree() = G.minInDegree() and
for w being Vertex of G holds v.inDegree() c= w.inDegree() by Th37;
take v;
thus thesis by A2;
end;
cluster with_min_out_degree for Vertex of G;
existence
proof
consider v being Vertex of G such that
A3: v.outDegree() = G.minOutDegree() and
for w being Vertex of G holds v.outDegree() c= w.outDegree() by Th38;
take v;
thus thesis by A3;
end;
cluster with_min_in_degree with_min_out_degree -> with_min_degree
for Vertex of G;
coherence
proof
let v be Vertex of G;
assume A4: v is with_min_in_degree with_min_out_degree;
now
let w be Vertex of G;
v.inDegree() c= w.inDegree() & v.outDegree() c= w.outDegree()
by A4, Th92, Th93;
hence v.degree() c= w.degree() by CARD_2:83;
end;
hence thesis by Th36;
end;
cluster with_max_in_degree with_max_out_degree -> with_max_degree
for Vertex of G;
coherence
proof
let w be Vertex of G;
assume A5: w is with_max_in_degree with_max_out_degree;
now
let v be Vertex of G;
v.inDegree() c= w.inDegree() & v.outDegree() c= w.outDegree()
by A5, Th95, Th96;
hence v.degree() c= w.degree() by CARD_2:83;
end;
hence thesis by Th48;
end;
cluster isolated -> with_min_degree with_min_in_degree
with_min_out_degree for Vertex of G;
coherence
proof
let v be Vertex of G;
assume A6: v is isolated;
then G.minDegree()=0 & G.minInDegree()=0 & G.minOutDegree()=0 by Th46;
hence thesis by A6, GLIB_000:156,157;
end;
end;
theorem Th97:
for G being _Graph holds G is with_max_degree iff
ex v being Vertex of G st v is with_max_degree
proof
let G be _Graph;
hereby
assume G is with_max_degree;
then consider v being Vertex of G such that
A1: v.degree() = G.supDegree() and
for w being Vertex of G holds w.degree() c= v.degree() by Th79;
take v;
thus v is with_max_degree by A1;
end;
thus thesis by Lm3;
end;
theorem Th98:
for G being _Graph holds G is with_max_in_degree iff
ex v being Vertex of G st v is with_max_in_degree
proof
let G be _Graph;
hereby
assume G is with_max_in_degree;
then consider v being Vertex of G such that
A1: v.inDegree() = G.supInDegree() and
for w being Vertex of G holds w.inDegree() c= v.inDegree() by Th80;
take v;
thus v is with_max_in_degree by A1;
end;
thus thesis by Lm4;
end;
theorem Th99:
for G being _Graph holds G is with_max_out_degree iff
ex v being Vertex of G st v is with_max_out_degree
proof
let G be _Graph;
hereby
assume G is with_max_out_degree;
then consider v being Vertex of G such that
A1: v.outDegree() = G.supOutDegree() and
for w being Vertex of G holds w.outDegree() c= v.outDegree() by Th81;
take v;
thus v is with_max_out_degree by A1;
end;
thus thesis by Lm5;
end;
registration
let G be with_max_degree _Graph;
cluster with_max_degree for Vertex of G;
existence by Th97;
end;
registration
let G be with_max_in_degree _Graph;
cluster with_max_in_degree for Vertex of G;
existence by Th98;
end;
registration
let G be with_max_out_degree _Graph;
cluster with_max_out_degree for Vertex of G;
existence by Th99;
end;
:: registration
:: let G be without_max_out_degree _Graph;
:: cluster -> non with_max_out_degree for Vertex of G;
:: coherence by Th125;
:: end;
::
:: registration
:: let G be without_max_degree _Graph;
:: cluster -> non with_max_degree for Vertex of G;
:: coherence by Th126;
:: end;
::
:: registration
:: let G be without_max_in_degree _Graph;
:: cluster -> non with_max_in_degree for Vertex of G;
:: coherence by Th127;
:: end;
:: added, SK 8.12.2024
theorem Th8:
for G being complete _Graph st 3 c= G.order() holds G is non acyclic
proof
let G be complete _Graph;
set u = the Vertex of G;
assume 3 c= G.order();
then consider v,w being object such that
A1: v in the_Vertices_of G & w in the_Vertices_of G and
A2: v <> u & w <> u & v <> w by SCMYCIEL:5;
reconsider v,w as Vertex of G by A1;
consider e1 being object such that
A3: e1 Joins u,v,G by A2, CHORD:def 3, CHORD:def 6;
consider e2 being object such that
A4: e2 Joins v,w,G by A2, CHORD:def 3, CHORD:def 6;
consider e3 being object such that
A5: e3 Joins w,u,G by A2, CHORD:def 3, CHORD:def 6;
set W1 = G.walkOf(u,e1,v), W2 = W1.addEdge(e2), W3 = W2.addEdge(e3);
A6: W1.first() = u & W1.last() = v by A3, GLIB_001:15;
then A7: W2.first() = u & W2.last() = w by A4, GLIB_001:63;
A9: W1 is open by A2, A6, GLIB_001:def 24;
W1.vertices() = {u,v} by A3, GLIB_001:91;
then not w in W1.vertices() by A2, TARSKI:def 2;
then A10: W2 is Path-like by A4, A6, A9, GLIB_001:151;
A11: W2 is open by A2, A7, GLIB_001:def 24;
len W2 = len W1 + 2 by A4, A6, GLIB_001:64
.= 3 + 2 by A3, GLIB_001:14;
then W3 is Cycle-like by A5, A7, A10, A11, CHORD:33;
hence G is non acyclic by GLIB_002:def 2;
end;
registration
let n be Nat;
cluster (n+3)-vertex complete -> non acyclic for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is (n+3)-vertex complete;
3+0 <= 3+n by XREAL_1:6;
then 3 c= n+3 by FIELD_5:3;
hence thesis by A1, Th8;
end;
end;
theorem
for G being _Graph, n being Nat
st for v being Vertex of G holds v.degree() c= n
holds G is with_max_degree
proof
let G be _Graph, n be Nat;
assume A1: for v being Vertex of G holds v.degree() c= n;
defpred P[Nat] means ex v being Vertex of G st v.degree() = $1;
A2: for k being Nat st P[k] holds k <= n
proof
let k be Nat;
given v being Vertex of G such that
A3: v.degree() = k;
Segm k c= Segm n by A1, A3;
hence thesis by NAT_1:39;
end;
A4: ex k being Nat st P[k]
proof
set v = the Vertex of G;
v.degree() is finite by A1, FINSET_1:1;
then reconsider k = v.degree() as Nat;
take k,v;
thus thesis;
end;
consider k being Nat such that
A5: P[k] & for i being Nat st P[i] holds i <= k from NAT_1:sch 6(A2,A4);
consider v being Vertex of G such that
A6: v.degree() = k by A5;
now
let w be Vertex of G;
w.degree() is finite by A1, FINSET_1:1;
then reconsider i = w.degree() as Nat;
Segm i c= Segm k by A5, NAT_1:39;
hence w.degree() c= v.degree() by A6;
end;
hence thesis;
end;
theorem
for G being _Graph, n being Nat
st for v being Vertex of G holds v.inDegree() c= n
holds G is with_max_in_degree
proof
let G be _Graph, n be Nat;
assume A1: for v being Vertex of G holds v.inDegree() c= n;
defpred P[Nat] means ex v being Vertex of G st v.inDegree() = $1;
A2: for k being Nat st P[k] holds k <= n
proof
let k be Nat;
given v being Vertex of G such that
A3: v.inDegree() = k;
Segm k c= Segm n by A1, A3;
hence thesis by NAT_1:39;
end;
A4: ex k being Nat st P[k]
proof
set v = the Vertex of G;
v.inDegree() is finite by A1, FINSET_1:1;
then reconsider k = v.inDegree() as Nat;
take k,v;
thus thesis;
end;
consider k being Nat such that
A5: P[k] & for i being Nat st P[i] holds i <= k from NAT_1:sch 6(A2,A4);
consider v being Vertex of G such that
A6: v.inDegree() = k by A5;
now
let w be Vertex of G;
w.inDegree() is finite by A1, FINSET_1:1;
then reconsider i = w.inDegree() as Nat;
Segm i c= Segm k by A5, NAT_1:39;
hence w.inDegree() c= v.inDegree() by A6;
end;
hence thesis;
end;
theorem
for G being _Graph, n being Nat
st for v being Vertex of G holds v.outDegree() c= n
holds G is with_max_out_degree
proof
let G be _Graph, n be Nat;
assume A1: for v being Vertex of G holds v.outDegree() c= n;
defpred P[Nat] means ex v being Vertex of G st v.outDegree() = $1;
A2: for k being Nat st P[k] holds k <= n
proof
let k be Nat;
given v being Vertex of G such that
A3: v.outDegree() = k;
Segm k c= Segm n by A1, A3;
hence thesis by NAT_1:39;
end;
A4: ex k being Nat st P[k]
proof
set v = the Vertex of G;
v.outDegree() is finite by A1, FINSET_1:1;
then reconsider k = v.outDegree() as Nat;
take k,v;
thus thesis;
end;
consider k being Nat such that
A5: P[k] & for i being Nat st P[i] holds i <= k from NAT_1:sch 6(A2,A4);
consider v being Vertex of G such that
A6: v.outDegree() = k by A5;
now
let w be Vertex of G;
w.outDegree() is finite by A1, FINSET_1:1;
then reconsider i = w.outDegree() as Nat;
Segm i c= Segm k by A5, NAT_1:39;
hence w.outDegree() c= v.outDegree() by A6;
end;
hence thesis;
end;
registration
cluster edge-finite connected -> vertex-finite _finite for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is edge-finite connected;
thus G is vertex-finite
proof
assume G is non vertex-finite;
then reconsider G9 = G as non vertex-finite edge-finite _Graph by A1;
set v = the isolated Vertex of G9;
{v} = G9.reachableFrom(v) by GLIB_006:51
.= the_Vertices_of G9 by A1, GLIB_002:16;
hence contradiction;
end;
hence thesis by A1;
end;
end;
registration
let G be edgeless _Graph;
cluster G.minDegree() -> zero;
coherence
proof
now
take v = the Vertex of G;
thus v.degree() = 0;
let w be Vertex of G;
thus v.degree() c= w.degree();
end;
hence thesis by Th36;
end;
cluster G.minInDegree() -> zero;
coherence
proof
now
take v = the Vertex of G;
thus v.inDegree() = 0;
let w be Vertex of G;
thus v.inDegree() c= w.inDegree();
end;
hence thesis by Th37;
end;
cluster G.minOutDegree() -> zero;
coherence
proof
now
take v = the Vertex of G;
thus v.outDegree() = 0;
let w be Vertex of G;
thus v.outDegree() c= w.outDegree();
end;
hence thesis by Th38;
end;
cluster G.supDegree() -> zero;
coherence
proof
now
take v = the Vertex of G;
thus v.degree() = 0;
let w be Vertex of G;
thus w.degree() c= v.degree();
end;
hence thesis by Th48;
end;
cluster G.supInDegree() -> zero;
coherence
proof
now
take v = the Vertex of G;
thus v.inDegree() = 0;
let w be Vertex of G;
thus w.inDegree() c= v.inDegree();
end;
hence thesis by Th49;
end;
cluster G.supOutDegree() -> zero;
coherence
proof
now
take v = the Vertex of G;
thus v.outDegree() = 0;
let w be Vertex of G;
thus w.outDegree() c= v.outDegree();
end;
hence thesis by Th50;
end;
end;
theorem
for G being _Graph, C being Component of G holds
G.minDegree() c= C.minDegree() &
G.minInDegree() c= C.minInDegree() &
G.minOutDegree() c= C.minOutDegree()
proof
let G be _Graph, C being Component of G;
A1: the_Vertices_of C c= the_Vertices_of G;
thus G.minDegree() c= C.minDegree()
proof
set A = the set of all v.degree() where v is Vertex of G;
set B = the set of all w.degree() where w is Vertex of C;
A2: B <> {}
proof
set w = the Vertex of C;
w.degree() in B;
hence thesis;
end;
now
let x be object;
assume x in B;
then consider w being Vertex of C such that
A3: x = w.degree();
reconsider v = w as Vertex of G by A1, TARSKI:def 3;
x = v.degree() by A3, GLIBPRE0:44;
hence x in A;
end;
then meet A c= meet B by A2, SETFAM_1:6, TARSKI:def 3;
then G.minDegree() c= meet B;
hence thesis;
end;
thus G.minInDegree() c= C.minInDegree()
proof
set A = the set of all v.inDegree() where v is Vertex of G;
set B = the set of all w.inDegree() where w is Vertex of C;
A4: B <> {}
proof
set w = the Vertex of C;
w.inDegree() in B;
hence thesis;
end;
now
let x be object;
assume x in B;
then consider w being Vertex of C such that
A5: x = w.inDegree();
reconsider v = w as Vertex of G by A1, TARSKI:def 3;
x = v.inDegree() by A5, GLIBPRE0:44;
hence x in A;
end;
then meet A c= meet B by A4, SETFAM_1:6, TARSKI:def 3;
then G.minInDegree() c= meet B;
hence thesis;
end;
thus G.minOutDegree() c= C.minOutDegree()
proof
set A = the set of all v.outDegree() where v is Vertex of G;
set B = the set of all w.outDegree() where w is Vertex of C;
A6: B <> {}
proof
set w = the Vertex of C;
w.outDegree() in B;
hence thesis;
end;
now
let x be object;
assume x in B;
then consider w being Vertex of C such that
A7: x = w.outDegree();
reconsider v = w as Vertex of G by A1, TARSKI:def 3;
x = v.outDegree() by A7, GLIBPRE0:44;
hence x in A;
end;
then meet A c= meet B by A6, SETFAM_1:6, TARSKI:def 3;
then G.minOutDegree() c= meet B;
hence thesis;
end;
end;