:: Introduction to Graph Colorings
:: by Sebastian Koch
::
:: Received July 23, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

definition

let G be _Graph;
mode VColoring of G is ManySortedSet of the_Vertices_of G;

end;

registration

let G be _Graph;

cluster Relation-like the_Vertices_of G -defined Function-like total -> non empty for set ;

coherence
for b₁ being VColoring of G holds not b₁ is empty

proof end;

end;

theorem Th1: :: GLCOLO00:1

for G being _Graph
for f being VColoring of G
for f9 being Function st rng f c= dom f9 holds
f9 * f is VColoring of G

proof end;

definition

let G be _Graph;
let f be VColoring of G;
let f9 be ManySortedSet of rng f;
:: original: *
redefine func f9 * f -> VColoring of G;
coherence
f * f9 is VColoring of G

proof end;

end;

:: might need Proof outside this article

theorem :: GLCOLO00:2

for G being _Graph
for f being VColoring of G
for v being Vertex of G
for x being object holds f +* (v .--> x) is VColoring of G ;

theorem Th3: :: GLCOLO00:3

for G being _Graph
for f being VColoring of G
for H being Subgraph of G holds f | (the_Vertices_of H) is VColoring of H

proof end;

theorem Th4: :: GLCOLO00:4

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V
for f being VColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) holds
f +* h is VColoring of G1

proof end;

:: since the vertices do not change for addEdge, no extra theorem is provided

theorem :: GLCOLO00:5

for G2 being _Graph
for v, e, x being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for f being VColoring of G2 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
f +* (v .--> x) is VColoring of G1

proof end;

theorem Th6: :: GLCOLO00:6

for G2 being _Graph
for v being Vertex of G2
for e, w, x being object
for G1 being addAdjVertex of G2,v,e,w
for f being VColoring of G2 st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
f +* (w .--> x) is VColoring of G1

proof end;

theorem Th7: :: GLCOLO00:7

for G2 being _Graph
for v, x being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f2 being VColoring of G2 st not v in the_Vertices_of G2 holds
f2 +* (v .--> x) is VColoring of G1

proof end;

theorem Th8: :: GLCOLO00:8

for G, G1 being _Graph
for f being VColoring of G
for F being PGraphMapping of G1,G st dom (F _V) = the_Vertices_of G1 holds
f * (F _V) is VColoring of G1

proof end;

theorem Th9: :: GLCOLO00:9

for G, G1 being _Graph
for f being VColoring of G
for F being PGraphMapping of G1,G st F is total holds
f * (F _V) is VColoring of G1

proof end;

definition

let G be _Graph;
let f be VColoring of G;

attr f is proper means :: GLCOLO00:def 1
for v, w being Vertex of G st v,w are_adjacent holds
f . v <> f . w;

end;

:: deftheorem defines proper GLCOLO00:def 1 :
for G being _Graph
for f being VColoring of G holds
( f is proper iff for v, w being Vertex of G st v,w are_adjacent holds
f . v <> f . w );

theorem Th10: :: GLCOLO00:10

for G being _Graph
for f being VColoring of G holds
( f is proper iff for e, v, w being object st e Joins v,w,G holds
f . v <> f . w )

proof end;

theorem Th11: :: GLCOLO00:11

for G being _Graph
for f being VColoring of G holds
( f is proper iff for e, v, w being object st e DJoins v,w,G holds
f . v <> f . w )

proof end;

theorem Th12: :: GLCOLO00:12

for G being _Graph
for f being VColoring of G
for f9 being one-to-one Function
for f2 being VColoring of G st f2 = f9 * f & f is proper & rng f c= dom f9 holds
f2 is proper

proof end;

theorem :: GLCOLO00:13

for G being _Graph
for f being VColoring of G
for f9 being one-to-one ManySortedSet of rng f st f is proper holds
f9 * f is proper

proof end;

theorem Th14: :: GLCOLO00:14

for G being _Graph st ex f being VColoring of G st f is proper holds
G is loopless

proof end;

registration

let G be non loopless _Graph;

cluster Relation-like the_Vertices_of G -defined Function-like total -> non proper for set ;

coherence
for b₁ being VColoring of G holds not b₁ is proper by Th14;

end;

registration

let G be loopless _Graph;

cluster Relation-like the_Vertices_of G -defined Function-like one-to-one total -> proper for set ;

coherence
for b₁ being VColoring of G st b₁ is one-to-one holds
b₁ is proper

proof end;

end;

registration

let G be loopless _Graph;

cluster non empty Relation-like the_Vertices_of G -defined Function-like one-to-one total proper for set ;

existence
ex b₁ being VColoring of G st
( b₁ is one-to-one & b₁ is proper )

proof end;

end;

theorem Th15: :: GLCOLO00:15

for G being _Graph
for f being VColoring of G
for H being Subgraph of G
for f9 being VColoring of H st f9 = f | (the_Vertices_of H) & f is proper holds
f9 is proper

proof end;

theorem Th16: :: GLCOLO00:16

for G1, G2 being _Graph
for f1 being VColoring of G1
for f2 being VColoring of G2 st G1 == G2 & f1 = f2 & f1 is proper holds
f2 is proper

proof end;

theorem Th17: :: GLCOLO00:17

for G1, G2 being _Graph
for f1 being VColoring of G1
for f2 being VColoring of G2
for v being Vertex of G1
for x being object st G1 == G2 & f2 = f1 +* (v .--> x) & not x in rng f1 & f1 is proper holds
f2 is proper

proof end;

Lm1: for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 & f1 is proper holds
f2 is proper

proof end;

theorem Th18: :: GLCOLO00:18

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 holds
( f1 is proper iff f2 is proper )

proof end;

theorem Th19: :: GLCOLO00:19

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V
for f1 being VColoring of G1
for f2 being VColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & f1 = f2 +* h & f2 is proper holds
f1 is proper

proof end;

theorem Th20: :: GLCOLO00:20

for G2 being _Graph
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 & v,w are_adjacent & f2 is proper holds
f1 is proper

proof end;

