:: Refined Finiteness and Degree properties in Graphs
:: by Sebastian Koch
::
:: Received May 19, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


theorem Th1: :: GLIB_013:1
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 end;

theorem Th2: :: GLIB_013:2
for G being non-Dmulti _Graph holds G .size() c= (G .order()) *` (G .order())
proof end;

theorem Th3: :: GLIB_013:3
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 end;

theorem Th4: :: GLIB_013:4
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 end;

theorem Th5: :: GLIB_013:5
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 end;

definition
let G be _Graph;
attr G is vertex-finite means :Def1: :: GLIB_013:def 1
 the_Vertices_of G is finite ;
attr G is edge-finite means :Def2: :: GLIB_013:def 2
 the_Edges_of G is finite ;
end;

:: deftheorem Def1 defines vertex-finite GLIB_013:def 1 :
for G being _Graph holds
( G is vertex-finite iff the_Vertices_of G is finite );

:: deftheorem Def2 defines edge-finite GLIB_013:def 2 :
for G being _Graph holds
( G is edge-finite iff the_Edges_of G is finite );

theorem Th6: :: GLIB_013:6
for G being _Graph holds
( G is vertex-finite iff G .order() is finite ) ;

theorem Th7: :: GLIB_013:7
for G being _Graph holds
( G is edge-finite iff G .size() is finite ) ;

theorem Th8: :: GLIB_013:8
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 ;
let E be set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) -> vertex-finite ;
coherence
createGraph (V,E,S,T) is vertex-finite ;
end;

registration
let V be infinite set ;
let E be set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) -> non vertex-finite ;
coherence
not createGraph (V,E,S,T) is vertex-finite ;
end;

registration
let V be non empty set ;
let E be finite set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) -> edge-finite ;
coherence
createGraph (V,E,S,T) is edge-finite ;
end;

registration
let V be non empty set ;
let E be infinite set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) -> non edge-finite ;
coherence
not createGraph (V,E,S,T) is edge-finite ;
end;

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] _finite -> vertex-finite edge-finite for set ;
coherence
for b1 being _Graph st b1 is _finite holds
( b1 is vertex-finite & b1 is edge-finite ) ;
cluster Relation-like omega -defined Function-like finite [Graph-like] vertex-finite edge-finite -> _finite for set ;
coherence
for b1 being _Graph st b1 is vertex-finite & b1 is edge-finite holds
b1 is _finite by GLIB_000:def 17;
cluster Relation-like omega -defined Function-like finite [Graph-like] edgeless -> edge-finite for set ;
coherence
for b1 being _Graph st b1 is edgeless holds
b1 is edge-finite ;
cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial -> vertex-finite for set ;
coherence
for b1 being _Graph st b1 is _trivial holds
b1 is vertex-finite ;
cluster Relation-like omega -defined Function-like finite [Graph-like] non-Dmulti vertex-finite -> edge-finite for set ;
coherence
for b1 being _Graph st b1 is vertex-finite & b1 is non-Dmulti holds
b1 is edge-finite
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] loopfull non vertex-finite -> non edge-finite for set ;
coherence
for b1 being _Graph st not b1 is vertex-finite & b1 is loopfull holds
not b1 is edge-finite
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] simple vertex-finite edge-finite for set ;
existence
ex b1 being _Graph st
( b1 is vertex-finite & b1 is edge-finite & b1 is simple )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] vertex-finite non edge-finite for set ;
existence
ex b1 being _Graph st
( b1 is vertex-finite & not b1 is edge-finite )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] non vertex-finite edge-finite for set ;
existence
ex b1 being _Graph st
( not b1 is vertex-finite & b1 is edge-finite )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] non vertex-finite non edge-finite for set ;
existence
ex b1 being _Graph st
( not b1 is vertex-finite & not b1 is edge-finite )
proof end;
end;

registration
let G be vertex-finite _Graph;
cluster G .order() -> natural non zero ;
coherence
( not G .order() is zero & G .order() is natural )
proof end;
end;

definition
let G be vertex-finite _Graph;
:: original: .order()
redefine func G .order() -> non zero Nat;
coherence
G .order() is non zero Nat ;
end;

registration
let G be edge-finite _Graph;
cluster G .size() -> natural ;
coherence
G .size() is natural
proof end;
end;

definition
let G be edge-finite _Graph;
:: original: .size()
redefine func G .size() -> Nat;
coherence
G .size() is Nat ;
end;

theorem :: GLIB_013:9
for G being non-Dmulti vertex-finite _Graph holds G .size() <= (G .order()) ^2
proof end;

theorem :: GLIB_013:10
for G being Dsimple vertex-finite _Graph holds G .size() <= ((G .order()) ^2) - (G .order())
proof end;

theorem :: GLIB_013:11
for G being non-multi vertex-finite _Graph holds G .size() <= (((G .order()) ^2) + (G .order())) / 2
proof end;

theorem :: GLIB_013:12
for G being simple vertex-finite _Graph holds G .size() <= (((G .order()) ^2) - (G .order())) / 2
proof end;

registration
let G be vertex-finite _Graph;
cluster the_Vertices_of G -> finite ;
coherence
the_Vertices_of G is finite by Def1;
cluster -> vertex-finite for Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is vertex-finite
proof end;
cluster -> vertex-finite edge-finite for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds
( b1 is vertex-finite & b1 is edge-finite )
proof end;
cluster -> vertex-finite edge-finite for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds
( b1 is vertex-finite & b1 is edge-finite )
proof end;
cluster -> vertex-finite edge-finite for DGraphComplement of G;
coherence
for b1 being DGraphComplement of G holds
( b1 is vertex-finite & b1 is edge-finite )
proof end;
cluster -> vertex-finite edge-finite for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds
( b1 is vertex-finite & b1 is edge-finite )
proof end;
let V be finite set ;
cluster -> vertex-finite for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is vertex-finite
proof end;
end;

registration
let G be vertex-finite _Graph;
let v be object ;
cluster -> vertex-finite for addVertices of G,{v};
coherence
for b1 being addVertex of G,v holds b1 is vertex-finite ;
let e, w be object ;
cluster -> vertex-finite for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is vertex-finite
proof end;
cluster -> vertex-finite for addAdjVertex of G,v,e,w;
coherence
for b1 being addAdjVertex of G,v,e,w holds b1 is vertex-finite
proof end;
end;

registration
let G be vertex-finite _Graph;
let E be set ;
cluster -> vertex-finite for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is vertex-finite
proof end;
end;

registration
let G be vertex-finite _Graph;
let v be object ;
let V be set ;
cluster -> vertex-finite for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds b1 is vertex-finite
proof end;
end;

registration
let G be vertex-finite _Graph;
let V be set ;
cluster -> vertex-finite for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is vertex-finite
proof end;
end;

registration
let G be _Graph;
let V be infinite set ;
cluster -> non vertex-finite for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds not b1 is vertex-finite
proof end;
end;

registration
let G be non vertex-finite _Graph;
cluster the_Vertices_of G -> infinite ;
coherence
not the_Vertices_of G is finite by Def1;
cluster -> non vertex-finite for Supergraph of G;
coherence
for b1 being Supergraph of G holds not b1 is vertex-finite
proof end;
cluster spanning -> non vertex-finite for Subgraph of G;
coherence
for b1 being Subgraph of G st b1 is spanning holds
not b1 is vertex-finite
proof end;
cluster -> non vertex-finite for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds not b1 is vertex-finite
proof end;
cluster -> non vertex-finite for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds not b1 is vertex-finite
proof end;
cluster -> non vertex-finite for DGraphComplement of G;
coherence
for b1 being DGraphComplement of G holds not b1 is vertex-finite
proof end;
cluster -> non vertex-finite for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds not b1 is vertex-finite
proof end;
let V be infinite set ;
let E be set ;
cluster -> non vertex-finite for inducedSubgraph of G,V,E;
coherence
for b1 being inducedSubgraph of G,V,E holds not b1 is vertex-finite
proof end;
end;

registration
let G be non vertex-finite _Graph;
let V be infinite Subset of (the_Vertices_of G);
cluster -> non edge-finite for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds not b1 is edge-finite
proof end;
end;

registration
let G be edge-finite _Graph;
cluster the_Edges_of G -> finite ;
coherence
the_Edges_of G is finite by Def2;
cluster -> edge-finite for Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is edge-finite
proof end;
let V be set ;
cluster -> edge-finite for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is edge-finite
proof end;
end;

registration
let G be edge-finite _Graph;
let E be set ;
cluster -> edge-finite for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is edge-finite
proof end;
end;

registration
let G be edge-finite _Graph;
let v be object ;
cluster -> edge-finite for addVertices of G,{v};
coherence
for b1 being addVertex of G,v holds b1 is edge-finite ;
let e, w be object ;
cluster -> edge-finite for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is edge-finite
proof end;
cluster -> edge-finite for addAdjVertex of G,v,e,w;
coherence
for b1 being addAdjVertex of G,v,e,w holds b1 is edge-finite
proof end;
end;

registration
let G be edge-finite _Graph;
let v be object ;
let V be finite set ;
cluster -> edge-finite for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds b1 is edge-finite
proof end;
end;

registration
let G be edge-finite _Graph;
let V be finite Subset of (the_Vertices_of G);
cluster -> edge-finite for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is edge-finite
proof end;
end;

registration
let G be non vertex-finite edge-finite _Graph;
cluster isolated for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is isolated
proof end;
end;

registration
let G be non vertex-finite edge-finite _Graph;
cluster -> non edge-finite for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds not b1 is edge-finite
proof end;
cluster -> non edge-finite for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds not b1 is edge-finite
proof end;
cluster -> non edge-finite for DGraphComplement of G;
coherence
for b1 being DGraphComplement of G holds not b1 is edge-finite
proof end;
cluster -> non edge-finite for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds not b1 is edge-finite
proof end;
end;

registration
let G be non edge-finite _Graph;
cluster the_Edges_of G -> infinite ;
coherence
not the_Edges_of G is finite by Def2;
cluster -> non edge-finite for Supergraph of G;
coherence
for b1 being Supergraph of G holds not b1 is edge-finite
proof end;
let V be set ;
let E be infinite Subset of (the_Edges_of G);
cluster -> non edge-finite for inducedSubgraph of G,V,E;
coherence
for b1 being inducedSubgraph of G,V,E holds not b1 is edge-finite
proof end;
end;

registration
let G be non edge-finite _Graph;
let E be finite set ;
cluster -> non edge-finite for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
coherence
for b1 being removeEdges of G,E holds not b1 is edge-finite ;
end;

registration
let G be non edge-finite _Graph;
let e be set ;
cluster -> non edge-finite for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};
coherence
for b1 being removeEdge of G,e holds not b1 is edge-finite ;
end;

theorem Th13: :: GLIB_013:13
for G1, G2 being _Graph
for 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 end;

theorem Th14: :: GLIB_013:14
for G1, G2 being _Graph
for 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 end;

theorem :: GLIB_013:15
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( ( G1 is vertex-finite implies G2 is vertex-finite ) & ( G2 is vertex-finite implies G1 is vertex-finite ) & ( G1 is edge-finite implies G2 is edge-finite ) & ( G2 is edge-finite implies G1 is edge-finite ) ) by Th13, Th14;

definition
let c be Cardinal;
let G be _Graph;
attr G is c -vertex means :Def3: :: GLIB_013:def 3
G .order() = c;
attr G is c -edge means :Def4: :: GLIB_013:def 4
G .size() = c;
end;

:: deftheorem Def3 defines -vertex GLIB_013:def 3 :
for c being Cardinal
for G being _Graph holds
( G is c -vertex iff G .order() = c );

:: deftheorem Def4 defines -edge GLIB_013:def 4 :
for c being Cardinal
for G being _Graph holds
( G is c -edge iff G .size() = c );

theorem :: GLIB_013:16
for G being _Graph holds
( G is vertex-finite iff ex n being non zero Nat st G is n -vertex )
proof end;

theorem :: GLIB_013:17
for G being _Graph holds
( G is edge-finite iff ex n being Nat st G is n -edge )
proof end;

theorem Th18: :: GLIB_013:18
for G1, G2 being _Graph
for c being Cardinal st the_Vertices_of G1 = the_Vertices_of G2 & G1 is c -vertex holds
G2 is c -vertex ;

theorem Th19: :: GLIB_013:19
for G1, G2 being _Graph
for c being Cardinal st the_Edges_of G1 = the_Edges_of G2 & G1 is c -edge holds
G2 is c -edge ;

theorem Th20: :: GLIB_013:20
for G1, G2 being _Graph
for 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 :: GLIB_013:21
for G being _Graph holds
( G is G .order() -vertex & G is G .size() -edge ) ;

registration
let V be non empty set ;
let E be set ;
let S, T be Function of E,V;
cluster createGraph (V,E,S,T) -> card V -vertex card E -edge ;
coherence
( createGraph (V,E,S,T) is card V -vertex & createGraph (V,E,S,T) is card E -edge ) ;
end;

registration
let a be non zero Cardinal;
let b be Cardinal;
cluster Relation-like omega -defined Function-like finite [Graph-like] a -vertex b -edge for set ;
existence
ex b1 being _Graph st
( b1 is a -vertex & b1 is b -edge )
proof end;
end;

registration
let c be Cardinal;
cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial c -edge for set ;
existence
ex b1 being _Graph st
( b1 is _trivial & b1 is c -edge )
proof end;
end;

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] -> non 0 -vertex for set ;
coherence
for b1 being _Graph holds not b1 is 0 -vertex ;
cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial -> 1 -vertex for set ;
coherence
for b1 being _Graph st b1 is _trivial holds
b1 is 1 -vertex by GLIB_000:def 19;
cluster Relation-like omega -defined Function-like finite [Graph-like] 1 -vertex -> _trivial for set ;
coherence
for b1 being _Graph st b1 is 1 -vertex holds
b1 is _trivial by GLIB_000:def 19;
let n be non zero Nat;
cluster Relation-like omega -defined Function-like finite [Graph-like] n -vertex -> vertex-finite for set ;
coherence
for b1 being _Graph st b1 is n -vertex holds
b1 is vertex-finite ;
end;

registration
let c be non zero Cardinal;
let G be c -vertex _Graph;
cluster spanning -> c -vertex for Subgraph of G;
coherence
for b1 being Subgraph of G st b1 is spanning holds
b1 is c -vertex
proof end;
cluster -> c -vertex for DLGraphComplement of G;
coherence
for b1 being DLGraphComplement of G holds b1 is c -vertex
proof end;
cluster -> c -vertex for LGraphComplement of G;
coherence
for b1 being LGraphComplement of G holds b1 is c -vertex
proof end;
cluster -> c -vertex for DGraphComplement of G;
coherence
for b1 being DGraphComplement of G holds b1 is c -vertex
proof end;
cluster -> c -vertex for GraphComplement of G;
coherence
for b1 being GraphComplement of G holds b1 is c -vertex
proof end;
let E be set ;
cluster -> c -vertex for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is c -vertex
proof end;
end;

registration
let c be non zero Cardinal;
let G be c -vertex _Graph;
let V be set ;
cluster -> c -vertex for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is c -vertex
proof end;
end;

registration
let c be non zero Cardinal;
let G be c -vertex _Graph;
let v, e, w be object ;
cluster -> c -vertex for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is c -vertex
proof end;
end;

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] edgeless -> 0 -edge for set ;
coherence
for b1 being _Graph st b1 is edgeless holds
b1 is 0 -edge ;
cluster Relation-like omega -defined Function-like finite [Graph-like] 0 -edge -> edgeless for set ;
coherence
for b1 being _Graph st b1 is 0 -edge holds
b1 is edgeless ;
let n be Nat;
cluster Relation-like omega -defined Function-like finite [Graph-like] n -edge -> edge-finite for set ;
coherence
for b1 being _Graph st b1 is n -edge holds
b1 is edge-finite ;
end;

registration
let c be Cardinal;
let G be c -edge _Graph;
let E be set ;
cluster -> c -edge for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is c -edge
proof end;
end;

registration
let c be Cardinal;
let G be c -edge _Graph;
let V be set ;
cluster -> c -edge for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is c -edge
proof end;
end;

theorem :: GLIB_013:22
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2
for c being Cardinal st F is isomorphism holds
( ( G1 is c -vertex implies G2 is c -vertex ) & ( G2 is c -vertex implies G1 is c -vertex ) & ( G1 is c -edge implies G2 is c -edge ) & ( G2 is c -edge implies G1 is c -edge ) ) by GLIB_010:84;

definition
let G be _Graph;
attr G is locally-finite means :Def5: :: GLIB_013:def 5
 for v being Vertex of G holds v .edgesInOut() is finite ;
end;

:: deftheorem Def5 defines locally-finite GLIB_013:def 5 :
for G being _Graph holds
( G is locally-finite iff for v being Vertex of G holds v .edgesInOut() is finite );

theorem Th23: :: GLIB_013:23
for G being _Graph holds
( G is locally-finite iff for v being Vertex of G holds v .degree() is finite )
proof end;

theorem Th24: :: GLIB_013:24
for G1, G2 being _Graph st G1 == G2 & G1 is locally-finite holds
G2 is locally-finite
proof end;

theorem Th25: :: GLIB_013:25
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 end;

theorem :: GLIB_013:26
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 end;

theorem :: GLIB_013:27
for V being non empty set
for E being set
for 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 end;

theorem :: GLIB_013:28
for V being non empty set
for E being set
for 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
not createGraph (V,E,S,T) is locally-finite
proof 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
for b1 being addAdjVertexAll of G, the_Vertices_of G,V holds not b1 is locally-finite
proof end;
end;

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] edge-finite -> locally-finite for set ;
coherence
for b1 being _Graph st b1 is edge-finite holds
b1 is locally-finite ;
cluster Relation-like omega -defined Function-like finite [Graph-like] non 0 -vertex locally-finite for set ;
existence
ex b1 being _Graph st b1 is locally-finite
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] non 0 -vertex non locally-finite for set ;
existence
not for b1 being _Graph holds b1 is locally-finite
proof end;
end;

registration
let G be locally-finite _Graph;
cluster -> locally-finite for Subgraph of G;
coherence
for b1 being Subgraph of G holds b1 is locally-finite
proof end;
let X be finite set ;
cluster G .edgesInto X -> finite ;
coherence
G .edgesInto X is finite
proof end;
cluster G .edgesOutOf X -> finite ;
coherence
G .edgesOutOf X is finite
proof end;
cluster G .edgesInOut X -> finite ;
coherence
G .edgesInOut X is finite ;
cluster G .edgesBetween X -> finite ;
coherence
G .edgesBetween X is finite ;
let Y be finite set ;
cluster G .edgesBetween (X,Y) -> finite ;
coherence
G .edgesBetween (X,Y) is finite
proof end;
cluster G .edgesDBetween (X,Y) -> finite ;
coherence
G .edgesDBetween (X,Y) is finite
proof end;
end;

registration
let G be locally-finite _Graph;
let v be Vertex of G;
cluster v .edgesIn() -> finite ;
coherence
v .edgesIn() is finite ;
cluster v .edgesOut() -> finite ;
coherence
v .edgesOut() is finite ;
cluster v .edgesInOut() -> finite ;
coherence
v .edgesInOut() is finite ;
cluster v .inDegree() -> finite ;
coherence
v .inDegree() is finite ;
cluster v .outDegree() -> finite ;
coherence
v .outDegree() is finite ;
cluster v .degree() -> finite ;
coherence
v .degree() is finite ;
end;

definition
let G be locally-finite _Graph;
let v be Vertex of G;
:: original: .inDegree()
redefine func v .inDegree() -> Nat;
coherence
v .inDegree() is Nat ;
:: original: .outDegree()
redefine func v .outDegree() -> Nat;
coherence
v .outDegree() is Nat ;
:: original: .degree()
redefine func v .degree() -> Nat;
coherence
v .degree() is Nat ;
end;

registration
let G be locally-finite _Graph;
let V be set ;
cluster -> locally-finite for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is locally-finite
proof end;
cluster -> locally-finite for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is locally-finite
proof end;
end;

registration
let G be locally-finite _Graph;
let E be set ;
cluster -> locally-finite for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is locally-finite
proof 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
for b1 being addEdge of G,v,e,w holds b1 is locally-finite
proof end;
cluster -> locally-finite for addAdjVertex of G,v,e,w;
coherence
for b1 being addAdjVertex of G,v,e,w holds b1 is locally-finite
proof end;
end;

theorem Th29: :: GLIB_013:29
for G2 being _Graph
for v being object
for 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 end;

registration
let G be locally-finite _Graph;
let v be object ;
let V be finite set ;
cluster -> locally-finite for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds b1 is locally-finite
proof end;
end;

registration
let G be non locally-finite _Graph;
cluster -> non locally-finite for Supergraph of G;
coherence
for b1 being Supergraph of G holds not b1 is locally-finite
proof end;
let E be finite set ;
cluster -> non locally-finite for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ E;
coherence
for b1 being removeEdges of G,E holds not b1 is locally-finite
proof end;
end;

registration
let G be non locally-finite _Graph;
let e be set ;
cluster -> non locally-finite for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ {e};
coherence
for b1 being removeEdge of G,e holds not b1 is locally-finite ;
end;

theorem Th30: :: GLIB_013:30
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
not G2 is locally-finite
proof end;

theorem :: GLIB_013:31
for G1 being non locally-finite _Graph
for v being Vertex of G1
for G2 being removeVertex of G1,v st v .edgesInOut() is finite holds
not G2 is locally-finite
proof end;

theorem Th32: :: GLIB_013:32
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is locally-finite holds
G1 is locally-finite
proof end;

theorem :: GLIB_013:33
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous & G1 is locally-finite holds
G2 is locally-finite
proof end;

theorem :: GLIB_013:34
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is locally-finite iff G2 is locally-finite )
proof end;

definition
let G be _Graph;
func G .supDegree() -> Cardinal equals :: GLIB_013:def 6
 union { (v .degree()) where v is Vertex of G : verum } ;
coherence
union { (v .degree()) where v is Vertex of G : verum } is Cardinal
proof end;
func G .supInDegree() -> Cardinal equals :: GLIB_013:def 7
 union { (v .inDegree()) where v is Vertex of G : verum } ;
coherence
union { (v .inDegree()) where v is Vertex of G : verum } is Cardinal
proof end;
func G .supOutDegree() -> Cardinal equals :: GLIB_013:def 8
 union { (v .outDegree()) where v is Vertex of G : verum } ;
coherence
union { (v .outDegree()) where v is Vertex of G : verum } is Cardinal
proof end;
func G .minDegree() -> Cardinal equals :: GLIB_013:def 9
 meet { (v .degree()) where v is Vertex of G : verum } ;
coherence
meet { (v .degree()) where v is Vertex of G : verum } is Cardinal
proof end;
func G .minInDegree() -> Cardinal equals :: GLIB_013:def 10
 meet { (v .inDegree()) where v is Vertex of G : verum } ;
coherence
meet { (v .inDegree()) where v is Vertex of G : verum } is Cardinal
proof end;
func G .minOutDegree() -> Cardinal equals :: GLIB_013:def 11
 meet { (v .outDegree()) where v is Vertex of G : verum } ;
coherence
meet { (v .outDegree()) where v is Vertex of G : verum } is Cardinal
proof end;
end;

:: deftheorem defines .supDegree() GLIB_013:def 6 :
for G being _Graph holds G .supDegree() = union { (v .degree()) where v is Vertex of G : verum } ;

:: deftheorem defines .supInDegree() GLIB_013:def 7 :
for G being _Graph holds G .supInDegree() = union { (v .inDegree()) where v is Vertex of G : verum } ;

:: deftheorem defines .supOutDegree() GLIB_013:def 8 :
for G being _Graph holds G .supOutDegree() = union { (v .outDegree()) where v is Vertex of G : verum } ;

:: deftheorem defines .minDegree() GLIB_013:def 9 :
for G being _Graph holds G .minDegree() = meet { (v .degree()) where v is Vertex of G : verum } ;

:: deftheorem defines .minInDegree() GLIB_013:def 10 :
for G being _Graph holds G .minInDegree() = meet { (v .inDegree()) where v is Vertex of G : verum } ;

:: deftheorem defines .minOutDegree() GLIB_013:def 11 :
for G being _Graph holds G .minOutDegree() = meet { (v .outDegree()) where v is Vertex of G : verum } ;

theorem Th35: :: GLIB_013:35
for G being _Graph
for 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 end;

theorem Th36: :: GLIB_013:36
for G being _Graph
for 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 end;

theorem Th37: :: GLIB_013:37
for G being _Graph
for 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 end;

theorem Th38: :: GLIB_013:38
for G being _Graph
for 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 end;

theorem Th39: :: GLIB_013:39
for G being _Graph holds G .supInDegree() c= G .supDegree()
proof end;

theorem Th40: :: GLIB_013:40
for G being _Graph holds G .supOutDegree() c= G .supDegree()
proof end;

theorem :: GLIB_013:41
for G being _Graph holds G .minInDegree() c= G .minDegree()
proof end;

theorem :: GLIB_013:42
for G being _Graph holds G .minOutDegree() c= G .minDegree()
proof end;

theorem :: GLIB_013:43
for G being _Graph holds G .minDegree() c= G .supDegree() by SETFAM_1:2;

theorem :: GLIB_013:44
for G being _Graph holds G .minInDegree() c= G .supInDegree() by SETFAM_1:2;

theorem :: GLIB_013:45
for G being _Graph holds G .minOutDegree() c= G .supOutDegree() by SETFAM_1:2;

theorem Th46: :: GLIB_013:46
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 end;

theorem :: GLIB_013:47
for G being _Graph st G .minDegree() = 0 holds
ex v being Vertex of G st v is isolated
proof 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: :: GLIB_013:48
for G being _Graph
for 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 end;

theorem Th49: :: GLIB_013:49
for G being _Graph
for 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 end;

theorem Th50: :: GLIB_013:50
for G being _Graph
for 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 end;

theorem Th51: :: GLIB_013:51
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .supDegree() c= G2 .supDegree()
proof end;

theorem Th52: :: GLIB_013:52
for G1, G2 being _Graph
for 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 end;

theorem :: GLIB_013:53
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous holds
G2 .supDegree() c= G1 .supDegree()
proof end;

theorem :: GLIB_013:54
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 holds
G2 .minDegree() c= G1 .minDegree()
proof end;

theorem Th55: :: GLIB_013:55
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() )
proof end;

theorem Th56: :: GLIB_013:56
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding holds
( G1 .supInDegree() c= G2 .supInDegree() & G1 .supOutDegree() c= G2 .supOutDegree() )
proof end;

theorem Th57: :: GLIB_013:57
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is directed & F is weak_SG-embedding & rng (F _V) = the_Vertices_of G2 holds
( G1 .minInDegree() c= G2 .minInDegree() & G1 .minOutDegree() c= G2 .minOutDegree() )
proof end;

theorem Th58: :: GLIB_013:58
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous holds
( G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )
proof end;

theorem Th59: :: GLIB_013:59
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is onto & F is semi-Dcontinuous & dom (F _V) = the_Vertices_of G1 holds
( G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )
proof end;

theorem Th60: :: GLIB_013:60
for G1, G2 being _Graph
for 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 end;

theorem :: GLIB_013:61
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 .supDegree() = G2 .supDegree() & G1 .minDegree() = G2 .minDegree() )
proof end;

theorem Th62: :: GLIB_013:62
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 end;

theorem Th63: :: GLIB_013:63
for G1 being _Graph
for G2 being Subgraph of G1 holds
( G2 .supDegree() c= G1 .supDegree() & G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() )
proof end;

theorem :: GLIB_013:64
for G1 being _Graph
for G2 being spanning Subgraph of G1 holds
( G2 .minDegree() c= G1 .minDegree() & G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() )
proof end;

theorem :: GLIB_013:65
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 .supDegree() = G2 .supDegree() & G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() )
proof end;

theorem :: GLIB_013:66
for G2 being _Graph
for V being set
for G1 being addVertices of G2,V st V \ (the_Vertices_of G2) <> {} holds
( G1 .minDegree() = 0 & G1 .minInDegree() = 0 & G1 .minOutDegree() = 0 )
proof end;

registration
let G be non edgeless _Graph;
cluster G .supDegree() -> non empty ;
coherence
not G .supDegree() is empty
proof end;
cluster G .supInDegree() -> non empty ;
coherence
not G .supInDegree() is empty
proof end;
cluster G .supOutDegree() -> non empty ;
coherence
not G .supOutDegree() is empty
proof 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
G .minDegree() is natural
proof end;
cluster G .minInDegree() -> natural ;
coherence
G .minInDegree() is natural
proof end;
cluster G .minOutDegree() -> natural ;
coherence
G .minOutDegree() is natural
proof end;
end;

definition
let G be locally-finite _Graph;
:: original: .minDegree()
redefine func G .minDegree() -> Nat;
coherence
G .minDegree() is Nat ;
:: original: .minInDegree()
redefine func G .minInDegree() -> Nat;
coherence
G .minInDegree() is Nat ;
:: original: .minOutDegree()
redefine func G .minOutDegree() -> Nat;
coherence
G .minOutDegree() is Nat ;
end;

theorem :: GLIB_013:67
for G being locally-finite _Graph
for 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 end;

theorem :: GLIB_013:68
for G being locally-finite _Graph
for 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 end;

theorem :: GLIB_013:69
for G being locally-finite _Graph
for 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 end;

Lm1: for a, b being Cardinal st a c= b & a <> b holds
a +` 1 c= b
proof end;

