:: About Regular Graphs
:: by Sebastian Koch
::
:: Received June 30, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

definition

let G be _Graph;

attr G is Dcomplete means :Def1: :: GLIB_016:def 1
for v, w being Vertex of G st v <> w holds
ex e being object st e DJoins v,w,G;

end;

:: deftheorem Def1 defines Dcomplete GLIB_016:def 1 :
for G being _Graph holds
( G is Dcomplete iff for v, w being Vertex of G st v <> w holds
ex e being object st e DJoins v,w,G );

definition

let c be non empty Cardinal;

func canCompleteGraph c -> _Graph equals :: GLIB_016:def 2
createGraph (c,((RelIncl c) \ (id c)));

coherence
createGraph (c,((RelIncl c) \ (id c))) is _Graph ;

func canDCompleteGraph c -> _Graph equals :: GLIB_016:def 3
createGraph (c,([:c,c:] \ (id c)));

coherence
createGraph (c,([:c,c:] \ (id c))) is _Graph ;

end;

:: deftheorem defines canCompleteGraph GLIB_016:def 2 :
for c being non empty Cardinal holds canCompleteGraph c = createGraph (c,((RelIncl c) \ (id c)));

:: deftheorem defines canDCompleteGraph GLIB_016:def 3 :
for c being non empty Cardinal holds canDCompleteGraph c = createGraph (c,([:c,c:] \ (id c)));

registration

let c be non empty Cardinal;

reduce the_Vertices_of (canCompleteGraph c) to c;

correctness
reducibility
the_Vertices_of (canCompleteGraph c) = c;
;

reduce the_Vertices_of (canDCompleteGraph c) to c;

correctness
reducibility
the_Vertices_of (canDCompleteGraph c) = c;
;

end;

registration

let c be non empty Cardinal;

cluster -> ordinal for Element of the_Vertices_of (canCompleteGraph c);

coherence
for b₁ being Vertex of (canCompleteGraph c) holds b₁ is ordinal ;

cluster -> ordinal for Element of the_Vertices_of (canDCompleteGraph c);

coherence
for b₁ being Vertex of (canDCompleteGraph c) holds b₁ is ordinal ;

end;

registration

cluster -> natural for Element of the_Vertices_of (canCompleteGraph omega);

coherence
for b₁ being Vertex of (canCompleteGraph omega) holds b₁ is natural ;

cluster -> natural for Element of the_Vertices_of (canDCompleteGraph omega);

coherence
for b₁ being Vertex of (canDCompleteGraph omega) holds b₁ is natural ;
let n be non zero Nat;

cluster canCompleteGraph n -> _finite ;

coherence
canCompleteGraph n is _finite ;

cluster canDCompleteGraph n -> _finite ;

coherence
canDCompleteGraph n is _finite ;

cluster -> natural for Element of the_Vertices_of (canCompleteGraph n);

coherence
for b₁ being Vertex of (canCompleteGraph n) holds b₁ is natural

proof end;

cluster -> natural for Element of the_Vertices_of (canDCompleteGraph n);

coherence
for b₁ being Vertex of (canDCompleteGraph n) holds b₁ is natural

proof end;

end;

registration

let c be non empty Cardinal;

cluster canCompleteGraph c -> simple complete plain c -vertex ;

coherence
( canCompleteGraph c is plain & canCompleteGraph c is c -vertex & canCompleteGraph c is simple & canCompleteGraph c is complete )

proof end;

cluster canDCompleteGraph c -> Dsimple plain c -vertex Dcomplete ;

coherence
( canDCompleteGraph c is plain & canDCompleteGraph c is c -vertex & canDCompleteGraph c is Dsimple & canDCompleteGraph c is Dcomplete )

proof end;

end;

theorem Th1: :: GLIB_016:1

for c being non empty Cardinal
for v being Vertex of (canCompleteGraph c) holds
( v .inNeighbors() = v & v .outNeighbors() = c \ (succ v) )

proof end;

theorem :: GLIB_016:2

for v being Vertex of (canCompleteGraph omega) holds
( v .inDegree() = v & v .outDegree() = omega )

proof end;

theorem :: GLIB_016:3

for n being non zero Nat
for v being Vertex of (canCompleteGraph n) holds
( v .inDegree() = v & v .outDegree() = (n - v) - 1 )

proof end;

registration

let c be non empty Cardinal;

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

existence
ex b₁ being _Graph st
( b₁ is simple & b₁ is c -vertex & b₁ is complete )

proof end;

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

existence
ex b₁ being _Graph st
( b₁ is Dsimple & b₁ is c -vertex & b₁ is Dcomplete )

proof end;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] Dcomplete -> complete for set ;

coherence
for b₁ being _Graph st b₁ is Dcomplete holds
b₁ is complete

proof end;

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

coherence
for b₁ being _Graph st b₁ is _trivial holds
b₁ is Dcomplete by GLIB_000:116;

cluster Relation-like omega -defined Function-like finite [Graph-like] non _trivial Dcomplete -> non non-multi non edgeless for set ;

coherence
for b₁ being _Graph st not b₁ is _trivial & b₁ is Dcomplete holds
( not b₁ is non-multi & not b₁ is edgeless )

proof end;

end;

registration

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

existence
not for b₁ being _Graph holds b₁ is Dcomplete