theorem Th21: :: GLCOLO00:21

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (v .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper

proof end;

theorem Th22: :: GLCOLO00:22

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st f1 = f2 +* (w .--> x) & v <> w & not x in rng f2 & f2 is proper holds
f1 is proper

proof end;

theorem Th23: :: GLCOLO00:23

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2 . w & f2 is proper holds
f1 is proper

proof end;

theorem Th24: :: GLCOLO00:24

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2
for x being object st not w in the_Vertices_of G2 & f1 = f2 +* (w .--> x) & x <> f2 . v & f2 is proper holds
f1 is proper

proof end;

theorem Th25: :: GLCOLO00:25

for G2 being _Graph
for v, x being object
for V being Subset of (the_Vertices_of G2)
for G1 being addAdjVertexAll of G2,v,V
for f1 being VColoring of G1
for f2 being VColoring of G2 st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & not x in rng f2 & f2 is proper holds
f1 is proper

proof end;

theorem Th26: :: GLCOLO00:26

for G, G1 being _Graph
for f being VColoring of G
for F being PGraphMapping of G1,G
for f9 being VColoring of G1 st F is total & f9 = f * (F _V) & f is proper holds
f9 is proper

proof end;

definition

let c be Cardinal;
let G be _Graph;

attr G is c -vcolorable means :: GLCOLO00:def 2
ex f being VColoring of G st
( f is proper & card (rng f) c= c );

end;

:: deftheorem defines -vcolorable GLCOLO00:def 2 :
for c being Cardinal
for G being _Graph holds
( G is c -vcolorable iff ex f being VColoring of G st
( f is proper & card (rng f) c= c ) );

theorem Th27: :: GLCOLO00:27

for G being _Graph
for c1, c2 being Cardinal st c1 c= c2 & G is c1 -vcolorable holds
G is c2 -vcolorable by XBOOLE_1:1;

:: might need Proof outside this article

theorem :: GLCOLO00:28

for G being _Graph st ex c being Cardinal st G is c -vcolorable holds
G is loopless ;

registration

let c be Cardinal;

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

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

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

coherence
for b₁ being _Graph st b₁ is loopless & b₁ is c -vertex holds
b₁ is c -vcolorable

proof end;

end;

registration

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

coherence
for b₁ being _Graph holds not b₁ is 0 -vcolorable by XBOOLE_1:3;

end;

theorem Th29: :: GLCOLO00:29

for G being _Graph st G is loopless holds
G is G .order() -vcolorable

proof end;

theorem Th30: :: GLCOLO00:30

for G being _Graph holds
( G is edgeless iff G is 1 -vcolorable )

proof end;

registration

let c be non zero Cardinal;

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

existence
ex b₁ being _Graph st b₁ is c -vcolorable

proof end;

end;

theorem Th31: :: GLCOLO00:31

for G being _Graph
for c being Cardinal
for H being Subgraph of G st G is c -vcolorable holds
H is c -vcolorable

proof end;

registration

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

coherence
for b₁ being _Graph st b₁ is edgeless holds
b₁ is 1 -vcolorable by Th30;

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

coherence
for b₁ being _Graph st b₁ is 1 -vcolorable holds
b₁ is edgeless by Th30;
let c be non zero Cardinal;
let G be c -vcolorable _Graph;

cluster -> c -vcolorable for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is c -vcolorable by Th31;

end;

theorem Th32: :: GLCOLO00:32

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

proof end;

Lm2: for E being set
for G1 being _Graph
for c being Cardinal
for G2 being reverseEdgeDirections of G1,E st G1 is c -vcolorable holds
G2 is c -vcolorable

proof end;

theorem Th33: :: GLCOLO00:33

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

proof end;

registration

let c be non zero Cardinal;
let G1 be c -vcolorable _Graph;
let E be set ;

cluster -> c -vcolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds b₁ is c -vcolorable by Th33;

end;

Lm3: for x being object
for X being set
for f being Function st x in rng f holds
rng (f +* (X --> x)) c= rng f

proof end;

theorem Th34: :: GLCOLO00:34

for V being set
for G2 being _Graph
for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -vcolorable iff G2 is c -vcolorable )

proof end;

registration

let c be non zero Cardinal;
let G2 be c -vcolorable _Graph;
let V be set ;

cluster -> c -vcolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds b₁ is c -vcolorable by Th34;

end;

theorem :: GLCOLO00:35

for G2 being _Graph
for c being Cardinal
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w st v,w are_adjacent holds
( G1 is c -vcolorable iff G2 is c -vcolorable )

proof end;

theorem Th36: :: GLCOLO00:36

for G2 being _Graph
for c being Cardinal
for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w & G2 is c -vcolorable holds
G1 is c +` 1 -vcolorable

proof end;

Lm4: for c being Cardinal
for G2 being non edgeless _Graph
for v being Vertex of G2
for 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 & G2 is c -vcolorable holds
G1 is c -vcolorable

proof end;

theorem Th37: :: GLCOLO00:37

for c being Cardinal
for G2 being non edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is c -vcolorable iff G2 is c -vcolorable )

proof end;

Lm5: for G2 being edgeless _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 is 2 -vcolorable

proof end;

theorem Th38: :: GLCOLO00:38

for G2 being edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 2 -vcolorable

proof end;

theorem Th39: :: GLCOLO00:39

for V being set
for G2 being _Graph
for c being Cardinal
for v being object
for G1 being addAdjVertexAll of G2,v,V st G2 is c -vcolorable holds
G1 is c +` 1 -vcolorable

proof end;

theorem Th40: :: GLCOLO00:40

for G1 being _Graph
for c being Cardinal
for G2 being removeParallelEdges of G1 holds
( G1 is c -vcolorable iff G2 is c -vcolorable )

proof end;

registration

let c be non zero Cardinal;
let G1 be c -vcolorable _Graph;

cluster -> c -vcolorable for removeParallelEdges of G1;

coherence
for b₁ being removeParallelEdges of G1 holds b₁ is c -vcolorable ;

end;

theorem Th41: :: GLCOLO00:41

for G1 being _Graph
for c being Cardinal
for G2 being removeDParallelEdges of G1 holds
( G1 is c -vcolorable iff G2 is c -vcolorable )

proof end;

registration

let c be non zero Cardinal;
let G1 be c -vcolorable _Graph;

cluster -> c -vcolorable for removeDParallelEdges of G1;

coherence
for b₁ being removeDParallelEdges of G1 holds b₁ is c -vcolorable ;

end;

theorem Th42: :: GLCOLO00:42

for G1, G2 being _Graph
for c being Cardinal
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -vcolorable holds
G1 is c -vcolorable

proof end;

theorem Th43: :: GLCOLO00:43

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

proof end;

registration

let c be non zero Cardinal;
let G be c -vcolorable _Graph;

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

coherence
for b₁ being _Graph st b₁ is G -isomorphic holds
b₁ is c -vcolorable

proof end;

end;

definition

let G be _Graph;

attr G is finite-vcolorable means :Def3: :: GLCOLO00:def 3
ex n being Nat st G is n -vcolorable ;

end;

:: deftheorem Def3 defines finite-vcolorable GLCOLO00:def 3 :
for G being _Graph holds
( G is finite-vcolorable iff ex n being Nat st G is n -vcolorable );

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] finite-vcolorable -> loopless for set ;

coherence
for b₁ being _Graph st b₁ is finite-vcolorable holds
b₁ is loopless ;

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

coherence
for b₁ being _Graph st b₁ is vertex-finite & b₁ is loopless holds
b₁ is finite-vcolorable

proof end;

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

coherence
for b₁ being _Graph st b₁ is edgeless holds
b₁ is finite-vcolorable by Th30;
let n be Nat;

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

coherence
for b₁ being _Graph st b₁ is n -vcolorable holds
b₁ is finite-vcolorable ;

end;

registration

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

existence
ex b₁ being _Graph st b₁ is finite-vcolorable

proof end;

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

existence
not for b₁ being _Graph holds b₁ is finite-vcolorable

proof end;

end;

registration

let G be finite-vcolorable _Graph;

cluster -> finite-vcolorable for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is finite-vcolorable

proof end;

end;

registration

let G be non finite-vcolorable _Graph;

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

coherence
for b₁ being Supergraph of G holds not b₁ is finite-vcolorable

proof end;

end;

theorem :: GLCOLO00:44

for G1, G2 being _Graph st G1 == G2 & G1 is finite-vcolorable holds
G2 is finite-vcolorable

proof end;

Lm6: for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E st G1 is finite-vcolorable holds
G2 is finite-vcolorable

proof end;

theorem Th45: :: GLCOLO00:45

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

registration

let G1 be finite-vcolorable _Graph;
let E be set ;

cluster -> finite-vcolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds b₁ is finite-vcolorable by Th45;

end;

registration

let G1 be non finite-vcolorable _Graph;
let E be set ;

cluster -> non finite-vcolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds not b₁ is finite-vcolorable by Th45;

end;

theorem Th46: :: GLCOLO00:46

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

registration

let G2 be finite-vcolorable _Graph;
let V be set ;

cluster -> finite-vcolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds b₁ is finite-vcolorable by Th46;

end;

theorem :: GLCOLO00:47

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