theorem Th70: :: GLIB_013:70
for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = ((v .degree()) /\ (w .degree())) +` 1 )
proof end;

theorem Th71: :: GLIB_013:71
for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) +` 1 )
proof end;

theorem Th72: :: GLIB_013:72
for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minOutDegree() = G2 .minOutDegree() or G1 .minOutDegree() = (v .outDegree()) +` 1 )
proof end;

theorem :: GLIB_013:73
for G2 being locally-finite _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minDegree() = G2 .minDegree() or G1 .minDegree() = (min ((v .degree()),(w .degree()))) + 1 )
proof end;

theorem :: GLIB_013:74
for G2 being locally-finite _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minInDegree() = G2 .minInDegree() or G1 .minInDegree() = (w .inDegree()) + 1 )
proof end;

theorem :: GLIB_013:75
for G2 being locally-finite _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w holds
( not v <> w or G1 .minOutDegree() = G2 .minOutDegree() or G1 .minOutDegree() = (v .outDegree()) + 1 )
proof 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: :: GLIB_013:76
for G2 being _Graph
for 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 end;

theorem :: GLIB_013:77
for G2 being _finite _Graph
for 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 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 end;

theorem :: GLIB_013:78
for G2 being _Graph
for V being set
for G1 being addLoops of G2,V holds G1 .minDegree() c= (G2 .minDegree()) +` 2
proof end;