proof end;

end;

theorem Th4: :: GLIB_016:4

for G1, G2 being _Graph st G1 == G2 & G1 is Dcomplete holds
G2 is Dcomplete

proof end;

theorem Th5: :: GLIB_016:5

for G1 being _Graph
for G2 being removeLoops of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )

proof end;

theorem Th6: :: GLIB_016:6

for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )

proof end;

theorem Th7: :: GLIB_016:7

for G1 being _Graph
for G2 being DSimpleGraph of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )

proof end;

Lm1: for G1 being _Graph
for G2 being reverseEdgeDirections of G1 st G1 is Dcomplete holds
G2 is Dcomplete

proof end;

theorem Th8: :: GLIB_016:8

for G1 being _Graph
for G2 being reverseEdgeDirections of G1 holds
( G1 is Dcomplete iff G2 is Dcomplete )

proof end;

registration

let G be Dcomplete _Graph;

cluster -> Dcomplete for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds b₁ is Dcomplete by Th5;

cluster -> Dcomplete for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds b₁ is Dcomplete by Th6;

cluster -> Dcomplete for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds b₁ is Dcomplete by Th7;

cluster -> Dcomplete for reverseEdgeDirections of G, the_Edges_of G;

coherence
for b₁ being reverseEdgeDirections of G holds b₁ is Dcomplete by Th8;
let V be set ;

cluster -> Dcomplete for inducedSubgraph of G,V,G .edgesBetween V;

coherence
for b₁ being inducedSubgraph of G,V holds b₁ is Dcomplete

proof end;

cluster -> Dcomplete for addLoops of G,V;

coherence
for b₁ being addLoops of G,V holds b₁ is Dcomplete

proof end;

end;

registration

let G be Dcomplete _Graph;
let v, e, w be object ;

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

coherence
for b₁ being addEdge of G,v,e,w holds b₁ is Dcomplete

proof end;

end;

registration

let G be non Dcomplete _Graph;

cluster -> non Dcomplete for inducedSubgraph of G, the_Vertices_of G,(the_Edges_of G) \ (G .loops());

coherence
for b₁ being removeLoops of G holds not b₁ is Dcomplete by Th5;

cluster -> non Dcomplete for removeDParallelEdges of G;

coherence
for b₁ being removeDParallelEdges of G holds not b₁ is Dcomplete by Th6;

cluster -> non Dcomplete for DSimpleGraph of G;

coherence
for b₁ being DSimpleGraph of G holds not b₁ is Dcomplete by Th7;

cluster -> non Dcomplete for reverseEdgeDirections of G, the_Edges_of G;

coherence
for b₁ being reverseEdgeDirections of G holds not b₁ is Dcomplete by Th8;

cluster spanning -> non Dcomplete for Subgraph of G;

coherence
for b₁ being Subgraph of G st b₁ is spanning holds
not b₁ is Dcomplete

proof end;

end;

theorem Th9: :: GLIB_016:9

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Dcontinuous & F is strong_SG-embedding & G2 is Dcomplete holds
G1 is Dcomplete

proof end;

theorem Th10: :: GLIB_016:10

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is Dcomplete iff G2 is Dcomplete )

proof end;

registration

let G be Dcomplete _Graph;

cluster Relation-like omega -defined Function-like finite [Graph-like] G -Disomorphic -> Dcomplete for set ;

coherence
for b₁ being _Graph st b₁ is G -Disomorphic holds
b₁ is Dcomplete

proof end;

end;

theorem Th11: :: GLIB_016:11

for G being Dcomplete _Graph
for v being Vertex of G holds
( (the_Vertices_of G) \ {v} c= v .inNeighbors() & (the_Vertices_of G) \ {v} c= v .outNeighbors() & (the_Vertices_of G) \ {v} c= v .allNeighbors() )

proof end;

theorem Th12: :: GLIB_016:12

for G being loopless Dcomplete _Graph
for v being Vertex of G holds
( v .inNeighbors() = (the_Vertices_of G) \ {v} & v .outNeighbors() = (the_Vertices_of G) \ {v} & v .allNeighbors() = (the_Vertices_of G) \ {v} )

proof end;

theorem Th13: :: GLIB_016:13

for G being Dsimple Dcomplete _Graph
for v being Vertex of G holds
( (v .inDegree()) +` 1 = G .order() & (v .outDegree()) +` 1 = G .order() )

proof end;

:: more general version of GLIB_012:57

theorem Th14: :: GLIB_016:14

for G1 being _Graph
for G2 being DLGraphComplement of G1 holds
( the_Edges_of G1 = G1 .loops() iff G2 is Dcomplete )

proof end;

registration

let G be edgeless _Graph;

cluster -> Dcomplete for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is Dcomplete

proof end;

end;

:: directed version of GLIB_012:75
:: Proof copied from the reverse version and reordered

theorem Th15: :: GLIB_016:15

for G1 being _Graph
for G2 being DLGraphComplement of G1 holds
( G1 is Dcomplete iff the_Edges_of G2 = G2 .loops() )

proof end;

registration

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

existence
ex b₁ being _Graph st
( b₁ is loopfull & b₁ is Dcomplete )

proof end;

end;

registration

let G be loopfull Dcomplete _Graph;