theorem Th48: :: GLCOLO00:48

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

registration

let G2 be finite-vcolorable _Graph;
let v, e, w be object ;

cluster -> finite-vcolorable for addAdjVertex of G2,v,e,w;

coherence
for b₁ being addAdjVertex of G2,v,e,w holds b₁ is finite-vcolorable by Th48;

end;

theorem Th49: :: GLCOLO00:49

for V being set
for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

registration

let G2 be finite-vcolorable _Graph;
let v be object ;
let V be set ;

cluster -> finite-vcolorable for addAdjVertexAll of G2,v,V;

coherence
for b₁ being addAdjVertexAll of G2,v,V holds b₁ is finite-vcolorable by Th49;

end;

theorem Th50: :: GLCOLO00:50

for G1 being _Graph
for G2 being removeParallelEdges of G1 holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

registration

let G1 be non finite-vcolorable _Graph;

cluster -> non finite-vcolorable for removeParallelEdges of G1;

coherence
for b₁ being removeParallelEdges of G1 holds not b₁ is finite-vcolorable by Th50;

end;

theorem Th51: :: GLCOLO00:51

for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )

proof end;

registration

let G1 be non finite-vcolorable _Graph;

cluster -> non finite-vcolorable for removeDParallelEdges of G1;

coherence
for b₁ being removeDParallelEdges of G1 holds not b₁ is finite-vcolorable by Th51;

end;

theorem Th52: :: GLCOLO00:52

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is finite-vcolorable holds
G1 is finite-vcolorable

proof end;

theorem Th53: :: GLCOLO00:53

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

proof end;

registration

let G be finite-vcolorable _Graph;

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

coherence
for b₁ being _Graph st b₁ is G -isomorphic holds
b₁ is finite-vcolorable

proof end;

end;

deffunc H₁( _Graph) -> set = { c where c is cardinal Subset of ($1 .order()) : $1 is c -vcolorable } ;

definition

let G be _Graph;

func G .vChromaticNum() -> Cardinal equals :: GLCOLO00:def 4
meet { c where c is cardinal Subset of (G .order()) : G is c -vcolorable } ;

coherence
meet { c where c is cardinal Subset of (G .order()) : G is c -vcolorable } is Cardinal

proof end;

end;

:: deftheorem defines .vChromaticNum() GLCOLO00:def 4 :
for G being _Graph holds G .vChromaticNum() = meet { c where c is cardinal Subset of (G .order()) : G is c -vcolorable } ;

theorem Th54: :: GLCOLO00:54

for G being _Graph st G is loopless holds
G is G .vChromaticNum() -vcolorable

proof end;

theorem Th55: :: GLCOLO00:55

for G being _Graph holds
( not G is loopless iff G .vChromaticNum() = 0 )

proof end;

registration

let G be loopless _Graph;

cluster G .vChromaticNum() -> non zero ;

coherence
not G .vChromaticNum() is zero by Th55;

end;

registration

let G be non loopless _Graph;

cluster G .vChromaticNum() -> zero ;

coherence
G .vChromaticNum() is zero by Th55;

end;

theorem Th56: :: GLCOLO00:56

for G being _Graph holds G .vChromaticNum() c= G .order()

proof end;

theorem Th57: :: GLCOLO00:57

for G being _Graph
for c being Cardinal st G is c -vcolorable holds
G .vChromaticNum() c= c

proof end;

theorem Th58: :: GLCOLO00:58

for G being _Graph
for c being Cardinal st G is c -vcolorable & ( for d being Cardinal st G is d -vcolorable holds
c c= d ) holds
G .vChromaticNum() = c

proof end;

registration

let G be finite-vcolorable _Graph;

cluster G .vChromaticNum() -> natural ;

coherence
G .vChromaticNum() is natural

proof end;

end;

definition

let G be finite-vcolorable _Graph;
:: original: .vChromaticNum()
redefine func G .vChromaticNum() -> Nat;
coherence
G .vChromaticNum() is Nat ;

end;

theorem Th59: :: GLCOLO00:59

for G being loopless _Graph holds 1 c= G .vChromaticNum()

proof end;

theorem Th60: :: GLCOLO00:60

for G being _Graph holds
( G is edgeless iff G .vChromaticNum() = 1 )

proof end;

theorem :: GLCOLO00:61

for G being loopless non edgeless _Graph holds 2 c= G .vChromaticNum()

proof end;

theorem :: GLCOLO00:62

for G being loopless _Graph st G is complete holds
G .vChromaticNum() = G .order()

proof end;

theorem Th63: :: GLCOLO00:63

for G being loopless _Graph
for H being Subgraph of G holds H .vChromaticNum() c= G .vChromaticNum()

proof end;

theorem :: GLCOLO00:64

for G1, G2 being _Graph st G1 == G2 holds
G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:65

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:66

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V holds G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:67

for G2 being non edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:68

for G2 being edgeless _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .vChromaticNum() = 2

proof end;

theorem :: GLCOLO00:69

for G2 being edgeless _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .vChromaticNum() = 2

proof end;

theorem Th70: :: GLCOLO00:70

for V being set
for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 .vChromaticNum() c= (G2 .vChromaticNum()) +` 1

proof end;

theorem :: GLCOLO00:71

for G2 being loopless _Graph
for v being object
for G1 being addAdjVertexAll of G2,v st not v in the_Vertices_of G2 holds
G1 .vChromaticNum() = (G2 .vChromaticNum()) +` 1

proof end;

theorem :: GLCOLO00:72

for G1 being _Graph
for G2 being removeParallelEdges of G1 holds G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:73

for G1 being _Graph
for G2 being removeDParallelEdges of G1 holds G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:74

for G1 being _Graph
for G2 being loopless _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .vChromaticNum() c= G2 .vChromaticNum()

proof end;

theorem Th75: :: GLCOLO00:75

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

theorem :: GLCOLO00:76

for G1 being _Graph
for G2 being b₁ -isomorphic _Graph holds G1 .vChromaticNum() = G2 .vChromaticNum()

proof end;

definition

let G be _Graph;
mode EColoring of G is ManySortedSet of the_Edges_of G;

end;

theorem Th77: :: GLCOLO00:77

for G being _Graph
for g being EColoring of G
for g9 being Function st rng g c= dom g9 holds
g9 * g is EColoring of G

proof end;

definition

let G be _Graph;
let g be EColoring of G;
let g9 be ManySortedSet of rng g;
:: original: *
redefine func g9 * g -> EColoring of G;
coherence
g * g9 is EColoring of G

proof end;

end;

theorem Th78: :: GLCOLO00:78

for G being _Graph
for g being EColoring of G
for H being Subgraph of G holds g | (the_Edges_of H) is EColoring of H

proof end;

theorem Th79: :: GLCOLO00:79

for G2 being _Graph
for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for g being EColoring of G2
for x being object st not e in the_Edges_of G2 holds
g +* (e .--> x) is EColoring of G1

proof end;

theorem :: GLCOLO00:80

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for g being EColoring of G2
for x being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
g +* (e .--> x) is EColoring of G1

proof end;

theorem :: GLCOLO00:81

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for g being EColoring of G2
for x being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
g +* (e .--> x) is EColoring of G1

proof end;

theorem Th82: :: GLCOLO00:82

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
for g2 being EColoring of G2
for h being Function st not v in the_Vertices_of G2 & dom h = G1 .edgesBetween (V,{v}) holds
g2 +* h is EColoring of G1

proof end;

theorem Th83: :: GLCOLO00:83

for G, G1 being _Graph
for g being EColoring of G
for F being PGraphMapping of G1,G st dom (F _E) = the_Edges_of G1 holds
g * (F _E) is EColoring of G1