registration
let G be edge-finite _Graph;
cluster G .supDegree() -> natural ;
coherence
G .supDegree() is natural
proof end;
cluster G .supInDegree() -> natural ;
coherence
G .supInDegree() is natural
proof end;
cluster G .supOutDegree() -> natural ;
coherence
G .supOutDegree() is natural
proof end;
end;

definition
let G be edge-finite _Graph;
:: original: .supDegree()
redefine func G .supDegree() -> Nat;
coherence
G .supDegree() is Nat ;
:: original: .supInDegree()
redefine func G .supInDegree() -> Nat;
coherence
G .supInDegree() is Nat ;
:: original: .supOutDegree()
redefine func G .supOutDegree() -> Nat;
coherence
G .supOutDegree() is Nat ;
end;

definition
let G be _Graph;
attr G is with_max_degree means :Def12: :: GLIB_013:def 12
 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: :: GLIB_013:def 13
 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: :: GLIB_013:def 14
 ex v being Vertex of G st
for w being Vertex of G holds w .outDegree() c= v .outDegree() ;
end;

:: deftheorem Def12 defines with_max_degree GLIB_013:def 12 :
for G being _Graph holds
( G is with_max_degree iff ex v being Vertex of G st
for w being Vertex of G holds w .degree() c= v .degree() );

