:: 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)] ) )

( 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 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)] ) )

( 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)} ) )

( 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)} ) )

( 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;

:: 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 );

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 );

for G being _Graph holds

( G is edge-finite iff the_Edges_of G 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;

( ( 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;

coherence

createGraph (V,E,S,T) is vertex-finite ;

end;
let E be set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is vertex-finite ;

registration

let V be infinite set ;

let E be set ;

let S, T be Function of E,V;

coherence

not createGraph (V,E,S,T) is vertex-finite ;

end;
let E be set ;

let S, T be Function of E,V;

coherence

not createGraph (V,E,S,T) is vertex-finite ;

registration

let V be non empty set ;

let E be finite set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is edge-finite ;

end;
let E be finite set ;

let S, T be Function of E,V;

coherence

createGraph (V,E,S,T) is edge-finite ;

registration

let V be non empty set ;

let E be infinite set ;

let S, T be Function of E,V;

coherence

not createGraph (V,E,S,T) is edge-finite ;

end;
let E be infinite set ;

let S, T be Function of E,V;

coherence

not createGraph (V,E,S,T) is edge-finite ;

registration

for b_{1} being _Graph st b_{1} is _finite holds

( b_{1} is vertex-finite & b_{1} is edge-finite )
;

for b_{1} being _Graph st b_{1} is vertex-finite & b_{1} is edge-finite holds

b_{1} is _finite
by GLIB_000:def 17;

for b_{1} being _Graph st b_{1} is edgeless holds

b_{1} is edge-finite
;

for b_{1} being _Graph st b_{1} is _trivial holds

b_{1} is vertex-finite
;

for b_{1} being _Graph st b_{1} is vertex-finite & b_{1} is non-Dmulti holds

b_{1} is edge-finite

for b_{1} being _Graph st not b_{1} is vertex-finite & b_{1} is loopfull holds

not b_{1} is edge-finite

ex b_{1} being _Graph st

( b_{1} is vertex-finite & b_{1} is edge-finite & b_{1} is simple )

ex b_{1} being _Graph st

( b_{1} is vertex-finite & not b_{1} is edge-finite )

ex b_{1} being _Graph st

( not b_{1} is vertex-finite & b_{1} is edge-finite )

ex b_{1} being _Graph st

( not b_{1} is vertex-finite & not b_{1} is edge-finite )
end;

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

coherence for b

( b

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

coherence for b

b

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

coherence for b

b

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

coherence for b

b

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

coherence for b

b

proof end;

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

coherence for b

not b

proof end;

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

existence ex b

( b

proof end;

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

existence ex b

( b

proof end;

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

existence ex b

( not b

proof end;

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

existence ex b

( not b

proof end;

registration

let G be vertex-finite _Graph;

coherence

( not G .order() is zero & G .order() is natural )

end;
coherence

( not G .order() is zero & G .order() is natural )

proof 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;
:: original: .order()

redefine func G .order() -> non zero Nat;

coherence

G .order() is non zero Nat ;

definition

let G be edge-finite _Graph;

:: original: .size()

redefine func G .size() -> Nat;

coherence

G .size() is Nat ;

end;
:: original: .size()

redefine func G .size() -> Nat;

coherence

G .size() is Nat ;

theorem :: GLIB_013:11

for G being non-multi vertex-finite _Graph holds G .size() <= (((G .order()) ^2) + (G .order())) / 2

proof end;

registration

let G be vertex-finite _Graph;

coherence

the_Vertices_of G is finite by Def1;

coherence

for b_{1} being Subgraph of G holds b_{1} is vertex-finite

for b_{1} being DLGraphComplement of G holds

( b_{1} is vertex-finite & b_{1} is edge-finite )

for b_{1} being LGraphComplement of G holds

( b_{1} is vertex-finite & b_{1} is edge-finite )

for b_{1} being DGraphComplement of G holds

( b_{1} is vertex-finite & b_{1} is edge-finite )

for b_{1} being GraphComplement of G holds

( b_{1} is vertex-finite & b_{1} is edge-finite )

coherence

for b_{1} being addVertices of G,V holds b_{1} is vertex-finite

end;
coherence

the_Vertices_of G is finite by Def1;

coherence

for b

proof end;

coherence for b

( b

proof end;

coherence for b

( b

proof end;

coherence for b

( b

proof end;

coherence for b

( b

proof end;

let V be finite set ;coherence

for b

proof end;

registration

let G be vertex-finite _Graph;

let v be object ;

coherence

for b_{1} being addVertex of G,v holds b_{1} is vertex-finite
;

let e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is vertex-finite

for b_{1} being addAdjVertex of G,v,e,w holds b_{1} is vertex-finite

end;
let v be object ;

coherence

for b

let e, w be object ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be vertex-finite _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is vertex-finite

end;
let E be set ;

coherence

for b

proof end;

registration

let G be vertex-finite _Graph;

let v be object ;

let V be set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is vertex-finite

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be vertex-finite _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is vertex-finite

end;
let V be set ;

coherence

for b

proof end;

registration

let G be _Graph;

let V be infinite set ;

coherence

for b_{1} being addVertices of G,V holds not b_{1} is vertex-finite

end;
let V be infinite set ;

coherence

for b

proof end;

registration

let G be non vertex-finite _Graph;

coherence

not the_Vertices_of G is finite by Def1;

coherence

for b_{1} being Supergraph of G holds not b_{1} is vertex-finite

for b_{1} being Subgraph of G st b_{1} is spanning holds

not b_{1} is vertex-finite

for b_{1} being DLGraphComplement of G holds not b_{1} is vertex-finite

for b_{1} being LGraphComplement of G holds not b_{1} is vertex-finite

for b_{1} being DGraphComplement of G holds not b_{1} is vertex-finite

for b_{1} being GraphComplement of G holds not b_{1} is vertex-finite

let E be set ;

coherence

for b_{1} being inducedSubgraph of G,V,E holds not b_{1} is vertex-finite

end;
coherence

not the_Vertices_of G is finite by Def1;

coherence

for b

proof end;

coherence for b

not b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

let V be infinite set ;let E be set ;

coherence

for b

proof end;

registration

let G be non vertex-finite _Graph;

let V be infinite Subset of (the_Vertices_of G);

coherence

for b_{1} being addLoops of G,V holds not b_{1} is edge-finite

end;
let V be infinite Subset of (the_Vertices_of G);

coherence

for b

proof end;

registration

let G be edge-finite _Graph;

coherence

the_Edges_of G is finite by Def2;

coherence

for b_{1} being Subgraph of G holds b_{1} is edge-finite

coherence

for b_{1} being addVertices of G,V holds b_{1} is edge-finite

end;
coherence

the_Edges_of G is finite by Def2;

coherence

for b

proof end;

let V be set ;coherence

for b

proof end;

registration

let G be edge-finite _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is edge-finite

end;
let E be set ;

coherence

for b

proof end;

registration

let G be edge-finite _Graph;

let v be object ;

coherence

for b_{1} being addVertex of G,v holds b_{1} is edge-finite
;

let e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is edge-finite

for b_{1} being addAdjVertex of G,v,e,w holds b_{1} is edge-finite

end;
let v be object ;

coherence

for b

let e, w be object ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be edge-finite _Graph;

let v be object ;

let V be finite set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is edge-finite

end;
let v be object ;

let V be finite set ;

coherence

for b

proof end;

registration

let G be edge-finite _Graph;

let V be finite Subset of (the_Vertices_of G);

coherence

for b_{1} being addLoops of G,V holds b_{1} is edge-finite

end;
let V be finite Subset of (the_Vertices_of G);

coherence

for b

proof end;

registration

let G be non vertex-finite edge-finite _Graph;

existence

ex b_{1} being Vertex of G st b_{1} is isolated

end;
existence

ex b

proof end;

registration

let G be non vertex-finite edge-finite _Graph;

coherence

for b_{1} being DLGraphComplement of G holds not b_{1} is edge-finite

for b_{1} being LGraphComplement of G holds not b_{1} is edge-finite

for b_{1} being DGraphComplement of G holds not b_{1} is edge-finite

for b_{1} being GraphComplement of G holds not b_{1} is edge-finite

end;
coherence

for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

registration

let G be non edge-finite _Graph;

coherence

not the_Edges_of G is finite by Def2;

coherence

for b_{1} being Supergraph of G holds not b_{1} is edge-finite

let E be infinite Subset of (the_Edges_of G);

coherence

for b_{1} being inducedSubgraph of G,V,E holds not b_{1} is edge-finite

end;
coherence

not the_Edges_of G is finite by Def2;

coherence

for b

proof end;

let V be set ;let E be infinite Subset of (the_Edges_of G);

coherence

for b

proof end;

registration

let G be non edge-finite _Graph;

let E be finite set ;

coherence

for b_{1} being removeEdges of G,E holds not b_{1} is edge-finite
;

end;
let E be finite set ;

coherence

for b

registration

let G be non edge-finite _Graph;

let e be set ;

coherence

for b_{1} being removeEdge of G,e holds not b_{1} is edge-finite
;

end;
let e be set ;

coherence

for b

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 ) )

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 ) )

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;

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;

:: 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 );

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 );

for c being Cardinal

for G being _Graph holds

( G is c -edge iff G .size() = c );

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 ;

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 ;

for c being Cardinal st the_Edges_of G1 = the_Edges_of G2 & G1 is c -edge holds

G2 is c -edge ;

theorem :: GLIB_013:21

registration

let V be non empty set ;

let E be set ;

let S, T be Function of E,V;

coherence

( createGraph (V,E,S,T) is card V -vertex & createGraph (V,E,S,T) is card E -edge ) ;

end;
let E be set ;

let S, T be Function of E,V;

coherence

( createGraph (V,E,S,T) is card V -vertex & createGraph (V,E,S,T) is card E -edge ) ;

registration

let a be non zero Cardinal;

let b be Cardinal;

existence

ex b_{1} being _Graph st

( b_{1} is a -vertex & b_{1} is b -edge )

end;
let b be Cardinal;

existence

ex b

( b

proof end;

registration

let c be Cardinal;

existence

ex b_{1} being _Graph st

( b_{1} is _trivial & b_{1} is c -edge )

end;
existence

ex b

( b

proof end;

registration

coherence

for b_{1} being _Graph holds not b_{1} is 0 -vertex
;

for b_{1} being _Graph st b_{1} is _trivial holds

b_{1} is 1 -vertex
by GLIB_000:def 19;

for b_{1} being _Graph st b_{1} is 1 -vertex holds

b_{1} is _trivial
by GLIB_000:def 19;

let n be non zero Nat;

for b_{1} being _Graph st b_{1} is n -vertex holds

b_{1} is vertex-finite
;

end;
for b

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

coherence for b

b

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

coherence for b

b

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

b

registration

let c be non zero Cardinal;

let G be c -vertex _Graph;

coherence

for b_{1} being Subgraph of G st b_{1} is spanning holds

b_{1} is c -vertex

for b_{1} being DLGraphComplement of G holds b_{1} is c -vertex

for b_{1} being LGraphComplement of G holds b_{1} is c -vertex

for b_{1} being DGraphComplement of G holds b_{1} is c -vertex

for b_{1} being GraphComplement of G holds b_{1} is c -vertex

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is c -vertex

end;
let G be c -vertex _Graph;

coherence

for b

b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

coherence for b

proof end;

let E be set ;coherence

for b

proof end;

registration

let c be non zero Cardinal;

let G be c -vertex _Graph;

let V be set ;

coherence

for b_{1} being addLoops of G,V holds b_{1} is c -vertex

end;
let G be c -vertex _Graph;

let V be set ;

coherence

for b

proof end;

registration

let c be non zero Cardinal;

let G be c -vertex _Graph;

let v, e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is c -vertex

end;
let G be c -vertex _Graph;

let v, e, w be object ;

coherence

for b

proof end;

registration

for b_{1} being _Graph st b_{1} is edgeless holds

b_{1} is 0 -edge
;

for b_{1} being _Graph st b_{1} is 0 -edge holds

b_{1} is edgeless
;

let n be Nat;

for b_{1} being _Graph st b_{1} is n -edge holds

b_{1} is edge-finite
;

end;

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

coherence for b

b

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

coherence for b

b

let n be Nat;

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

coherence for b

b

registration

let c be Cardinal;

let G be c -edge _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is c -edge

end;
let G be c -edge _Graph;

let E be set ;

coherence

for b

proof end;

registration

let c be Cardinal;

let G be c -edge _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is c -edge

end;
let G be c -edge _Graph;

let V be set ;

coherence

for b

proof 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;

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;

end;
attr G is locally-finite means :Def5: :: GLIB_013:def 5

for v being Vertex of G holds v .edgesInOut() is finite ;

for v being Vertex of G holds v .edgesInOut() is finite ;

:: 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 );

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 )

( G is locally-finite iff for v being Vertex of G holds v .degree() is 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 ) )

( 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 ) )

( 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

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

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);

coherence

for b_{1} being addAdjVertexAll of G, the_Vertices_of G,V holds not b_{1} is locally-finite

end;
let V be infinite Subset of (the_Vertices_of G);

coherence

for b

proof end;

registration

for b_{1} being _Graph st b_{1} is edge-finite holds

b_{1} is locally-finite
;

ex b_{1} being _Graph st b_{1} is locally-finite

not for b_{1} being _Graph holds b_{1} is locally-finite
end;

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

coherence for b

b

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

existence ex b

proof end;

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

existence not for b

proof end;

registration

let G be locally-finite _Graph;

coherence

for b_{1} being Subgraph of G holds b_{1} is locally-finite

coherence

G .edgesInto X is finite

G .edgesOutOf X is finite

G .edgesInOut X is finite ;

coherence

G .edgesBetween X is finite ;

let Y be finite set ;

coherence

G .edgesBetween (X,Y) is finite

G .edgesDBetween (X,Y) is finite

end;
coherence

for b

proof end;

let X be finite set ;coherence

G .edgesInto X is finite

proof end;

coherence G .edgesOutOf X is finite

proof end;

coherence G .edgesInOut X is finite ;

coherence

G .edgesBetween X is finite ;

let Y be finite set ;

coherence

G .edgesBetween (X,Y) is finite

proof end;

coherence G .edgesDBetween (X,Y) is finite

proof end;

registration

let G be locally-finite _Graph;

let v be Vertex of G;

coherence

v .edgesIn() is finite ;

coherence

v .edgesOut() is finite ;

coherence

v .edgesInOut() is finite ;

coherence

v .inDegree() is finite ;

coherence

v .outDegree() is finite ;

coherence

v .degree() is finite ;

end;
let v be Vertex of G;

coherence

v .edgesIn() is finite ;

coherence

v .edgesOut() is finite ;

coherence

v .edgesInOut() is finite ;

coherence

v .inDegree() is finite ;

coherence

v .outDegree() is finite ;

coherence

v .degree() is finite ;

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;
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 ;

registration

let G be locally-finite _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is locally-finite

for b_{1} being addLoops of G,V holds b_{1} is locally-finite

end;
let V be set ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be locally-finite _Graph;

let E be set ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is locally-finite

end;
let E be set ;

coherence

for b

proof end;

registration

let G be locally-finite _Graph;

let v, e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is locally-finite

for b_{1} being addAdjVertex of G,v,e,w holds b_{1} is locally-finite

end;
let v, e, w be object ;

coherence

for b

proof end;

coherence for b

proof 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 )

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 ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is locally-finite

end;
let v be object ;

let V be finite set ;

coherence

for b

proof end;

registration

let G be non locally-finite _Graph;

coherence

for b_{1} being Supergraph of G holds not b_{1} is locally-finite

coherence

for b_{1} being removeEdges of G,E holds not b_{1} is locally-finite

end;
coherence

for b

proof end;

let E be finite set ;coherence

for b

proof end;

registration

let G be non locally-finite _Graph;

let e be set ;

coherence

for b_{1} being removeEdge of G,e holds not b_{1} is locally-finite
;

end;
let e be set ;

coherence

for b

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

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

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

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

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 )

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;

union { (v .degree()) where v is Vertex of G : verum } is Cardinal

union { (v .inDegree()) where v is Vertex of G : verum } is Cardinal

union { (v .outDegree()) where v is Vertex of G : verum } is Cardinal

meet { (v .degree()) where v is Vertex of G : verum } is Cardinal

meet { (v .inDegree()) where v is Vertex of G : verum } is Cardinal

meet { (v .outDegree()) where v is Vertex of G : verum } is Cardinal

end;
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 } ;

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 } ;

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 } ;

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 } ;

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 } ;

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 } ;