cluster -> edgeless for DLGraphComplement of G;

coherence
for b₁ being DLGraphComplement of G holds b₁ is edgeless

proof end;

end;

:: more general version of GLIB_012:92
:: also directed version of second part of GLIB_012:113

theorem Th16: :: GLIB_016:16

for G1 being _Graph
for G2 being DGraphComplement of G1 holds
( the_Edges_of G1 = G1 .loops() iff G2 is Dcomplete )

proof end;

registration

let G be edgeless _Graph;

cluster -> Dcomplete for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is Dcomplete

proof end;

end;

:: directed version of first part of GLIB_012:113

theorem Th17: :: GLIB_016:17

for G1 being _Graph
for G2 being DGraphComplement of G1 holds
( G1 is Dcomplete iff G2 is edgeless )

proof end;

registration

let G be Dcomplete _Graph;

cluster -> edgeless for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is edgeless by Th17;

end;

registration

let G be non Dcomplete _Graph;

cluster -> non edgeless for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds not b₁ is edgeless by Th17;

end;

registration

let G1 be _Graph;
let G2 be DLGraphComplement of G1;

cluster -> Dcomplete for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is Dcomplete by GLIB_014:30;

end;

registration

let G1 be _Graph;
let G2 be DGraphComplement of G1;

cluster -> Dcomplete for GraphUnion of G1,G2;

coherence
for b₁ being GraphUnion of G1,G2 holds b₁ is Dcomplete by GLIB_014:32;

end;

theorem :: GLIB_016:18

for G being _Graph holds
( G is Dcomplete iff [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) c= VertexDomRel G )

proof end;

:: Proof mostly copied from previous one

theorem :: GLIB_016:19

for V being non empty set
for E being Relation of V holds
( createGraph (V,E) is Dcomplete iff [:V,V:] \ (id V) c= E )

proof end;

definition

let c be Cardinal;
let G be _Graph;

attr G is c -regular means :Def4: :: GLIB_016:def 4
for v being Vertex of G holds v .degree() = c;

end;

:: deftheorem Def4 defines -regular GLIB_016:def 4 :
for c being Cardinal
for G being _Graph holds
( G is c -regular iff for v being Vertex of G holds v .degree() = c );

registration

let c be Cardinal;

cluster Relation-like omega -defined Function-like finite [Graph-like] c -regular -> with_max_degree for set ;

coherence
for b₁ being _Graph st b₁ is c -regular holds
b₁ is with_max_degree

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] simple complete c +` 1 -vertex -> c -regular for set ;

coherence
for b₁ being _Graph st b₁ is c +` 1 -vertex & b₁ is simple & b₁ is complete holds
b₁ is c -regular

proof end;

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

existence
ex b₁ being _Graph st
( b₁ is simple & b₁ is c -regular )

proof end;

end;

:: Degree of regularity is unique.

theorem Th20: :: GLIB_016:20

for c1, c2 being Cardinal
for G being _Graph st G is c1 -regular & G is c2 -regular holds
c1 = c2

proof end;

theorem Th21: :: GLIB_016:21

for c being Cardinal
for G being _Graph holds
( G is c -regular iff for C being Component of G holds C is c -regular )

proof end;

registration

let c be Cardinal;

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

existence
not for b₁ being _Graph holds b₁ is c -regular

proof end;

let G be c -regular _Graph;

cluster Component-like -> c -regular for Subgraph of G;

coherence
for b₁ being Component of G holds b₁ is c -regular by Th21;

end;

theorem Th22: :: GLIB_016:22

for c being Cardinal
for G being b₁ -regular _Graph holds
( G .minDegree() = c & G .maxDegree() = c )

proof end;

theorem Th23: :: GLIB_016:23

for c being Cardinal
for G being _Graph st G .minDegree() = c & G .supDegree() = c holds
G is c -regular

proof end;

registration

let n be Nat;

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

coherence
for b₁ being _Graph st b₁ is n -regular holds
b₁ is locally-finite

proof end;

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

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

proof end;

end;

theorem Th24: :: GLIB_016:24

for G being _Graph holds
( G is edgeless iff G is 0 -regular )

proof end;

registration

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

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

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

coherence
for b₁ being _Graph st b₁ is 0 -regular holds
b₁ is edgeless by Th24;

end;

registration

let c be non empty Cardinal;

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

coherence
for b₁ being _Graph st b₁ is c -regular holds
not b₁ is edgeless

proof end;

end;

:: this is just a special case of
:: cluster without_isolated_vertices edge-finite -> vertex-finite
:: and
:: cluster c-regular -> without_isolated_vertices
:: registration
:: let c be non empty Cardinal;
:: cluster c-regular edge-finite -> vertex-finite for _Graph;
:: coherence;
:: end;

theorem :: GLIB_016:25

for c being Cardinal
for G being simple b₁ -regular _Graph holds c c= G .order()

proof end;

theorem Th26: :: GLIB_016:26

for n being Nat
for G1 being simple vertex-finite b₁ -regular _Graph
for G2 being GraphComplement of G1 holds G2 is (G1 .order()) -' (n + 1) -regular

proof end;

theorem Th27: :: GLIB_016:27

for c being Cardinal
for G being _Graph st ex v being Vertex of G st v is isolated & G is c -regular holds
c = 0