proof end;

theorem Th84: :: GLCOLO00:84

for G, G1 being _Graph
for g being EColoring of G
for F being PGraphMapping of G1,G st F is total holds
g * (F _E) is EColoring of G1

proof end;

definition

let G be _Graph;
let g be EColoring of G;

attr g is proper means :Def5: :: GLCOLO00:def 5
for v being Vertex of G holds g | (v .edgesInOut()) is one-to-one ;

end;

:: deftheorem Def5 defines proper GLCOLO00:def 5 :
for G being _Graph
for g being EColoring of G holds
( g is proper iff for v being Vertex of G holds g | (v .edgesInOut()) is one-to-one );

theorem Th85: :: GLCOLO00:85

for G being _Graph
for g being EColoring of G holds
( g is proper iff for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2 )

proof end;

theorem Th86: :: GLCOLO00:86

for G being _Graph
for g being EColoring of G holds
( g is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2 )

proof end;

theorem Th87: :: GLCOLO00:87

for G being _Graph
for g being EColoring of G
for g9 being one-to-one Function
for g2 being EColoring of G st g2 = g9 * g & g is proper holds
g2 is proper

proof end;

theorem :: GLCOLO00:88

for G being _Graph
for g being EColoring of G
for g9 being one-to-one ManySortedSet of rng g st g is proper holds
g9 * g is proper by Th87;

registration

let G be _Graph;

cluster Relation-like the_Edges_of G -defined Function-like one-to-one total -> proper for set ;

coherence
for b₁ being EColoring of G st b₁ is one-to-one holds
b₁ is proper by FUNCT_1:52;

end;

registration

let G be _Graph;

cluster Relation-like the_Edges_of G -defined Function-like one-to-one total proper for set ;

existence
ex b₁ being EColoring of G st
( b₁ is one-to-one & b₁ is proper )

proof end;

end;

theorem Th89: :: GLCOLO00:89

for G being _Graph
for g being EColoring of G
for H being Subgraph of G
for g9 being EColoring of H st g9 = g | (the_Edges_of H) & g is proper holds
g9 is proper

proof end;

theorem Th90: :: GLCOLO00:90

for G1, G2 being _Graph
for g1 being EColoring of G1
for g2 being EColoring of G2 st G1 == G2 & g1 = g2 & g1 is proper holds
g2 is proper

proof end;

Lm7: for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for g1 being EColoring of G1
for g2 being EColoring of G2 st g1 = g2 & g1 is proper holds
g2 is proper

proof end;

theorem Th91: :: GLCOLO00:91

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for g1 being EColoring of G1
for g2 being EColoring of G2 st g1 = g2 holds
( g1 is proper iff g2 is proper )

proof end;

theorem Th92: :: GLCOLO00:92

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V
for g1 being EColoring of G1
for g2 being EColoring of G2 st g1 = g2 & g2 is proper holds
g1 is proper

proof end;

theorem Th93: :: GLCOLO00:93

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2 & g2 is proper holds
g1 is proper

proof end;

theorem Th94: :: GLCOLO00:94

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper

proof end;

theorem :: GLCOLO00:95

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper

proof end;

Lm8: for X being set
for x being object holds dom <:(X --> x),(id X):> = X

proof end;

Lm9: for X being set
for x, y being object st y in X holds
<:(X --> x),(id X):> . y = [x,y]

proof end;

Lm10: for X being set
for x being object holds rng <:(X --> x),(id X):> = [:{x},X:]

proof end;

Lm11: for X, Y being set holds Y misses rng <:(X --> Y),(id X):>

proof end;

theorem Th96: :: GLCOLO00:96

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
for g2 being EColoring of G2
for g1 being EColoring of G1
for X, E being set st E = G1 .edgesBetween (V,{v}) & rng g2 c= X & g1 = g2 +* <:(E --> X),(id E):> & not v in the_Vertices_of G2 & g2 is proper holds
g1 is proper

proof end;

theorem Th97: :: GLCOLO00:97

for G, G1 being _Graph
for g being EColoring of G
for F being PGraphMapping of G1,G
for g9 being EColoring of G1 st dom (F _E) = the_Edges_of G1 & F _E is one-to-one & g9 = g * (F _E) & g is proper holds
g9 is proper

proof end;

theorem Th98: :: GLCOLO00:98

for G, G1 being _Graph
for g being EColoring of G
for F being PGraphMapping of G1,G
for g9 being EColoring of G1 st F is weak_SG-embedding & g9 = g * (F _E) & g is proper holds
g9 is proper

proof end;

definition

let c be Cardinal;
let G be _Graph;

attr G is c -ecolorable means :Def6: :: GLCOLO00:def 6
ex g being proper EColoring of G st card (rng g) c= c;

end;

:: deftheorem Def6 defines -ecolorable GLCOLO00:def 6 :
for c being Cardinal
for G being _Graph holds
( G is c -ecolorable iff ex g being proper EColoring of G st card (rng g) c= c );

theorem Th99: :: GLCOLO00:99

for G being _Graph
for c1, c2 being Cardinal st c1 c= c2 & G is c1 -ecolorable holds
G is c2 -ecolorable by XBOOLE_1:1;

theorem Th100: :: GLCOLO00:100

for G being _Graph holds G is G .size() -ecolorable

proof end;

theorem Th101: :: GLCOLO00:101

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

proof end;

registration

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

coherence
for b₁ being _Graph st b₁ is edgeless holds
b₁ is 0 -ecolorable by Th101;

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

coherence
for b₁ being _Graph st b₁ is 0 -ecolorable holds
b₁ is edgeless by Th101;
let c be Cardinal;

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

coherence
for b₁ being _Graph st b₁ is c -edge holds
b₁ is c -ecolorable

proof end;

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

existence
ex b₁ being _Graph st b₁ is c -ecolorable

proof end;

end;

theorem Th102: :: GLCOLO00:102

for G being _Graph
for c being Cardinal
for H being Subgraph of G st G is c -ecolorable holds
H is c -ecolorable

proof end;

registration

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

cluster -> c -ecolorable for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is c -ecolorable by Th102;

end;

theorem Th103: :: GLCOLO00:103

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

proof end;

Lm12: for E being set
for G1 being _Graph
for c being Cardinal
for G2 being reverseEdgeDirections of G1,E st G1 is c -ecolorable holds
G2 is c -ecolorable

proof end;

theorem Th104: :: GLCOLO00:104

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

proof end;

registration

let c be Cardinal;
let G1 be c -ecolorable _Graph;
let E be set ;

cluster -> c -ecolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds b₁ is c -ecolorable by Th104;

end;

theorem Th105: :: GLCOLO00:105

for V being set
for G2 being _Graph
for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -ecolorable iff G2 is c -ecolorable )

proof end;

registration

let c be Cardinal;
let G2 be c -ecolorable _Graph;
let V be set ;

cluster -> c -ecolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds b₁ is c -ecolorable by Th105;

end;

theorem Th106: :: GLCOLO00:106

for c being Cardinal
for G2 being b₁ -ecolorable _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w holds G1 is c +` 1 -ecolorable

proof end;

theorem Th107: :: GLCOLO00:107

for c being Cardinal
for G2 being b₁ -ecolorable _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is c +` 1 -ecolorable

proof end;

Lm13: for G2 being edgeless _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 is 1 -ecolorable

proof end;

theorem :: GLCOLO00:108

for G2 being edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 1 -ecolorable

proof end;

registration

let c be Cardinal;
let G2 be c -ecolorable _Graph;
let v, e, w be object ;