meet { (v .outDegree()) where v is Vertex of G : verum } is Cardinal

proof 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 } ;

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 } ;

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 } ;

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 } ;

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 } ;

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 } ;

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() )

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() ) ) )

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() ) ) )

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() ) ) )

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 :: GLIB_013:45

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 )

( G .minDegree() = 0 & G .minInDegree() = 0 & G .minOutDegree() = 0 )

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;

::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

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

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

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()

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()

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()

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()

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() )

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() )

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() )

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() )

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() )

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() )

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() )

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() )

( 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() )

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() )

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() )

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 )

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;

coherence

not G .supDegree() is empty

not G .supInDegree() is empty

not G .supOutDegree() is empty

end;
coherence

not G .supDegree() is empty

proof end;

coherence not G .supInDegree() is empty

proof end;

coherence not G .supOutDegree() is empty

proof 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;

:: 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;

coherence

G .minDegree() is natural

G .minInDegree() is natural

G .minOutDegree() is natural

end;
coherence

G .minDegree() is natural

proof end;

coherence G .minInDegree() is natural

proof end;

coherence G .minOutDegree() is natural

proof 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;
:: 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 ;

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() ) ) )

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() ) ) )

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() ) ) )

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 )

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 )

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 )

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 )

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 )

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 )

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