:: deftheorem Def13 defines with_max_in_degree GLIB_013:def 13 :
for G being _Graph holds
( G is with_max_in_degree iff ex v being Vertex of G st
for w being Vertex of G holds w .inDegree() c= v .inDegree() );

:: deftheorem Def14 defines with_max_out_degree GLIB_013:def 14 :
for G being _Graph holds
( G is with_max_out_degree iff ex v being Vertex of G st
for w being Vertex of G holds w .outDegree() c= v .outDegree() );

theorem Th79: :: GLIB_013:79
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 end;

theorem Th80: :: GLIB_013:80
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 end;

theorem Th81: :: GLIB_013:81
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 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 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 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 end;

notation
let G be _Graph;
antonym without_max_degree G for with_max_degree ;
antonym without_max_in_degree G for with_max_in_degree ;
antonym without_max_out_degree G for with_max_out_degree ;
end;

registration
cluster Relation-like omega -defined Function-like finite [Graph-like] with_max_in_degree with_max_out_degree -> with_max_degree for set ;
coherence
for b1 being _Graph st b1 is with_max_in_degree & b1 is with_max_out_degree holds
b1 is with_max_degree
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] vertex-finite -> with_max_degree with_max_in_degree with_max_out_degree for set ;
coherence
for b1 being _Graph st b1 is vertex-finite holds
( b1 is with_max_degree & b1 is with_max_in_degree & b1 is with_max_out_degree )
proof end;
cluster Relation-like omega -defined Function-like finite [Graph-like] edge-finite -> with_max_degree with_max_in_degree with_max_out_degree for set ;
coherence
for b1 being _Graph st b1 is edge-finite holds
( b1 is with_max_degree & b1 is with_max_in_degree & b1 is with_max_out_degree )
proof end;
end;