proof end;

theorem Th28: :: GLIB_016:28

for c being Cardinal
for G being _Graph st ex v being Vertex of G st v is endvertex & G is c -regular holds
c = 1

proof end;

registration

let G be 1 -regular _Graph;

cluster -> endvertex for Element of the_Vertices_of G;

coherence
for b₁ being Vertex of G holds b₁ is endvertex

proof end;

end;

theorem Th29: :: GLIB_016:29

for G being 1 -regular _Graph
for T being Trail of G st T is trivial holds
ex e being object st
( e Joins T .first() ,T .last() ,G & T = G .walkOf ((T .first()),e,(T .last())) )

proof end;

::$INSERT The connected $1$-regular graph is $K_2$

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] connected 1 -regular -> complete 2 -vertex 1 -edge for set ;

coherence
for b₁ being _Graph st b₁ is 1 -regular & b₁ is connected holds
( b₁ is 2 -vertex & b₁ is 1 -edge & b₁ is complete )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] simple connected 2 -vertex -> 1 -regular for set ;

coherence
for b₁ being _Graph st b₁ is simple & b₁ is 2 -vertex & b₁ is connected holds
b₁ is 1 -regular

proof end;

end;

Lm2: for c being Cardinal
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism & G1 is c -regular holds
G2 is c -regular

proof end;

theorem Th30: :: GLIB_016:30

for c being Cardinal
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is c -regular iff G2 is c -regular )

proof end;

theorem Th31: :: GLIB_016:31

for c being Cardinal
for G1, G2 being _Graph st G1 == G2 & G1 is c -regular holds
G2 is c -regular

proof end;

theorem Th32: :: GLIB_016:32

for c being Cardinal
for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is c -regular iff G2 is c -regular )

proof end;

:: The 1-regular graphs are sometimes called ladder graph or ladder rung graph
:: but since it is rarely used in the literature, it is omitted here.
:: If you think a definition is needed nonetheless, please use the
:: term "ladder-rung" rather than "ladder" cause the latter is more often used
:: to refer to P_n x P_2 instead of nP_2.
:: On the other hand cubic graphs are often used AND shorten the number of
:: characters needed for the attribute descriptor, hence they are defined here.

definition

let G be _Graph;

attr G is cubic means :: GLIB_016:def 5
G is 3 -regular ;

end;

:: deftheorem defines cubic GLIB_016:def 5 :
for G being _Graph holds
( G is cubic iff G is 3 -regular );

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] cubic -> 3 -regular for set ;

coherence
for b₁ being _Graph st b₁ is cubic holds
b₁ is 3 -regular ;

cluster Relation-like omega -defined Function-like finite [Graph-like] 3 -regular -> cubic for set ;

coherence
for b₁ being _Graph st b₁ is 3 -regular holds
b₁ is cubic ;

end;

theorem :: GLIB_016:33

for G being _Graph holds
( G is cubic iff for v being Vertex of G holds v .degree() = 3 ) by Def4;

theorem :: GLIB_016:34

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is cubic iff G2 is cubic ) by Th30;

theorem :: GLIB_016:35

for G1, G2 being _Graph st G1 == G2 & G1 is cubic holds
G2 is cubic by Th31;

theorem :: GLIB_016:36

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is cubic iff G2 is cubic ) by Th32;

definition

let G be _Graph;

attr G is regular means :Def6: :: GLIB_016:def 6
ex c being Cardinal st G is c -regular ;

end;

:: deftheorem Def6 defines regular GLIB_016:def 6 :
for G being _Graph holds
( G is regular iff ex c being Cardinal st G is c -regular );

theorem :: GLIB_016:37

for G being _Graph holds
( G is regular iff G .minDegree() = G .supDegree() )

proof end;

definition

let G be locally-finite _Graph;

redefine attr G is regular means :Def7: :: GLIB_016:def 7
ex n being Nat st G is n -regular ;

compatibility
( G is regular iff ex n being Nat st G is n -regular )

proof end;

end;

:: deftheorem Def7 defines regular GLIB_016:def 7 :
for G being locally-finite _Graph holds
( G is regular iff ex n being Nat st G is n -regular );

registration

let c be Cardinal;

cluster Relation-like omega -defined Function-like finite [Graph-like] c -regular -> regular for set ;

coherence
for b₁ being _Graph st b₁ is c -regular holds
b₁ is regular ;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] cubic -> regular for set ;

coherence
for b₁ being _Graph st b₁ is cubic holds
b₁ is regular ;

cluster Relation-like omega -defined Function-like finite [Graph-like] regular -> with_max_degree for set ;

coherence
for b₁ being _Graph st b₁ is regular holds
b₁ is with_max_degree ;

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

existence
ex b₁ being _Graph st
( b₁ is simple & not b₁ is edgeless & b₁ is finite & b₁ is regular )

proof end;

end;

registration

let G be regular _Graph;

cluster Component-like -> regular for Subgraph of G;

coherence
for b₁ being Component of G holds b₁ is regular

proof end;

end;

registration

let G be _finite simple regular _Graph;

cluster -> regular for GraphComplement of G;

coherence
for b₁ being GraphComplement of G holds b₁ is regular

proof end;

end;

theorem :: GLIB_016:38