cluster -> c +` 1 -ecolorable for addEdge of G2,v,e,w;

coherence
for b₁ being addEdge of G2,v,e,w holds b₁ is c +` 1 -ecolorable by Th106;

cluster -> c +` 1 -ecolorable for addAdjVertex of G2,v,e,w;

coherence
for b₁ being addAdjVertex of G2,v,e,w holds b₁ is c +` 1 -ecolorable by Th107;

end;

theorem Th109: :: GLCOLO00:109

for V being set
for c being Cardinal
for G2 being b₂ -ecolorable _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 is c +` (card V) -ecolorable

proof end;

registration

let c be Cardinal;
let G2 be c -ecolorable _Graph;
let v be object ;
let V be set ;

cluster -> c +` (card V) -ecolorable for addAdjVertexAll of G2,v,V;

coherence
for b₁ being addAdjVertexAll of G2,v,V holds b₁ is c +` (card V) -ecolorable by Th109;

end;

theorem Th110: :: GLCOLO00:110

for G1, G2 being _Graph
for c being Cardinal
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -ecolorable holds
G1 is c -ecolorable

proof end;

theorem Th111: :: GLCOLO00:111

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

proof end;

registration

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

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

coherence
for b₁ being _Graph st b₁ is G -isomorphic holds
b₁ is c -ecolorable

proof end;

end;

definition

let G be _Graph;

attr G is finite-ecolorable means :Def7: :: GLCOLO00:def 7
ex n being Nat st G is n -ecolorable ;

end;

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

registration

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

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

proof end;

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

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

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

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

proof end;

let n be Nat;

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

coherence
for b₁ being _Graph st b₁ is n -ecolorable holds
b₁ is finite-ecolorable ;

end;

registration

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

existence
ex b₁ being _Graph st b₁ is finite-ecolorable

proof end;

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

existence
not for b₁ being _Graph holds b₁ is finite-ecolorable

proof end;

end;

registration

let G be finite-ecolorable _Graph;

cluster -> finite-ecolorable for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is finite-ecolorable

proof end;

end;

theorem :: GLCOLO00:112

for G1, G2 being _Graph st G1 == G2 & G1 is finite-ecolorable holds
G2 is finite-ecolorable

proof end;

theorem Th113: :: GLCOLO00:113

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )

proof end;

registration

let G1 be finite-ecolorable _Graph;
let E be set ;

cluster -> finite-ecolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds b₁ is finite-ecolorable by Th113;

end;

registration

let G1 be non finite-ecolorable _Graph;
let E be set ;

cluster -> non finite-ecolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds not b₁ is finite-ecolorable by Th113;

end;

theorem Th114: :: GLCOLO00:114

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )

proof end;

registration

let G2 be finite-ecolorable _Graph;
let V be set ;

cluster -> finite-ecolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds b₁ is finite-ecolorable by Th114;

end;

registration

let G2 be non finite-ecolorable _Graph;
let V be set ;

cluster -> non finite-ecolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds not b₁ is finite-ecolorable by Th114;

end;

theorem Th115: :: GLCOLO00:115

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )

proof end;

registration

let G2 be finite-ecolorable _Graph;
let v, e, w be object ;

cluster -> finite-ecolorable for addEdge of G2,v,e,w;

coherence
for b₁ being addEdge of G2,v,e,w holds b₁ is finite-ecolorable by Th115;

end;

registration

let G2 be non finite-ecolorable _Graph;
let v, e, w be object ;

cluster -> non finite-ecolorable for addEdge of G2,v,e,w;

coherence
for b₁ being addEdge of G2,v,e,w holds not b₁ is finite-ecolorable by Th115;

end;

theorem Th116: :: GLCOLO00:116

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )

proof end;

registration

let G2 be finite-ecolorable _Graph;
let v, e, w be object ;

cluster -> finite-ecolorable for addAdjVertex of G2,v,e,w;

coherence
for b₁ being addAdjVertex of G2,v,e,w holds b₁ is finite-ecolorable by Th116;

end;

registration

let G2 be non finite-ecolorable _Graph;
let v, e, w be object ;

cluster -> non finite-ecolorable for addAdjVertex of G2,v,e,w;

coherence
for b₁ being addAdjVertex of G2,v,e,w holds not b₁ is finite-ecolorable by Th116;

end;

theorem Th117: :: GLCOLO00:117

for G2 being _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-ecolorable iff G2 is finite-ecolorable )

proof end;

registration

let G2 be finite-ecolorable _Graph;
let v be object ;
let V be finite set ;

cluster -> finite-ecolorable for addAdjVertexAll of G2,v,V;

coherence
for b₁ being addAdjVertexAll of G2,v,V holds b₁ is finite-ecolorable by Th117;

end;

theorem Th118: :: GLCOLO00:118

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is finite-ecolorable holds
G1 is finite-ecolorable

proof end;

theorem Th119: :: GLCOLO00:119

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

proof end;

registration

let G be finite-ecolorable _Graph;

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

coherence
for b₁ being _Graph st b₁ is G -isomorphic holds
b₁ is finite-ecolorable

proof end;

end;

deffunc H₂( _Graph) -> set = { c where c is cardinal Subset of ($1 .size()) : $1 is c -ecolorable } ;

definition

let G be _Graph;

func G .eChromaticNum() -> Cardinal equals :: GLCOLO00:def 8
meet { c where c is cardinal Subset of (G .size()) : G is c -ecolorable } ;

coherence
meet { c where c is cardinal Subset of (G .size()) : G is c -ecolorable } is Cardinal

proof end;

end;

:: deftheorem defines .eChromaticNum() GLCOLO00:def 8 :
for G being _Graph holds G .eChromaticNum() = meet { c where c is cardinal Subset of (G .size()) : G is c -ecolorable } ;

Lm14: for G being _Graph holds G is G .eChromaticNum() -ecolorable

proof end;

theorem Th120: :: GLCOLO00:120

for G being _Graph holds G .eChromaticNum() c= G .size()

proof end;

theorem Th121: :: GLCOLO00:121

for G being _Graph holds
( G is edgeless iff G .eChromaticNum() = 0 )

proof end;

registration

let G be edgeless _Graph;

cluster G .eChromaticNum() -> zero ;

coherence
G .eChromaticNum() is zero by Th121;

end;

registration

let G be non edgeless _Graph;

cluster G .eChromaticNum() -> non zero ;

coherence
not G .eChromaticNum() is zero by Th121;

end;

Lm15: for G being _Graph
for c being Cardinal st G is c -ecolorable holds
G .eChromaticNum() c= c

proof end;

theorem Th122: :: GLCOLO00:122

for G being _Graph
for c being Cardinal holds
( ( G is c -ecolorable & ( for d being Cardinal st G is d -ecolorable holds
c c= d ) ) iff G .eChromaticNum() = c )

proof end;

registration

let G be finite-ecolorable _Graph;

cluster G .eChromaticNum() -> natural ;

coherence
G .eChromaticNum() is natural

proof end;

end;

definition

let G be finite-ecolorable _Graph;
:: original: .eChromaticNum()
redefine func G .eChromaticNum() -> Nat;
coherence
G .eChromaticNum() is Nat ;

end;

theorem Th123: :: GLCOLO00:123

for G being loopless _Graph holds G .supDegree() c= G .eChromaticNum()

proof end;

theorem :: GLCOLO00:124

for G1, G2 being _Graph st G1 == G2 holds
G1 .eChromaticNum() = G2 .eChromaticNum()

proof end;

theorem Th125: :: GLCOLO00:125

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds G1 .eChromaticNum() = G2 .eChromaticNum()

proof end;

theorem :: GLCOLO00:126

for G being _Graph
for H being Subgraph of G holds H .eChromaticNum() c= G .eChromaticNum()

proof end;

theorem :: GLCOLO00:127

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V holds G1 .eChromaticNum() = G2 .eChromaticNum()

proof end;

theorem :: GLCOLO00:128

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w holds G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` 1