theorem :: GLIB_013:82
for G being with_max_degree _Graph holds
( G is with_max_in_degree or G is with_max_out_degree )
proof 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 .supDegree() -> natural ;
coherence
G .maxDegree() is natural
proof end;
end;

definition
let G be locally-finite with_max_degree _Graph;
:: original: .supDegree()
redefine func G .maxDegree() -> Nat;
coherence
G .supDegree() is Nat ;
end;

registration
let G be locally-finite with_max_in_degree _Graph;
cluster G .supInDegree() -> natural ;
coherence
G .maxInDegree() is natural
proof end;
end;

definition
let G be locally-finite with_max_in_degree _Graph;
:: original: .supInDegree()
redefine func G .maxInDegree() -> Nat;
coherence
G .supInDegree() is Nat ;
end;

registration
let G be locally-finite with_max_out_degree _Graph;
cluster G .supOutDegree() -> natural ;
coherence
G .maxOutDegree() is natural
proof end;
end;

definition
let G be locally-finite with_max_out_degree _Graph;
:: original: .supOutDegree()
redefine func G .maxOutDegree() -> Nat;
coherence
G .supOutDegree() is Nat ;
end;

theorem Th83: :: GLIB_013:83
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is with_max_degree iff G2 is with_max_degree )
proof end;