:: 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())

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()))

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

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;

coherence

G .supDegree() is natural

G .supInDegree() is natural

G .supOutDegree() is natural

end;
coherence

G .supDegree() is natural

proof end;

coherence G .supInDegree() is natural

proof end;

coherence G .supOutDegree() is natural

proof 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;
:: 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 ;

definition

let G be _Graph;

end;
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() ;

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() ;

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() ;

ex v being Vertex of G st

for w being Vertex of G holds w .outDegree() c= v .outDegree() ;

:: 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() );

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() );

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() );

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() ) )

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() ) )

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() ) )

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;
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 ;

registration

for b_{1} being _Graph st b_{1} is with_max_in_degree & b_{1} is with_max_out_degree holds

b_{1} is with_max_degree

for b_{1} being _Graph st b_{1} is vertex-finite holds

( b_{1} is with_max_degree & b_{1} is with_max_in_degree & b_{1} is with_max_out_degree )

for b_{1} being _Graph st b_{1} is edge-finite holds

( b_{1} is with_max_degree & b_{1} is with_max_in_degree & b_{1} is with_max_out_degree )
end;

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

b

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

( b

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

( b

proof end;

registration
end;

definition

let G be locally-finite with_max_degree _Graph;

:: original: .supDegree()

redefine func G .maxDegree() -> Nat;

coherence

G .supDegree() is Nat ;

end;
:: original: .supDegree()

redefine func G .maxDegree() -> Nat;

coherence

G .supDegree() is Nat ;

registration
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;
:: original: .supInDegree()

redefine func G .maxInDegree() -> Nat;

coherence

G .supInDegree() is Nat ;

registration

let G be locally-finite with_max_out_degree _Graph;

coherence

G .maxOutDegree() is natural

end;
coherence

G .maxOutDegree() is natural

proof 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;
:: original: .supOutDegree()

redefine func G .maxOutDegree() -> Nat;

coherence

G .supOutDegree() is Nat ;

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 )

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 ) )

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 ) )