proof end;

theorem :: GLCOLO00:129

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` 1

proof end;

theorem Th130: :: GLCOLO00:130

for G2 being edgeless _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1

proof end;

theorem :: GLCOLO00:131

for G2 being edgeless _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1

proof end;

theorem :: GLCOLO00:132

for V being set
for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` (card V)

proof end;

theorem Th133: :: GLCOLO00:133

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .eChromaticNum() c= G2 .eChromaticNum()

proof end;

theorem Th134: :: GLCOLO00:134

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .eChromaticNum() = G2 .eChromaticNum()

proof end;

theorem :: GLCOLO00:135

for G1 being _Graph
for G2 being b₁ -isomorphic _Graph holds G1 .eChromaticNum() = G2 .eChromaticNum()

proof end;

theorem :: GLCOLO00:136

for G being _Graph st G is _trivial holds
G .eChromaticNum() = G .size()

proof end;

definition

let G be _Graph;

mode TColoring of G -> object means :Def9: :: GLCOLO00:def 9
ex f being VColoring of G ex g being EColoring of G st it = [f,g];

existence
ex b₁ being object ex f being VColoring of G ex g being EColoring of G st b₁ = [f,g]

proof end;

end;

:: deftheorem Def9 defines TColoring GLCOLO00:def 9 :
for G being _Graph
for b₂ being object holds
( b₂ is TColoring of G iff ex f being VColoring of G ex g being EColoring of G st b₂ = [f,g] );

registration

let G be _Graph;

cluster -> pair for TColoring of G;

coherence
for b₁ being TColoring of G holds b₁ is pair

proof end;

end;

notation

let G be _Graph;
let t be TColoring of G;
synonym t _V for G `1 ;
synonym t _E for G `2 ;

end;

registration

let G be _Graph;
let t be TColoring of G;

reduce [( _V),( _E)] to t;

reducibility
[( _V),( _E)] = t ;

end;

definition

let G be _Graph;
let t be TColoring of G;
:: original: _V
redefine func t _V -> VColoring of G;
coherence
_V is VColoring of G

proof end;

:: original: _E
redefine func t _E -> EColoring of G;
coherence
_E is EColoring of G

proof end;

end;

definition

let G be _Graph;
let f be VColoring of G;
let g be EColoring of G;
:: original: [
redefine func [f,g] -> TColoring of G;
coherence
[f,g] is TColoring of G by Def9;

end;

theorem Th137: :: GLCOLO00:137

for G being _Graph
for f being VColoring of G st G is edgeless holds
[f,{}] is TColoring of G

proof end;

theorem Th138: :: GLCOLO00:138

for G being _Graph
for t being TColoring of G
for H being Subgraph of G holds [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] is TColoring of H

proof end;

theorem Th139: :: GLCOLO00:139

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V
for t being TColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) holds
[((t _V) +* h),(t _E)] is TColoring of G1

proof end;

theorem Th140: :: GLCOLO00:140

for G2 being _Graph
for v, x being object
for G1 being addVertex of G2,v
for t being TColoring of G2 holds [((t _V) +* (v .--> x)),(t _E)] is TColoring of G1

proof end;

theorem Th141: :: GLCOLO00:141

for G2 being _Graph
for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for t being TColoring of G2
for y being object st not e in the_Edges_of G2 holds
[(t _V),((t _E) +* (e .--> y))] is TColoring of G1

proof end;

theorem Th142: :: GLCOLO00:142

for G2 being _Graph
for e being object
for v, w, u being Vertex of G2
for G1 being addEdge of G2,v,e,w
for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 holds
[((t _V) +* (u .--> x)),((t _E) +* (e .--> y))] is TColoring of G1

proof end;

theorem Th143: :: GLCOLO00:143

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 holds
[((t _V) +* (v .--> x)),((t _E) +* (e .--> y))] is TColoring of G1

proof end;

theorem Th144: :: GLCOLO00:144

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 holds
[((t _V) +* (w .--> x)),((t _E) +* (e .--> y))] is TColoring of G1

proof end;

theorem Th145: :: GLCOLO00:145

for G, G1 being _Graph
for t being TColoring of G
for F being PGraphMapping of G1,G st F is total holds
[((t _V) * (F _V)),((t _E) * (F _E))] is TColoring of G1

proof end;

definition

let G be _Graph;
let t be TColoring of G;

attr t is proper means :Def10: :: GLCOLO00:def 10
( t _V is proper & t _E is proper & ( for v being Vertex of G holds not (t _V) . v in (t _E) .: (v .edgesInOut()) ) );

end;

:: deftheorem Def10 defines proper GLCOLO00:def 10 :
for G being _Graph
for t being TColoring of G holds
( t is proper iff ( t _V is proper & t _E is proper & ( for v being Vertex of G holds not (t _V) . v in (t _E) .: (v .edgesInOut()) ) ) );

theorem Th146: :: GLCOLO00:146

for G being _Graph
for t being TColoring of G holds
( t is proper iff ( t _V is proper & t _E is proper & ( for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e ) ) )

proof end;

theorem Th147: :: GLCOLO00:147

for G being _Graph
for t being TColoring of G st t _V is proper & t _E is proper & rng (t _V) misses rng (t _E) holds
t is proper

proof end;

theorem Th148: :: GLCOLO00:148

for G being _Graph
for t being TColoring of G holds
( t is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) )

proof end;

theorem Th149: :: GLCOLO00:149

for G being _Graph
for f being VColoring of G
for g being EColoring of G st g is proper holds
ex g9 being proper EColoring of G st
( rng f misses rng g9 & card (rng g) = card (rng g9) )

proof end;

theorem Th150: :: GLCOLO00:150

for G being _Graph
for f being VColoring of G
for g being EColoring of G st f is proper holds
ex f9 being VColoring of G st
( f9 is proper & rng f9 misses rng g & card (rng f) = card (rng f9) )

proof end;

registration

let G be loopless _Graph;

cluster pair proper for TColoring of G;

existence
ex b₁ being TColoring of G st b₁ is proper

proof end;

end;

registration

let G be loopless _Graph;
let t be proper TColoring of G;

cluster _V -> proper for VColoring of G;

coherence
for b₁ being VColoring of G st b₁ = t _V holds
b₁ is proper by Def10;

cluster _E -> proper for EColoring of G;

coherence
for b₁ being EColoring of G st b₁ = t _E holds
b₁ is proper by Def10;

end;

theorem Th151: :: GLCOLO00:151

for G being _Graph
for t being TColoring of G
for H being Subgraph of G
for t9 being TColoring of H st t9 = [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] & t is proper holds
t9 is proper

proof end;

theorem Th152: :: GLCOLO00:152

for G1, G2 being _Graph
for t1 being TColoring of G1
for t2 being TColoring of G2 st G1 == G2 & t1 = t2 & t1 is proper holds
t2 is proper

proof end;

Lm16: for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for t1 being TColoring of G1
for t2 being TColoring of G2 st t1 = t2 & t1 is proper holds
t2 is proper

proof end;

theorem Th153: :: GLCOLO00:153

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for t1 being TColoring of G1
for t2 being TColoring of G2 st t1 = t2 holds
( t1 is proper iff t2 is proper )

proof end;

theorem Th154: :: GLCOLO00:154

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V
for t1 being TColoring of G1
for t2 being TColoring of G2
for h being Function st dom h = V \ (the_Vertices_of G2) & t1 _V = (t2 _V) +* h & t1 _E = t2 _E & t2 is proper holds
t1 is proper