theorem Th84: :: GLIB_013:84
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( ( G1 is with_max_in_degree implies G2 is with_max_in_degree ) & ( G2 is with_max_in_degree implies G1 is with_max_in_degree ) & ( G1 is with_max_out_degree implies G2 is with_max_out_degree ) & ( G2 is with_max_out_degree implies G1 is with_max_out_degree ) )
proof end;

theorem Th85: :: GLIB_013:85
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 end;

theorem Th86: :: GLIB_013:86
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is with_max_degree iff G2 is with_max_degree )
proof end;

registration
let G be with_max_degree _Graph;
let E be set ;
cluster -> with_max_degree for reverseEdgeDirections of G,E;
coherence
for b1 being reverseEdgeDirections of G,E holds b1 is with_max_degree 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 end;

registration
let G be with_max_degree _Graph;
let V be set ;
cluster -> with_max_degree for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is with_max_degree
proof end;
cluster -> with_max_degree for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is with_max_degree
proof end;
end;

registration
let G be with_max_degree _Graph;
let v, e, w be object ;
cluster -> with_max_degree for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is with_max_degree
proof end;
cluster -> with_max_degree for addAdjVertex of G,v,e,w;
coherence
for b1 being addAdjVertex of G,v,e,w holds b1 is with_max_degree
proof end;
end;