( ( 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 )

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 ;

coherence

for b_{1} being reverseEdgeDirections of G,E holds b_{1} is with_max_degree
by Th86;

end;
let E be set ;

coherence

for b

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 ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is with_max_degree

for b_{1} being addLoops of G,V holds b_{1} is with_max_degree

end;
let V be set ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be with_max_degree _Graph;

let v, e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is with_max_degree

for b_{1} being addAdjVertex of G,v,e,w holds b_{1} is with_max_degree

end;
let v, e, w be object ;

coherence

for b

proof end;

coherence for b

proof 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 ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is with_max_degree

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be with_max_in_degree _Graph;

coherence

for b_{1} being reverseEdgeDirections of G holds b_{1} is with_max_out_degree

end;
coherence

for b

proof end;

registration

let G be with_max_in_degree _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is with_max_in_degree

for b_{1} being addLoops of G,V holds b_{1} is with_max_in_degree

end;
let V be set ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be with_max_in_degree _Graph;

let v, e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is with_max_in_degree

for b_{1} being addAdjVertex of G,v,e,w holds b_{1} is with_max_in_degree

end;
let v, e, w be object ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be with_max_in_degree _Graph;

let v be object ;

let V be set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is with_max_in_degree

end;
let v be object ;

let V be set ;

coherence

for b

proof end;

registration

let G be with_max_out_degree _Graph;

coherence

for b_{1} being reverseEdgeDirections of G holds b_{1} is with_max_in_degree

end;
coherence

for b

proof end;

registration

let G be with_max_out_degree _Graph;

let V be set ;

coherence

for b_{1} being addVertices of G,V holds b_{1} is with_max_out_degree

for b_{1} being addLoops of G,V holds b_{1} is with_max_out_degree

end;
let V be set ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be with_max_out_degree _Graph;

let v, e, w be object ;

coherence

for b_{1} being addEdge of G,v,e,w holds b_{1} is with_max_out_degree

for b_{1} being addAdjVertex of G,v,e,w holds b_{1} is with_max_out_degree

end;
let v, e, w be object ;

coherence

for b

proof end;

coherence for b

proof end;

registration

let G be with_max_out_degree _Graph;

let v be object ;

let V be set ;

coherence

for b_{1} being addAdjVertexAll of G,v,V holds b_{1} is with_max_out_degree

end;
let v be object ;

let V be set ;

coherence

for b

proof 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;

:: 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() ) ) )

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() ) ) )

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() ) ) )

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_{1} -edge _Graph holds