proof end;

theorem Th155: :: GLCOLO00:155

for G2 being _Graph
for y, e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2 st not e in the_Edges_of G2 & v,w are_adjacent & t1 _V = t2 _V & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & t2 is proper holds
t1 is proper

proof end;

theorem Th156: :: GLCOLO00:156

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addEdge of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & v <> w & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper holds
t1 is proper

proof end;

theorem :: GLCOLO00:157

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addEdge of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & v <> w & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & {x,y} misses (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & t2 is proper holds
t1 is proper

proof end;

theorem Th158: :: GLCOLO00:158

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & t1 _V = (t2 _V) +* (v .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . w & t2 is proper holds
t1 is proper

proof end;

theorem :: GLCOLO00:159

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper

proof end;

theorem Th160: :: GLCOLO00:160

for G, G1 being _Graph
for t being TColoring of G
for F being PGraphMapping of G1,G
for t9 being TColoring of G1 st F is weak_SG-embedding & t9 = [((t _V) * (F _V)),((t _E) * (F _E))] & t is proper holds
t9 is proper

proof end;

definition

let c be Cardinal;
let G be _Graph;

attr G is c -tcolorable means :: GLCOLO00:def 11
ex t being TColoring of G st
( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= c );

end;

:: deftheorem defines -tcolorable GLCOLO00:def 11 :
for c being Cardinal
for G being _Graph holds
( G is c -tcolorable iff ex t being TColoring of G st
( t is proper & card ((rng (t _V)) \/ (rng (t _E))) c= c ) );

theorem Th161: :: GLCOLO00:161

for G being _Graph
for c1, c2 being Cardinal st c1 c= c2 & G is c1 -tcolorable holds
G is c2 -tcolorable by XBOOLE_1:1;

theorem Th162: :: GLCOLO00:162

for G being _Graph
for c being Cardinal st G is c -tcolorable holds
( G is c -vcolorable & G is c -ecolorable )

proof end;

theorem Th163: :: GLCOLO00:163

for G being _Graph
for c1, c2 being Cardinal st G is c1 -vcolorable & G is c2 -ecolorable holds
G is c1 +` c2 -tcolorable

proof end;

:: might need Proof outside this article

theorem :: GLCOLO00:164

for G being _Graph
for f being VColoring of G
for t being TColoring of G st G is edgeless & f is proper & t = [f,{}] holds
t is proper ;

theorem Th165: :: GLCOLO00:165

for G being _Graph holds
( G is edgeless iff G is 1 -tcolorable )

proof end;

registration

let c be non zero Cardinal;

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

existence
ex b₁ being _Graph st b₁ is c -tcolorable

proof end;

end;

theorem Th166: :: GLCOLO00:166

for G being _Graph
for c being Cardinal
for H being Subgraph of G st G is c -tcolorable holds
H is c -tcolorable

proof end;

registration

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

coherence
for b₁ being _Graph holds not b₁ is 0 -tcolorable by Th162;

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

coherence
for b₁ being _Graph st b₁ is edgeless holds
b₁ is 1 -tcolorable by Th165;

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

coherence
for b₁ being _Graph st b₁ is 1 -tcolorable holds
b₁ is edgeless by Th165;
let c be non zero Cardinal;
let G be c -tcolorable _Graph;

cluster -> c -tcolorable for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is c -tcolorable by Th166;

end;

registration

let c be Cardinal;

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

coherence
for b₁ being _Graph st b₁ is c -tcolorable holds
b₁ is loopless

proof end;

end;

theorem Th167: :: GLCOLO00:167

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

proof end;

Lm17: for E being set
for G1 being _Graph
for c being Cardinal
for G2 being reverseEdgeDirections of G1,E st G1 is c -tcolorable holds
G2 is c -tcolorable

proof end;

theorem Th168: :: GLCOLO00:168

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

proof end;

registration

let c be non zero Cardinal;
let G1 be c -tcolorable _Graph;
let E be set ;

cluster -> c -tcolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds b₁ is c -tcolorable by Th168;

end;

theorem Th169: :: GLCOLO00:169

for V being set
for G2 being _Graph
for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -tcolorable iff G2 is c -tcolorable )

proof end;

registration

let c be non zero Cardinal;
let G2 be c -tcolorable _Graph;
let V be set ;

cluster -> c -tcolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds b₁ is c -tcolorable by Th169;

end;

theorem :: GLCOLO00:170

for G2 being _Graph
for c being Cardinal
for e being object
for v, w being Vertex of G2
for G1 being addEdge of G2,v,e,w st v,w are_adjacent & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable

proof end;

theorem Th171: :: GLCOLO00:171

for G2 being _Graph
for c being Cardinal
for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w & G2 is c -tcolorable holds
G1 is c +` 2 -tcolorable

proof end;

Lm18: for c being Cardinal
for G2 being non edgeless _Graph
for v, e being object
for 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 & G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable

proof end;

theorem Th172: :: GLCOLO00:172

for c being Cardinal
for G2 being non edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w st G2 is c -tcolorable holds
G1 is c +` 1 -tcolorable

proof end;

Lm19: for f being Function
for x, y being object holds rng (f +* (x .--> y)) c= (rng f) \/ {y}

proof end;

theorem :: GLCOLO00:173

for G2 being _Graph
for c being Cardinal
for v being Vertex of G2
for 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 & v is endvertex & G2 is c -tcolorable holds
G1 is c -tcolorable

proof end;

theorem Th174: :: GLCOLO00:174

for G2 being edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 3 -tcolorable

proof end;

Lm20: for X, Y being set holds not Y in rng <:(X --> Y),(id X):>

proof end;

Lm21: for X, Y being set holds Y \/ {Y} misses rng <:(X --> Y),(id X):>

proof end;

theorem Th175: :: GLCOLO00:175

for V being set
for G2 being _Graph
for c being Cardinal
for v being object
for G1 being addAdjVertexAll of G2,v,V st G2 is c -tcolorable holds
G1 is (c +` 1) +` (card V) -tcolorable

proof end;

theorem Th176: :: GLCOLO00:176

for G1, G2 being _Graph
for c being Cardinal
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is c -tcolorable holds
G1 is c -tcolorable

proof end;

theorem Th177: :: GLCOLO00:177

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

proof end;

registration

let c be non zero Cardinal;
let G be c -tcolorable _Graph;

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

coherence
for b₁ being _Graph st b₁ is G -isomorphic holds
b₁ is c -tcolorable

proof end;

end;

definition

let G be _Graph;

attr G is finite-tcolorable means :Def12: :: GLCOLO00:def 12
ex n being Nat st G is n -tcolorable ;

end;

:: deftheorem Def12 defines finite-tcolorable GLCOLO00:def 12 :
for G being _Graph holds
( G is finite-tcolorable iff ex n being Nat st G is n -tcolorable );

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] finite-tcolorable -> loopless for set ;

coherence
for b₁ being _Graph st b₁ is finite-tcolorable holds
b₁ is loopless ;

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

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

proof end;

let n be Nat;

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

coherence
for b₁ being _Graph st b₁ is n -tcolorable holds
b₁ is finite-tcolorable ;

end;

registration

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

existence
ex b₁ being _Graph st b₁ is finite-tcolorable

proof end;

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

existence
not for b₁ being _Graph holds b₁ is finite-tcolorable

proof end;

end;

registration

let G be finite-tcolorable _Graph;

cluster -> finite-tcolorable for Subgraph of G;

coherence
for b₁ being Subgraph of G holds b₁ is finite-tcolorable

proof end;

end;

theorem :: GLCOLO00:178

for G1, G2 being _Graph st G1 == G2 & G1 is finite-tcolorable holds
G2 is finite-tcolorable

proof end;

theorem Th179: :: GLCOLO00:179

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )

proof end;

registration

let G1 be finite-tcolorable _Graph;
let E be set ;

cluster -> finite-tcolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds b₁ is finite-tcolorable by Th179;

end;

registration

let G1 be non finite-tcolorable _Graph;
let E be set ;

cluster -> non finite-tcolorable for reverseEdgeDirections of G1,E;

coherence
for b₁ being reverseEdgeDirections of G1,E holds not b₁ is finite-tcolorable by Th179;

end;

theorem Th180: :: GLCOLO00:180

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )

proof end;

registration

let G2 be finite-tcolorable _Graph;
let V be set ;

cluster -> finite-tcolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds b₁ is finite-tcolorable by Th180;

end;

registration

let G2 be non finite-tcolorable _Graph;
let V be set ;

cluster -> non finite-tcolorable for addVertices of G2,V;

coherence
for b₁ being addVertices of G2,V holds not b₁ is finite-tcolorable by Th180;

end;

theorem :: GLCOLO00:181

for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )

proof end;

theorem Th182: :: GLCOLO00:182

for G2 being _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )

proof end;

registration

let G2 be finite-tcolorable _Graph;
let v, e, w be object ;

cluster -> finite-tcolorable for addAdjVertex of G2,v,e,w;

coherence
for b₁ being addAdjVertex of G2,v,e,w holds b₁ is finite-tcolorable by Th182;

end;

registration

let G2 be non finite-tcolorable _Graph;
let v, e, w be object ;

cluster -> non finite-tcolorable for addAdjVertex of G2,v,e,w;

coherence
for b₁ being addAdjVertex of G2,v,e,w holds not b₁ is finite-tcolorable by Th182;

end;

theorem Th183: :: GLCOLO00:183

for G2 being _Graph
for v being object
for V being finite set
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )

proof end;

registration

let G2 be finite-tcolorable _Graph;
let v be object ;
let V be finite set ;

cluster -> finite-tcolorable for addAdjVertexAll of G2,v,V;

coherence
for b₁ being addAdjVertexAll of G2,v,V holds b₁ is finite-tcolorable by Th183;

end;

theorem Th184: :: GLCOLO00:184

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is finite-tcolorable holds
G1 is finite-tcolorable

proof end;

theorem Th185: :: GLCOLO00:185

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

proof end;

registration

let G be finite-tcolorable _Graph;

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

coherence
for b₁ being _Graph st b₁ is G -isomorphic holds
b₁ is finite-tcolorable

proof end;

end;

deffunc H₃( _Graph) -> set = { c where c is cardinal Subset of (($1 .order()) +` ($1 .size())) : $1 is c -tcolorable } ;