for G being _Graph st ex v being Vertex of G st v is isolated & G is regular holds
G is edgeless

proof end;

theorem :: GLIB_016:39

for G being _Graph st ex v being Vertex of G st v is endvertex & G is regular holds
G is 1 -regular

proof end;

theorem Th40: :: GLIB_016:40

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is regular iff G2 is regular )

proof end;

theorem :: GLIB_016:41

for G1, G2 being _Graph st G1 == G2 & G1 is regular holds
G2 is regular

proof end;

theorem :: GLIB_016:42

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is regular iff G2 is regular )

proof end;

definition

let c be Cardinal;
let G be _Graph;

attr G is c -Dregular means :Def8: :: GLIB_016:def 8
for v being Vertex of G holds
( v .inDegree() = c & v .outDegree() = c );

end;

:: deftheorem Def8 defines -Dregular GLIB_016:def 8 :
for c being Cardinal
for G being _Graph holds
( G is c -Dregular iff for v being Vertex of G holds
( v .inDegree() = c & v .outDegree() = c ) );

registration

let c be Cardinal;

cluster Relation-like omega -defined Function-like finite [Graph-like] c -Dregular -> with_max_in_degree with_max_out_degree for set ;

coherence
for b₁ being _Graph st b₁ is c -Dregular holds
( b₁ is with_max_in_degree & b₁ is with_max_out_degree )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] Dsimple c +` 1 -vertex Dcomplete -> c -Dregular for set ;

coherence
for b₁ being _Graph st b₁ is c +` 1 -vertex & b₁ is Dsimple & b₁ is Dcomplete holds
b₁ is c -Dregular

proof end;

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

existence
ex b₁ being _Graph st
( b₁ is Dsimple & b₁ is c -Dregular )

proof end;

end;

:: Degree of directed regularity is unique.

theorem Th43: :: GLIB_016:43

for c1, c2 being Cardinal
for G being _Graph st G is c1 -Dregular & G is c2 -Dregular holds
c1 = c2

proof end;

registration

let c be Cardinal;

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

existence
not for b₁ being _Graph holds b₁ is c -Dregular

proof end;

let G be c -Dregular _Graph;

cluster Component-like -> c -Dregular for Subgraph of G;

coherence
for b₁ being Component of G holds b₁ is c -Dregular

proof end;

end;

theorem Th44: :: GLIB_016:44

for c being Cardinal
for G being b₁ -Dregular _Graph holds
( G .minInDegree() = c & G .minOutDegree() = c & G .maxInDegree() = c & G .maxOutDegree() = c )

proof end;

theorem Th45: :: GLIB_016:45

for c being Cardinal
for G being _Graph st G .minInDegree() = c & G .minOutDegree() = c & G .supInDegree() = c & G .supOutDegree() = c holds
G is c -Dregular

proof end;

theorem Th46: :: GLIB_016:46

for G being _Graph
for n being Nat st G is n -Dregular holds
G is 2 * n -regular

proof end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n -Dregular -> locally-finite 2 * n -regular for set ;

coherence
for b₁ being _Graph st b₁ is n -Dregular holds
( b₁ is 2 * n -regular & b₁ is locally-finite )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] _finite Dsimple non 0 -vertex n -Dregular for set ;

existence
ex b₁ being _Graph st
( b₁ is Dsimple & b₁ is _finite & b₁ is n -Dregular )

proof end;

end;

registration

let c be infinite Cardinal;

cluster Relation-like omega -defined Function-like finite [Graph-like] c -Dregular -> c -regular for set ;

coherence
for b₁ being _Graph st b₁ is c -Dregular holds
b₁ is c -regular

proof end;

end;

theorem Th47: :: GLIB_016:47

for G being _Graph holds
( G is edgeless iff G is 0 -Dregular )

proof end;

registration

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

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

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

coherence
for b₁ being _Graph st b₁ is 0 -Dregular holds
b₁ is edgeless by Th47;

end;

registration

let c be non empty Cardinal;

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

coherence
for b₁ being _Graph st b₁ is c -Dregular holds
not b₁ is edgeless

proof end;

end;

:: same as above
:: registration
:: let c be non empty Cardinal;
:: cluster c-Dregular edge-finite -> vertex-finite for _Graph;
:: coherence;
:: end;

theorem :: GLIB_016:48

for c being Cardinal
for G being Dsimple b₁ -Dregular _Graph holds c c= G .order()

proof end;

theorem Th49: :: GLIB_016:49

for n being Nat
for G1 being Dsimple vertex-finite b₁ -Dregular _Graph
for G2 being DGraphComplement of G1 holds G2 is (G1 .order()) -' (n + 1) -Dregular

proof end;

theorem :: GLIB_016:50

for c being Cardinal
for G being _Graph st ex v being Vertex of G st v is isolated & G is c -Dregular holds
c = 0

proof end;

registration

let c be Cardinal;
let G be c -Dregular _Graph;

cluster -> non endvertex for Element of the_Vertices_of G;

coherence
for b₁ being Vertex of G holds not b₁ is endvertex

proof end;

end;

:: A connected 1-Dregular graph is either K2 with an additional edge in
:: the other direction, the trivial graph with 1 loop or a collection
:: of directed cycles or directed double rays (the latter two not shown here).

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] Dsimple 2 -vertex 2 -edge -> complete 1 -Dregular for set ;

