:: 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 b₁ being _Graph st b₁ is _finite holds
( b₁ is vertex-finite & b₁ is edge-finite ) ;

cluster Relation-like omega -defined Function-like finite [Graph-like] vertex-finite edge-finite -> _finite for set ;

coherence
for b₁ being _Graph st b₁ is vertex-finite & b₁ is edge-finite holds
b₁ is _finite by GLIB_000:def 17;

cluster Relation-like omega -defined Function-like finite [Graph-like] edgeless -> edge-finite for set ;

coherence
for b₁ being _Graph st b₁ is edgeless holds
b₁ is edge-finite ;

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial -> vertex-finite for set ;

coherence
for b₁ being _Graph st b₁ is _trivial holds
b₁ is vertex-finite ;

cluster Relation-like omega -defined Function-like finite [Graph-like] non-Dmulti vertex-finite -> edge-finite for set ;

coherence
for b₁ being _Graph st b₁ is vertex-finite & b₁ is non-Dmulti holds
b₁ 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 b₁ being _Graph st not b₁ is vertex-finite & b₁ is loopfull holds
not b₁ is edge-finite

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] simple vertex-finite edge-finite for set ;

existence
ex b₁ being _Graph st
( b₁ is vertex-finite & b₁ is edge-finite & b₁ is simple )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] vertex-finite non edge-finite for set ;

existence
ex b₁ being _Graph st
( b₁ is vertex-finite & not b₁ is edge-finite )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] non vertex-finite edge-finite for set ;