Lm7: for a, b being Cardinal st a in b +` 1 holds
a c= b
proof end;

registration
let G be with_max_degree _Graph;
let v be object ;
let V be set ;
cluster -> with_max_degree for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds b1 is with_max_degree
proof end;
end;

registration
let G be with_max_in_degree _Graph;
cluster -> with_max_out_degree for reverseEdgeDirections of G, the_Edges_of G;
coherence
for b1 being reverseEdgeDirections of G holds b1 is with_max_out_degree
proof end;
end;

registration
let G be with_max_in_degree _Graph;
let V be set ;
cluster -> with_max_in_degree for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is with_max_in_degree
proof end;
cluster -> with_max_in_degree for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is with_max_in_degree
proof end;
end;

registration
let G be with_max_in_degree _Graph;
let v, e, w be object ;
cluster -> with_max_in_degree for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is with_max_in_degree
proof end;
cluster -> with_max_in_degree for addAdjVertex of G,v,e,w;
coherence
for b1 being addAdjVertex of G,v,e,w holds b1 is with_max_in_degree
proof end;
end;

registration
let G be with_max_in_degree _Graph;
let v be object ;
let V be set ;
cluster -> with_max_in_degree for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds b1 is with_max_in_degree
proof end;
end;

registration
let G be with_max_out_degree _Graph;
cluster -> with_max_in_degree for reverseEdgeDirections of G, the_Edges_of G;
coherence
for b1 being reverseEdgeDirections of G holds b1 is with_max_in_degree
proof end;
end;

registration
let G be with_max_out_degree _Graph;
let V be set ;
cluster -> with_max_out_degree for addVertices of G,V;
coherence
for b1 being addVertices of G,V holds b1 is with_max_out_degree
proof end;
cluster -> with_max_out_degree for addLoops of G,V;
coherence
for b1 being addLoops of G,V holds b1 is with_max_out_degree
proof end;
end;

registration
let G be with_max_out_degree _Graph;
let v, e, w be object ;
cluster -> with_max_out_degree for addEdge of G,v,e,w;
coherence
for b1 being addEdge of G,v,e,w holds b1 is with_max_out_degree
proof end;
cluster -> with_max_out_degree for addAdjVertex of G,v,e,w;
coherence
for b1 being addAdjVertex of G,v,e,w holds b1 is with_max_out_degree
proof end;
end;

registration
let G be with_max_out_degree _Graph;
let v be object ;
let V be set ;
cluster -> with_max_out_degree for addAdjVertexAll of G,v,V;
coherence
for b1 being addAdjVertexAll of G,v,V holds b1 is with_max_out_degree
proof 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 :: GLIB_013:87
for G being locally-finite with_max_degree _Graph
for 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 end;

theorem :: GLIB_013:88
for G being locally-finite with_max_in_degree _Graph
for 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 end;

theorem :: GLIB_013:89
for G being locally-finite with_max_out_degree _Graph
for 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 end;

theorem :: GLIB_013:90
for c being Cardinal
for G being _trivial b1 -edge _Graph holds
( G .maxInDegree() = c & G .minInDegree() = c & G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )
proof end;

definition
let G be _Graph;
let v be Vertex of G;
attr v is with_min_degree means :: GLIB_013:def 15
v .degree() = G .minDegree() ;
attr v is with_min_in_degree means :: GLIB_013:def 16
v .inDegree() = G .minInDegree() ;
attr v is with_min_out_degree means :: GLIB_013:def 17
v .outDegree() = G .minOutDegree() ;
attr v is with_max_degree means :: GLIB_013:def 18
v .degree() = G .supDegree() ;
attr v is with_max_in_degree means :: GLIB_013:def 19
v .inDegree() = G .supInDegree() ;
attr v is with_max_out_degree means :: GLIB_013:def 20
v .outDegree() = G .supOutDegree() ;
end;

:: deftheorem defines with_min_degree GLIB_013:def 15 :
for G being _Graph
for v being Vertex of G holds
( v is with_min_degree iff v .degree() = G .minDegree() );

:: deftheorem defines with_min_in_degree GLIB_013:def 16 :
for G being _Graph
for v being Vertex of G holds
( v is with_min_in_degree iff v .inDegree() = G .minInDegree() );

:: deftheorem defines with_min_out_degree GLIB_013:def 17 :
for G being _Graph
for v being Vertex of G holds
( v is with_min_out_degree iff v .outDegree() = G .minOutDegree() );

:: deftheorem defines with_max_degree GLIB_013:def 18 :
for G being _Graph
for v being Vertex of G holds
( v is with_max_degree iff v .degree() = G .supDegree() );

:: deftheorem defines with_max_in_degree GLIB_013:def 19 :
for G being _Graph
for v being Vertex of G holds
( v is with_max_in_degree iff v .inDegree() = G .supInDegree() );

:: deftheorem defines with_max_out_degree GLIB_013:def 20 :
for G being _Graph
for v being Vertex of G holds
( v is with_max_out_degree iff v .outDegree() = G .supOutDegree() );

theorem :: GLIB_013:91
for G being _Graph
for v, w being Vertex of G st v is with_min_degree holds
v .degree() c= w .degree()
proof end;

theorem Th92: :: GLIB_013:92
for G being _Graph
for v, w being Vertex of G st v is with_min_in_degree holds
v .inDegree() c= w .inDegree()
proof end;

theorem Th93: :: GLIB_013:93
for G being _Graph
for v, w being Vertex of G st v is with_min_out_degree holds
v .outDegree() c= w .outDegree()
proof end;

theorem :: GLIB_013:94
for G being _Graph
for v, w being Vertex of G st w is with_max_degree holds
v .degree() c= w .degree()
proof end;

theorem Th95: :: GLIB_013:95
for G being _Graph
for v, w being Vertex of G st w is with_max_in_degree holds
v .inDegree() c= w .inDegree()
proof end;

theorem Th96: :: GLIB_013:96
for G being _Graph
for v, w being Vertex of G st w is with_max_out_degree holds
v .outDegree() c= w .outDegree()
proof end;

registration
let G be _Graph;
cluster with_min_degree for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is with_min_degree
proof end;
cluster with_min_in_degree for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is with_min_in_degree
proof end;
cluster with_min_out_degree for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is with_min_out_degree
proof end;
cluster with_min_in_degree with_min_out_degree -> with_min_degree for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G st b1 is with_min_in_degree & b1 is with_min_out_degree holds
b1 is with_min_degree
proof end;
cluster with_max_in_degree with_max_out_degree -> with_max_degree for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G st b1 is with_max_in_degree & b1 is with_max_out_degree holds
b1 is with_max_degree
proof end;
cluster isolated -> with_min_degree with_min_in_degree with_min_out_degree for Element of the_Vertices_of G;
coherence
for b1 being Vertex of G st b1 is isolated holds
( b1 is with_min_degree & b1 is with_min_in_degree & b1 is with_min_out_degree )
proof end;
end;

theorem Th97: :: GLIB_013:97
for G being _Graph holds
( G is with_max_degree iff ex v being Vertex of G st v is with_max_degree )
proof end;

theorem Th98: :: GLIB_013:98
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 end;

theorem Th99: :: GLIB_013:99
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 end;

registration
let G be with_max_degree _Graph;
cluster with_max_degree for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is with_max_degree by Th97;
end;

registration
let G be with_max_in_degree _Graph;
cluster with_max_in_degree for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is with_max_in_degree by Th98;
end;

registration
let G be with_max_out_degree _Graph;
cluster with_max_out_degree for Element of the_Vertices_of G;
existence
ex b1 being Vertex of G st b1 is with_max_out_degree by Th99;
end;