coherence
for b₁ being _Graph st b₁ is 2 -edge & b₁ is 2 -vertex & b₁ is Dsimple holds
( b₁ is 1 -Dregular & b₁ is complete )

proof end;

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

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is 1 -edge holds
b₁ is 1 -Dregular

proof end;

end;

Lm3: for c being Cardinal
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism & G1 is c -Dregular holds
G2 is c -Dregular

proof end;

theorem Th51: :: GLIB_016:51

for c being Cardinal
for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is c -Dregular iff G2 is c -Dregular )

proof end;

theorem :: GLIB_016:52

for c being Cardinal
for G1, G2 being _Graph st G1 == G2 & G1 is c -Dregular holds
G2 is c -Dregular

proof end;

definition

let G be _Graph;

attr G is Dregular means :Def9: :: GLIB_016:def 9
ex c being Cardinal st G is c -Dregular ;

end;

:: deftheorem Def9 defines Dregular GLIB_016:def 9 :
for G being _Graph holds
( G is Dregular iff ex c being Cardinal st G is c -Dregular );

theorem :: GLIB_016:53

for G being _Graph holds
( G is Dregular iff ( G .minInDegree() = G .supInDegree() & G .minOutDegree() = G .supOutDegree() & G .minInDegree() = G .minOutDegree() ) )

proof end;

definition

let G be locally-finite _Graph;

redefine attr G is Dregular means :Def10: :: GLIB_016:def 10
ex n being Nat st G is n -Dregular ;

compatibility
( G is Dregular iff ex n being Nat st G is n -Dregular )

proof end;

end;

:: deftheorem Def10 defines Dregular GLIB_016:def 10 :
for G being locally-finite _Graph holds
( G is Dregular iff ex n being Nat st G is n -Dregular );

registration

let c be Cardinal;

cluster Relation-like omega -defined Function-like finite [Graph-like] c -Dregular -> Dregular for set ;

coherence
for b₁ being _Graph st b₁ is c -Dregular holds
b₁ is Dregular ;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] Dregular -> with_max_degree for set ;

coherence
for b₁ being _Graph st b₁ is Dregular holds
b₁ is with_max_degree ;

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

existence
ex b₁ being _Graph st
( b₁ is Dsimple & not b₁ is edgeless & b₁ is finite & b₁ is Dregular )

proof end;

end;

registration

let G be Dregular _Graph;

cluster Component-like -> Dregular for Subgraph of G;

coherence
for b₁ being Component of G holds b₁ is Dregular

proof end;

end;

registration

let G be _finite Dsimple Dregular _Graph;

cluster -> Dregular for DGraphComplement of G;

coherence
for b₁ being DGraphComplement of G holds b₁ is Dregular

proof end;

end;

registration

let G be Dregular _Graph;

cluster -> non endvertex for Element of the_Vertices_of G;

coherence
for b₁ being Vertex of G holds not b₁ is endvertex

proof end;

end;

theorem Th54: :: GLIB_016:54

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is Dregular iff G2 is Dregular )

proof end;

theorem :: GLIB_016:55

for G1, G2 being _Graph st G1 == G2 & G1 is Dregular holds
G2 is Dregular

proof end;

:: basically infinite version of GROUP_2:156

theorem Th56: :: GLIB_016:56

for P being set
for c being Cardinal st P is mutually-disjoint & ( for A being set st A in P holds
card A = c ) holds
card (union P) = c *` (card P)

proof end;

theorem :: GLIB_016:57

for X being non empty set
for P being a_partition of X
for c being Cardinal st ( for x being Element of X holds card (EqClass (x,P)) = c ) holds
card X = c *` (card P)

proof end;

registration

let f be Function;
let X be set ;

cluster <:f,(id X):> -> one-to-one ;

coherence
<:f,(id X):> is one-to-one

proof end;

end;

registration

let f be one-to-one Function;

cluster f ~ -> one-to-one ;

coherence
f ~ is one-to-one

proof end;

cluster ~ f -> one-to-one ;

coherence
~ f is one-to-one by FUNCTOR0:8;

end;

registration

let X be set ;
let f be Function;

cluster <:(id X),f:> -> one-to-one ;

coherence
<:(id X),f:> is one-to-one

proof end;

end;

deffunc H₁( _Graph) -> set = <:(the_Source_of $1),(id (the_Edges_of $1)):>;

deffunc H₂( _Graph) -> set = <:(the_Target_of $1),(id (the_Edges_of $1)):>;

deffunc H₃( _Graph) -> set = [:H₁($1),(id {0}):];

deffunc H₄( _Graph) -> set = [:H₂($1),(id {1}):];

deffunc H₅( _Graph) -> set = H₃($1) +* H₄($1);

deffunc H₆( _Graph, Vertex of $1) -> set = [:{$2},($2 .edgesOut()),{0}:];

deffunc H₇( _Graph, Vertex of $1) -> set = [:{$2},($2 .edgesIn()),{1}:];

deffunc H₈( _Graph) -> set = { (H₆($1,v) \/ H₇($1,v)) where v is Vertex of $1 : not v is isolated } ;