existence
ex b₁ being _Graph st
( not b₁ is vertex-finite & b₁ 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 b₁ being _Graph st
( not b₁ is vertex-finite & not b₁ 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 b₁ being Subgraph of G holds b₁ is vertex-finite

proof end;

cluster -> vertex-finite edge-finite for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds
( b₁ is vertex-finite & b₁ is edge-finite )

proof end;

cluster -> vertex-finite edge-finite for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds
( b₁ is vertex-finite & b₁ is edge-finite )

proof end;

cluster -> vertex-finite edge-finite for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds
( b₁ is vertex-finite & b₁ is edge-finite )

proof end;

cluster -> vertex-finite edge-finite for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds
( b₁ is vertex-finite & b₁ is edge-finite )

proof end;

let V be finite set ;

cluster -> vertex-finite for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ 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 b₁ being addVertex of G,v holds b₁ is vertex-finite ;
let e, w be object ;

cluster -> vertex-finite for addEdge of G,v,e,w;

coherence
for b₁ being addEdge of G,v,e,w holds b₁ is vertex-finite

proof end;

cluster -> vertex-finite for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds b₁ 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 b₁ being reverseEdgeDirections of G,E holds b₁ 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 b₁ being addAdjVertexAll of G,v,V holds b₁ 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 b₁ being addLoops of G,V holds b₁ 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 b₁ being addVertices of G,V holds not b₁ 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 b₁ being Supergraph of G holds not b₁ is vertex-finite

proof end;

cluster spanning -> non vertex-finite for Subgraph of G;

coherence
for b₁ being Subgraph of G st b₁ is spanning holds
not b₁ is vertex-finite

proof end;

cluster -> non vertex-finite for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds not b₁ is vertex-finite

proof end;

cluster -> non vertex-finite for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds not b₁ is vertex-finite

proof end;

cluster -> non vertex-finite for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds not b₁ is vertex-finite

proof end;

cluster -> non vertex-finite for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds not b₁ 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 b₁ being inducedSubgraph of G,V,E holds not b₁ 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 b₁ being addLoops of G,V holds not b₁ 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 b₁ being Subgraph of G holds b₁ is edge-finite

proof end;

let V be set ;

cluster -> edge-finite for addVertices of G,V;

coherence
for b₁ being addVertices of G,V holds b₁ 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 b₁ being reverseEdgeDirections of G,E holds b₁ 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 b₁ being addVertex of G,v holds b₁ is edge-finite ;
let e, w be object ;

cluster -> edge-finite for addEdge of G,v,e,w;

coherence
for b₁ being addEdge of G,v,e,w holds b₁ is edge-finite

proof end;

cluster -> edge-finite for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds b₁ 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 b₁ being addAdjVertexAll of G,v,V holds b₁ 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 b₁ being addLoops of G,V holds b₁ 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 b₁ being Vertex of G st b₁ 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 b₁ being DLGraphComplement of G holds not b₁ is edge-finite

proof end;

cluster -> non edge-finite for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds not b₁ is edge-finite

proof end;

cluster -> non edge-finite for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds not b₁ is edge-finite

proof end;

cluster -> non edge-finite for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds not b₁ 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 b₁ being Supergraph of G holds not b₁ 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 b₁ being inducedSubgraph of G,V,E holds not b₁ 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 b₁ being removeEdges of G,E holds not b₁ 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 b₁ being removeEdge of G,e holds not b₁ 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 b₁ being _Graph st
( b₁ is a -vertex & b₁ 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 b₁ being _Graph st
( b₁ is _trivial & b₁ is c -edge )

proof end;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] -> non 0 -vertex for set ;

coherence
for b₁ being _Graph holds not b₁ is 0 -vertex ;

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial -> 1 -vertex for set ;

coherence
for b₁ being _Graph st b₁ is _trivial holds
b₁ 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 b₁ being _Graph st b₁ is 1 -vertex holds
b₁ 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 b₁ being _Graph st b₁ is n -vertex holds
b₁ 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 b₁ being Subgraph of G st b₁ is spanning holds
b₁ is c -vertex

proof end;

cluster -> c -vertex for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is c -vertex

proof end;

cluster -> c -vertex for LGraphComplement of G;

coherence
for b₁ being LGraphComplement of G holds b₁ is c -vertex

proof end;

cluster -> c -vertex for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is c -vertex

proof end;

cluster -> c -vertex for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds b₁ is c -vertex

proof end;

let E be set ;

cluster -> c -vertex for reverseEdgeDirections of G,E;

coherence
for b₁ being reverseEdgeDirections of G,E holds b₁ 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 b₁ being addLoops of G,V holds b₁ 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 b₁ being addEdge of G,v,e,w holds b₁ is c -vertex

proof end;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] edgeless -> 0 -edge for set ;

coherence
for b₁ being _Graph st b₁ is edgeless holds
b₁ is 0 -edge ;

cluster Relation-like omega -defined Function-like finite [Graph-like] 0 -edge -> edgeless for set ;

coherence
for b₁ being _Graph st b₁ is 0 -edge holds
b₁ is edgeless ;
let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n -edge -> edge-finite for set ;

coherence
for b₁ being _Graph st b₁ is n -edge holds
b₁ 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 b₁ being reverseEdgeDirections of G,E holds b₁ 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 b₁ being addVertices of G,V holds b₁ 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 b₁ being addAdjVertexAll of G, the_Vertices_of G,V holds not b₁ 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 b₁ being _Graph st b₁ is edge-finite holds
b₁ is locally-finite ;

cluster Relation-like omega -defined Function-like finite [Graph-like] non 0 -vertex locally-finite for set ;

existence
ex b₁ being _Graph st b₁ 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 b₁ being _Graph holds b₁ is locally-finite

proof end;

end;

registration

let G be locally-finite _Graph;

cluster -> locally-finite for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ 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 b₁ being addVertices of G,V holds b₁ is locally-finite

proof end;

cluster -> locally-finite for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ 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 b₁ being reverseEdgeDirections of G,E holds b₁ 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 b₁ being addEdge of G,v,e,w holds b₁ is locally-finite

proof end;

cluster -> locally-finite for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds b₁ 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 b₁ being addAdjVertexAll of G,v,V holds b₁ is locally-finite

proof end;

end;

registration

let G be non locally-finite _Graph;

cluster -> non locally-finite for Supergraph of G;

coherence
for b₁ being Supergraph of G holds not b₁ 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 b₁ being removeEdges of G,E holds not b₁ 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 b₁ being removeEdge of G,e holds not b₁ 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 b₁ being _Graph st b₁ is with_max_in_degree & b₁ is with_max_out_degree holds
b₁ 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 b₁ being _Graph st b₁ is vertex-finite holds
( b₁ is with_max_degree & b₁ is with_max_in_degree & b₁ 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 b₁ being _Graph st b₁ is edge-finite holds
( b₁ is with_max_degree & b₁ is with_max_in_degree & b₁ 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 b₁ being reverseEdgeDirections of G,E holds b₁ 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 b₁ being addVertices of G,V holds b₁ is with_max_degree

proof end;

cluster -> with_max_degree for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ 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 b₁ being addEdge of G,v,e,w holds b₁ is with_max_degree

proof end;

cluster -> with_max_degree for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds b₁ 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 b₁ being addAdjVertexAll of G,v,V holds b₁ 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 b₁ being reverseEdgeDirections of G holds b₁ 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 b₁ being addVertices of G,V holds b₁ is with_max_in_degree

proof end;

cluster -> with_max_in_degree for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ 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 b₁ being addEdge of G,v,e,w holds b₁ is with_max_in_degree

proof end;

cluster -> with_max_in_degree for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds b₁ 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 b₁ being addAdjVertexAll of G,v,V holds b₁ 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 b₁ being reverseEdgeDirections of G holds b₁ 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 b₁ being addVertices of G,V holds b₁ is with_max_out_degree

proof end;

cluster -> with_max_out_degree for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ 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 b₁ being addEdge of G,v,e,w holds b₁ is with_max_out_degree

proof end;

cluster -> with_max_out_degree for addAdjVertex of G,v,e,w;

coherence
for b₁ being addAdjVertex of G,v,e,w holds b₁ 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 b₁ being addAdjVertexAll of G,v,V holds b₁ 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 b₁ -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 b₁ being Vertex of G st b₁ is with_min_degree

proof end;

cluster with_min_in_degree for Element of the_Vertices_of G;

existence
ex b₁ being Vertex of G st b₁ is with_min_in_degree

proof end;

cluster with_min_out_degree for Element of the_Vertices_of G;

existence
ex b₁ being Vertex of G st b₁ 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 b₁ being Vertex of G st b₁ is with_min_in_degree & b₁ is with_min_out_degree holds
b₁ 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 b₁ being Vertex of G st b₁ is with_max_in_degree & b₁ is with_max_out_degree holds
b₁ 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 b₁ being Vertex of G st b₁ is isolated holds
( b₁ is with_min_degree & b₁ is with_min_in_degree & b₁ 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 b₁ being Vertex of G st b₁ 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 b₁ being Vertex of G st b₁ 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 b₁ being Vertex of G st b₁ is with_max_out_degree by Th99;

end;