( G .maxInDegree() = c & G .minInDegree() = c & G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )

for G being _trivial b

( G .maxInDegree() = c & G .minInDegree() = c & G .maxOutDegree() = c & G .minOutDegree() = c & G .maxDegree() = c +` c & G .minDegree() = c +` c )

proof 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() );

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() );

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() );

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() );

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() );

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() );

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()

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()

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()

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()

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()

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()

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;

existence

ex b_{1} being Vertex of G st b_{1} is with_min_degree

ex b_{1} being Vertex of G st b_{1} is with_min_in_degree

ex b_{1} being Vertex of G st b_{1} is with_min_out_degree

for b_{1} being Vertex of G st b_{1} is with_min_in_degree & b_{1} is with_min_out_degree holds

b_{1} is with_min_degree

for b_{1} being Vertex of G st b_{1} is with_max_in_degree & b_{1} is with_max_out_degree holds

b_{1} is with_max_degree

for b_{1} being Vertex of G st b_{1} is isolated holds

( b_{1} is with_min_degree & b_{1} is with_min_in_degree & b_{1} is with_min_out_degree )

end;
existence

ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

coherence for b

b

proof end;

coherence for b

b

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

( b

proof 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 )

( 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 )

( 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 )

( 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;

existence

ex b_{1} being Vertex of G st b_{1} is with_max_degree
by Th97;

end;
existence

ex b

registration

let G be with_max_in_degree _Graph;

existence

ex b_{1} being Vertex of G st b_{1} is with_max_in_degree
by Th98;

end;
existence

ex b

registration

let G be with_max_out_degree _Graph;

existence

ex b_{1} being Vertex of G st b_{1} is with_max_out_degree
by Th99;

end;
existence

ex b