Lm4: for G being _Graph holds
( dom H₁(G) = the_Edges_of G & dom H₂(G) = the_Edges_of G )

proof end;

Lm5: for G being _Graph holds
( dom H₃(G) = [:(the_Edges_of G),{0}:] & dom H₄(G) = [:(the_Edges_of G),{1}:] )

proof end;

Lm6: for G being _Graph holds dom H₃(G) misses dom H₄(G)

proof end;

Lm7: for G being _Graph holds rng H₃(G) misses rng H₄(G)

proof end;

Lm8: for G being _Graph holds H₅(G) is one-to-one

proof end;

Lm9: for G being _Graph holds dom H₅(G) = [:(the_Edges_of G),{0,1}:]

proof end;

Lm10: for G being _Graph
for v0, v1 being Vertex of G holds H₆(G,v0) misses H₇(G,v1)

proof end;

Lm11: for c being Cardinal
for G being b₁ -regular _Graph
for v being Vertex of G holds card (H₆(G,v) \/ H₇(G,v)) = c

proof end;

Lm12: for G being _Graph
for v, w being Vertex of G st H₆(G,v) meets H₆(G,w) holds
v = w

proof end;

Lm13: for G being _Graph
for v, w being Vertex of G st H₇(G,v) meets H₇(G,w) holds
v = w

proof end;

Lm14: for G being _Graph holds H₈(G) is mutually-disjoint

proof end;

Lm15: for c being non empty Cardinal
for G being b₁ -regular _Graph holds card H₈(G) = G .order()

proof end;

Lm16: for G being _Graph holds rng H₅(G) = union H₈(G)

proof end;

theorem :: GLIB_016:58

for c being Cardinal
for G being b₁ -regular _Graph holds 2 *` (G .size()) = c *` (G .order())

proof end;

definition

let G be _Graph;

func G .degreeMap() -> ManySortedSet of the_Vertices_of G means :Def11: :: GLIB_016:def 11
for v being Vertex of G holds it . v = v .degree() ;

existence
ex b₁ being ManySortedSet of the_Vertices_of G st
for v being Vertex of G holds b₁ . v = v .degree()

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of the_Vertices_of G st ( for v being Vertex of G holds b₁ . v = v .degree() ) & ( for v being Vertex of G holds b₂ . v = v .degree() ) holds
b₁ = b₂

proof end;

func G .inDegreeMap() -> ManySortedSet of the_Vertices_of G means :Def12: :: GLIB_016:def 12
for v being Vertex of G holds it . v = v .inDegree() ;

existence
ex b₁ being ManySortedSet of the_Vertices_of G st
for v being Vertex of G holds b₁ . v = v .inDegree()

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of the_Vertices_of G st ( for v being Vertex of G holds b₁ . v = v .inDegree() ) & ( for v being Vertex of G holds b₂ . v = v .inDegree() ) holds
b₁ = b₂

proof end;

func G .outDegreeMap() -> ManySortedSet of the_Vertices_of G means :Def13: :: GLIB_016:def 13
for v being Vertex of G holds it . v = v .outDegree() ;

existence
ex b₁ being ManySortedSet of the_Vertices_of G st
for v being Vertex of G holds b₁ . v = v .outDegree()

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of the_Vertices_of G st ( for v being Vertex of G holds b₁ . v = v .outDegree() ) & ( for v being Vertex of G holds b₂ . v = v .outDegree() ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines .degreeMap() GLIB_016:def 11 :
for G being _Graph
for b₂ being ManySortedSet of the_Vertices_of G holds
( b₂ = G .degreeMap() iff for v being Vertex of G holds b₂ . v = v .degree() );

:: deftheorem Def12 defines .inDegreeMap() GLIB_016:def 12 :
for G being _Graph
for b₂ being ManySortedSet of the_Vertices_of G holds
( b₂ = G .inDegreeMap() iff for v being Vertex of G holds b₂ . v = v .inDegree() );

:: deftheorem Def13 defines .outDegreeMap() GLIB_016:def 13 :
for G being _Graph
for b₂ being ManySortedSet of the_Vertices_of G holds
( b₂ = G .outDegreeMap() iff for v being Vertex of G holds b₂ . v = v .outDegree() );

registration

let G be _Graph;

cluster G .degreeMap() -> Cardinal-yielding ;

coherence
G .degreeMap() is Cardinal-yielding

proof end;

cluster G .inDegreeMap() -> Cardinal-yielding ;

coherence
G .inDegreeMap() is Cardinal-yielding

proof end;

cluster G .outDegreeMap() -> Cardinal-yielding ;

coherence
G .outDegreeMap() is Cardinal-yielding

proof end;

end;

theorem Th59: :: GLIB_016:59

for G being _Graph holds
( card (G .degreeMap()) = G .order() & card (G .inDegreeMap()) = G .order() & card (G .outDegreeMap()) = G .order() )

proof end;

theorem Th60: :: GLIB_016:60

for G being _Graph
for v being Vertex of G holds (G .degreeMap()) . v = ((G .inDegreeMap()) . v) +` ((G .outDegreeMap()) . v)

proof end;

registration

let G be locally-finite _Graph;

cluster G .degreeMap() -> natural-valued ;

coherence
G .degreeMap() is natural-valued

proof end;

cluster G .inDegreeMap() -> natural-valued ;

coherence
G .inDegreeMap() is natural-valued

proof end;

cluster G .outDegreeMap() -> natural-valued ;

coherence
G .outDegreeMap() is natural-valued

proof end;

end;

definition

let G be locally-finite _Graph;
:: original: .degreeMap()
redefine func G .degreeMap() -> Function of (the_Vertices_of G),NAT;
coherence
G .degreeMap() is Function of (the_Vertices_of G),NAT

proof end;

:: original: .inDegreeMap()
redefine func G .inDegreeMap() -> Function of (the_Vertices_of G),NAT;
coherence
G .inDegreeMap() is Function of (the_Vertices_of G),NAT

proof end;

:: original: .outDegreeMap()
redefine func G .outDegreeMap() -> Function of (the_Vertices_of G),NAT;
coherence
G .outDegreeMap() is Function of (the_Vertices_of G),NAT

proof end;

end;

registration

let G be vertex-finite _Graph;

cluster G .degreeMap() -> finite ;

coherence
G .degreeMap() is finite

proof end;

cluster G .inDegreeMap() -> finite ;

coherence
G .inDegreeMap() is finite

proof end;

cluster G .outDegreeMap() -> finite ;

coherence
G .outDegreeMap() is finite

proof end;

end;

theorem Th61: :: GLIB_016:61

for c being Cardinal
for G being _trivial b₁ -edge _Graph
for v being Vertex of G holds
( G .inDegreeMap() = v .--> c & G .outDegreeMap() = v .--> c & G .degreeMap() = v .--> (2 *` c) )