definition

let G be _Graph;

func G .tChromaticNum() -> Cardinal equals :: GLCOLO00:def 13
meet { c where c is cardinal Subset of ((G .order()) +` (G .size())) : G is c -tcolorable } ;

coherence
meet { c where c is cardinal Subset of ((G .order()) +` (G .size())) : G is c -tcolorable } is Cardinal

proof end;

end;

:: deftheorem defines .tChromaticNum() GLCOLO00:def 13 :
for G being _Graph holds G .tChromaticNum() = meet { c where c is cardinal Subset of ((G .order()) +` (G .size())) : G is c -tcolorable } ;

theorem Th186: :: GLCOLO00:186

for G being _Graph st G is loopless holds
G is G .tChromaticNum() -tcolorable

proof end;

theorem Th187: :: GLCOLO00:187

for G being _Graph holds
( not G is loopless iff G .tChromaticNum() = 0 )

proof end;

registration

let G be loopless _Graph;

cluster G .tChromaticNum() -> non zero ;

coherence
not G .tChromaticNum() is zero by Th187;

end;

registration

let G be non loopless _Graph;

cluster G .tChromaticNum() -> zero ;

coherence
G .tChromaticNum() is zero by Th187;

end;

theorem Th188: :: GLCOLO00:188

for G being _Graph holds G .tChromaticNum() c= (G .order()) +` (G .size())

proof end;

theorem Th189: :: GLCOLO00:189

for G being _Graph
for c being Cardinal st G is c -tcolorable holds
G .tChromaticNum() c= c

proof end;

theorem Th190: :: GLCOLO00:190

for G being _Graph
for c being Cardinal st G is c -tcolorable & ( for d being Cardinal st G is d -tcolorable holds
c c= d ) holds
G .tChromaticNum() = c

proof end;

registration

let G be finite-tcolorable _Graph;

cluster G .tChromaticNum() -> natural ;

coherence
G .tChromaticNum() is natural

proof end;

end;

definition

let G be finite-tcolorable _Graph;
:: original: .tChromaticNum()
redefine func G .tChromaticNum() -> Nat;
coherence
G .tChromaticNum() is Nat ;

end;

theorem :: GLCOLO00:191

for G being _Graph holds G .vChromaticNum() c= G .tChromaticNum()

proof end;

theorem Th192: :: GLCOLO00:192

for G being loopless _Graph holds G .eChromaticNum() c= G .tChromaticNum()

proof end;

theorem :: GLCOLO00:193

for G being _Graph holds G .tChromaticNum() c= (G .vChromaticNum()) +` (G .eChromaticNum())

proof end;

theorem :: GLCOLO00:194

for G being loopless _Graph holds (G .supDegree()) +` 1 c= G .tChromaticNum()

proof end;

theorem Th195: :: GLCOLO00:195

for G being _Graph holds
( G is edgeless iff G .tChromaticNum() = 1 )

proof end;

theorem Th196: :: GLCOLO00:196

for G being loopless non edgeless _Graph holds 3 c= G .tChromaticNum()

proof end;

theorem :: GLCOLO00:197

for G being loopless _Graph
for H being Subgraph of G holds H .tChromaticNum() c= G .tChromaticNum()

proof end;

theorem :: GLCOLO00:198

for G1, G2 being _Graph st G1 == G2 holds
G1 .tChromaticNum() = G2 .tChromaticNum()

proof end;

theorem :: GLCOLO00:199

for E being set
for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds G1 .tChromaticNum() = G2 .tChromaticNum()

proof end;

theorem :: GLCOLO00:200

for V being set
for G2 being _Graph
for G1 being addVertices of G2,V holds G1 .tChromaticNum() = G2 .tChromaticNum()

proof end;

theorem :: GLCOLO00:201

for G2 being non edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 .tChromaticNum() c= (G2 .tChromaticNum()) +` 1

proof end;

theorem :: GLCOLO00:202

for G2 being edgeless _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3

proof end;

theorem :: GLCOLO00:203

for G2 being edgeless _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .tChromaticNum() = 3

proof end;

theorem :: GLCOLO00:204

for V being set
for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 .tChromaticNum() c= ((G2 .tChromaticNum()) +` 1) +` (card V)

proof end;

theorem :: GLCOLO00:205

for G1 being _Graph
for G2 being loopless _Graph
for F being PGraphMapping of G1,G2 st F is weak_SG-embedding holds
G1 .tChromaticNum() c= G2 .tChromaticNum()

proof end;

theorem Th206: :: GLCOLO00:206

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .tChromaticNum() = G2 .tChromaticNum()

proof end;

theorem :: GLCOLO00:207

for G1 being _Graph
for G2 being b₁ -isomorphic _Graph holds G1 .tChromaticNum() = G2 .tChromaticNum()

proof end;