proof end;

registration

let G be _trivial _Graph;

cluster G .degreeMap() -> trivial ;

coherence
G .degreeMap() is trivial

proof end;

cluster G .inDegreeMap() -> trivial ;

coherence
G .inDegreeMap() is trivial

proof end;

cluster G .outDegreeMap() -> trivial ;

coherence
G .outDegreeMap() is trivial

proof end;

end;

:: theorem
:: for G1, G2 being _Graph, f being PVertexMapping of G1, G2
:: st f is isomorphism holds G2.degreeMap() = G1.degreeMap() * f;
::
:: theorem
:: for G1, G2 being _Graph, f being PVertexMapping of G1, G2
:: st f is Disomorphism holds
:: G2.inDegreeMap() = G1.inDegreeMap() * f &
:: G2.outDegreeMap() = G1.outDegreeMap() * f;
::
:: theorem
:: for G1, G2 being _Graph st G1 == G2 holds
:: G1.degreeMap() = G2.degreeMap() & G1.inDegreeMap() = G2.inDegreeMap() &
:: G1.outDegreeMap() = G2.outDegreeMap();
::
:: theorem
:: for G1 being _Graph, E being set, G2 being reverseEdgeDirections of G1, E
:: holds G1.degreeMap() = G2.degreeMap();

theorem :: GLIB_016:62

for G2 being _Graph
for V being set
for G1 being addVertices of G2,V holds
( G1 .degreeMap() = (G2 .degreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .inDegreeMap() = (G2 .inDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) & G1 .outDegreeMap() = (G2 .outDegreeMap()) +* ((V \ (the_Vertices_of G2)) --> 0) )

proof end;

theorem :: GLIB_016:63

for G being _Graph
for C being Component of G holds
( C .degreeMap() = (G .degreeMap()) | (the_Vertices_of C) & C .inDegreeMap() = (G .inDegreeMap()) | (the_Vertices_of C) & C .outDegreeMap() = (G .outDegreeMap()) | (the_Vertices_of C) )

proof end;

registration

let G be _Graph;
let v be Denumeration of (the_Vertices_of G);

cluster v * (G .degreeMap()) -> Sequence-like G .order() -element ;

coherence
( (G .degreeMap()) * v is Sequence-like & (G .degreeMap()) * v is G .order() -element )

proof end;

cluster v * (G .inDegreeMap()) -> Sequence-like G .order() -element ;

coherence
( (G .inDegreeMap()) * v is Sequence-like & (G .inDegreeMap()) * v is G .order() -element )

proof end;

cluster v * (G .outDegreeMap()) -> Sequence-like G .order() -element ;

coherence
( (G .outDegreeMap()) * v is Sequence-like & (G .outDegreeMap()) * v is G .order() -element )

proof end;

end;

theorem Th64: :: GLIB_016:64

for G being _finite _Graph
for v being Denumeration of (the_Vertices_of G) holds (G .degreeMap()) * v = ((G .inDegreeMap()) * v) + ((G .outDegreeMap()) * v)

proof end;

theorem Th65: :: GLIB_016:65

for G being _finite _Graph
for v being Denumeration of (the_Vertices_of G) holds
( G .size() = Sum ((G .inDegreeMap()) * v) & G .size() = Sum ((G .outDegreeMap()) * v) )

proof end;

theorem Th66: :: GLIB_016:66

for G being _finite _Graph
for v being Denumeration of (the_Vertices_of G) holds 2 * (G .size()) = Sum ((G .degreeMap()) * v)

proof end;

::#MR Handshaking Lemma

theorem :: GLIB_016:67

for G being _finite _Graph
for k being Nat st k = card { w where w is Vertex of G : not w .degree() is even } holds
k is even

proof end;