:: Introduction to Graph Colorings
:: by Sebastian Koch
::
:: Received July 23, 2022
:: Copyright (c) 2022-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, TARSKI, ARYTM_3,
CARD_1, XBOOLE_0, NAT_1, ARYTM_1, GLIB_000, PARTFUN1, FINSET_1, ZFMISC_1,
FUNCOP_1, GLIB_009, MOD_4, GLIB_006, GLIB_007, FUNCT_4, CARD_2, SCMYCIEL,
GLIB_010, SIMPLEX0, XCMPLX_0, MCART_1, SETFAM_1, FACIRC_1, ORDINAL1,
PBOOLE, CHORD, RING_3, REWRITE1, GLIB_013, GLCOLO00;
notations TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, WELLORD2, FUNCT_2, BINOP_1,
DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, PARTFUN2,
CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0,
NAT_D, CARD_2, FINSEQ_1, EQREL_1, FINSEQ_2, NEWTON, FUNCT_7, GLIB_000,
STRUCT_0, ALGSTR_0, ORDERS_2, GROUP_1, GROUP_2, GROUP_6, YELLOW_1,
SGRAPH1, MATRIX11, GLIB_001, CHORD, AOFA_I00, GLIB_006, GLIB_007,
GLIB_008, GLIB_009, GLIB_010, GLIB_013;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, NAT_D, BINOP_2, CARD_2,
FINSEQ_4, PBOOLE, ORDINAL3, WELLORD2, PARTFUN1, RELSET_1, GLIB_000,
STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, ALGSTR_0, GROUP_1, GLIB_001, ABIAN,
CARD_3, FINSEQ_1, GLIB_002, GLIB_003, SETFAM_1, EQREL_1, GROUP_2,
GROUP_6, GLIB_006, GLIB_007, PARTFUN2, CHORD, XTUPLE_0, MATRIX11,
GLIB_008, FUNCT_7, GLIB_009, GLIB_010, SQUARE_1, NEWTON, YELLOW_1,
VALUED_0, SGRAPH1, ORDERS_2, AOFA_I00, GLIB_013, FUNCT_3;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, GLIB_000, GLIB_002,
GLIB_003, INT_1, VALUED_0, CARD_1, FUNCT_2, PARTFUN1, RELSET_1, XTUPLE_0,
CARD_3, GROUP_1, STRUCT_0, GLIB_001, ABIAN, FINSEQ_4, GROUP_2, GLIB_006,
EQREL_1, GLIB_007, GLIB_008, CHORD, NECKLACE, FUNCT_7, GLIB_009,
MATRIX11, GLIB_010, SQUARE_1, NEWTON, SETFAM_1, FINSEQ_2, CARD_2,
GLIB_012, RAMSEY_1, MSAFREE5, GRFUNC_1, SGRAPH1, CARD_5, FUNCT_4,
WELLORD2, GLIBPRE0, YELLOW_1, ORDINAL7, RVSUM_4, AOFA_I00, GLIB_013,
FUNCT_3, GLIBPRE1;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
definitions GLIB_000;
equalities ORDINAL1, GLIB_000, GLIB_010;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ENUMSET1, RELAT_1, ZFMISC_1, SETFAM_1,
XREGULAR, XTUPLE_0, FUNCT_1, PARTFUN1, ORDINAL1, CARD_1, CARD_2,
XXREAL_0, NAT_1, FUNCOP_1, FUNCT_4, GLIB_000, CHORD, GLIB_006, GLIB_007,
GLIB_008, GLIB_009, GLIB_010, GLIBPRE0, GLIB_013, FUNCT_3, CARD_3,
XREAL_1, ORDINAL3, GLIBPRE1, FIELD_5;
begin :: Vertex Colorings
reserve E,V for set, G,G1,G2 for _Graph, c,c1,c2 for Cardinal, n for Nat;
definition
let G;
mode VColoring of G is ManySortedSet of the_Vertices_of G;
end;
registration
let G;
cluster -> non empty for VColoring of G;
coherence
proof
let f be VColoring of G;
dom f = the_Vertices_of G by PARTFUN1:def 2;
hence thesis;
end;
end;
reserve f for VColoring of G;
theorem Th1:
for f9 being Function st rng f c= dom f9 holds f9*f is VColoring of G
proof
let f9 be Function;
assume rng f c= dom f9;
then dom(f9*f) = dom f by RELAT_1:27
.= the_Vertices_of G by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
definition
let G, f; let f9 be ManySortedSet of rng f;
redefine func f9*f -> VColoring of G; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
rng f = dom f9 by PARTFUN1:def 2;
hence thesis by Th1;
end;
end;
:: might need Proof outside this article
theorem
for v being Vertex of G, x being object holds f+*(v.-->x) is VColoring of G;
theorem Th3:
for H being Subgraph of G holds f | the_Vertices_of H is VColoring of H
proof
let H be Subgraph of G;
set f9 = f | the_Vertices_of H;
the_Vertices_of H c= the_Vertices_of G;
then the_Vertices_of H c= dom f by PARTFUN1:def 2;
then dom f9 = the_Vertices_of H by RELAT_1:62;
hence thesis by PARTFUN1:def 2;
end;
theorem Th4:
for G1 being addVertices of G2, V, 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
let G1 be addVertices of G2, V;
let f be VColoring of G2, h being Function;
assume A1: dom h = V \ the_Vertices_of G2;
dom(f+*h) = dom f \/ dom h by FUNCT_4:def 1
.= the_Vertices_of G2 \/ (V \ the_Vertices_of G2) by A1, PARTFUN1:def 2
.= the_Vertices_of G2 \/ V by XBOOLE_1:39
.= the_Vertices_of G1 by GLIB_006:def 10;
hence f+*h is VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
end;
:: since the vertices do not change for addEdge, no extra theorem is provided
theorem
for v,e,x being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w, 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
let v,e,x be object, w be Vertex of G2, G1 be addAdjVertex of G2,v,e,w;
let f be VColoring of G2;
assume not e in the_Edges_of G2 & not v in the_Vertices_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by GLIB_006:def 12
.= dom f \/ {v} by PARTFUN1:def 2
.= dom f \/ dom{[v,x]} by RELAT_1:9
.= dom f \/ dom(v .--> x) by FUNCT_4:82
.= dom(f +* (v .--> x)) by FUNCT_4:def 1;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem Th6:
for v being Vertex of G2, e,w,x being object
for G1 being addAdjVertex of G2,v,e,w, 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
let v be Vertex of G2, e,w,x be object, G1 be addAdjVertex of G2,v,e,w;
let f be VColoring of G2;
assume not e in the_Edges_of G2 & not w in the_Vertices_of G2;
then the_Vertices_of G1 = the_Vertices_of G2 \/ {w} by GLIB_006:def 12
.= dom f \/ {w} by PARTFUN1:def 2
.= dom f \/ dom{[w,x]} by RELAT_1:9
.= dom f \/ dom(w .--> x) by FUNCT_4:82
.= dom(f +* (w .--> x)) by FUNCT_4:def 1;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem Th7:
for v,x being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2,v,V, f2 being VColoring of G2
st not v in the_Vertices_of G2 holds f2+*(v.-->x) is VColoring of G1
proof
let v,x be object, V be Subset of the_Vertices_of G2;
let G1 be addAdjVertexAll of G2,v,V, f2 be VColoring of G2;
set f1 = f2 +* (v .--> x);
assume not v in the_Vertices_of G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by GLIB_007:def 4;
dom f1 = dom f2 \/ dom(v .--> x) by FUNCT_4:def 1
.= dom f2 \/ dom{[v,x]} by FUNCT_4:82
.= dom f2 \/ {v} by RELAT_1:9
.= the_Vertices_of G1 by A1, PARTFUN1:def 2;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem Th8:
for F being PGraphMapping of G1,G st dom F_V = the_Vertices_of G1
holds f*F_V is VColoring of G1
proof
let F be PGraphMapping of G1,G;
assume A1: dom F_V = the_Vertices_of G1;
rng F_V c= the_Vertices_of G;
then rng F_V c= dom f by PARTFUN1:def 2;
then dom(f*(F_V)) = dom F_V by RELAT_1:27;
hence thesis by A1, PARTFUN1:def 2;
end;
theorem Th9:
for F being PGraphMapping of G1,G st F is total
holds f*F_V is VColoring of G1
proof
let F be PGraphMapping of G1, G;
assume F is total;
then dom F_V = the_Vertices_of G1 by GLIB_010:def 11;
hence thesis by Th8;
end;
definition
let G, f;
attr f is proper means
for v,w being Vertex of G st v,w are_adjacent holds f.v <> f.w;
end;
theorem Th10:
f is proper iff for e,v,w being object st e Joins v,w,G holds f.v <> f.w
proof
hereby
assume A1: f is proper;
let e,v,w be object;
assume A2: e Joins v,w,G;
then reconsider v0=v,w0=w as Vertex of G by GLIB_000:13;
v0,w0 are_adjacent by A2, CHORD:def 3;
hence f.v <> f.w by A1;
end;
assume A3: for e,v,w being object st e Joins v,w,G holds f.v <> f.w;
let v,w be Vertex of G;
assume v,w are_adjacent;
then consider e being object such that
A4: e Joins v,w,G by CHORD:def 3;
thus thesis by A3, A4;
end;
theorem Th11:
f is proper iff for e,v,w being object st e DJoins v,w,G holds f.v <> f.w
proof
hereby
assume A1: f is proper;
let e,v,w be object;
assume e DJoins v,w,G;
then e Joins v,w,G by GLIB_000:16;
hence f.v <> f.w by A1, Th10;
end;
assume A2: for e,v,w being object st e DJoins v,w,G holds f.v <> f.w;
now
let e,v,w be object;
assume e Joins v,w,G;
then per cases by GLIB_000:16;
suppose e DJoins v,w,G;
hence f.v <> f.w by A2;
end;
suppose e DJoins w,v,G;
hence f.v <> f.w by A2;
end;
end;
hence thesis by Th10;
end;
theorem Th12:
for f9 being one-to-one Function, f2 being VColoring of G
st f2 = f9*f & f is proper & rng f c= dom f9 holds f2 is proper
proof
let f9 be one-to-one Function, f2 be VColoring of G;
assume A1: f2 = f9*f & f is proper & rng f c= dom f9;
now
let e,v,w be object;
assume A2: e Joins v,w,G;
then v in the_Vertices_of G & w in the_Vertices_of G by GLIB_000:13;
then A3: v in dom f & w in dom f by PARTFUN1:def 2;
then A4: f2.v = f9.(f.v) & f2.w = f9.(f.w) by A1, FUNCT_1:13;
A5: f.v in rng f & f.w in rng f by A3, FUNCT_1:3;
f.v <> f.w by A1, A2, Th10;
hence f2.v <> f2.w by A1, A4, A5, FUNCT_1:def 4;
end;
hence thesis by Th10;
end;
theorem
for f9 being one-to-one ManySortedSet of rng f
holds f is proper implies f9*f is proper
proof
let f9 be one-to-one ManySortedSet of rng f;
rng f c= dom f9 by PARTFUN1:def 2;
hence thesis by Th12;
end;
theorem Th14:
(ex f st f is proper) implies G is loopless
proof
given f such that
A1: f is proper;
now
given v,e being object such that
A2: e Joins v,v,G;
f.v = f.v;
hence contradiction by A1, A2, Th10;
end;
hence thesis by GLIB_000:18;
end;
registration
let G be non loopless _Graph;
cluster -> non proper for VColoring of G;
coherence by Th14;
end;
registration
let G be loopless _Graph;
cluster one-to-one -> proper for VColoring of G;
coherence
proof
let f be VColoring of G;
assume A1: f is one-to-one;
now
let e,v,w be object;
assume A2: e Joins v,w,G;
then A3: v <> w by GLIB_000:18;
v in the_Vertices_of G & w in the_Vertices_of G by A2, GLIB_000:13;
then v in dom f & w in dom f by PARTFUN1:def 2;
hence f.v <> f.w by A1, A3, FUNCT_1:def 4;
end;
hence thesis by Th10;
end;
end;
registration
let G be loopless _Graph;
cluster one-to-one proper for VColoring of G;
existence
proof
take id the_Vertices_of G;
thus thesis;
end;
end;
theorem Th15:
for H being Subgraph of G, f9 being VColoring of H
st f9 = f | the_Vertices_of H & f is proper holds f9 is proper
proof
let H be Subgraph of G, f9 be VColoring of H;
assume A1: f9 = f | the_Vertices_of H & f is proper;
now
let e,v,w be object;
assume A2: e Joins v,w,H;
v is set & w is set by TARSKI:1;
then A3: f.v <> f.w by A1, A2, Th10, GLIB_000:72;
v in the_Vertices_of H & w in the_Vertices_of H by A2, GLIB_000:13;
then v in dom f9 & w in dom f9 by PARTFUN1:def 2;
then f.v = f9.v & f.w = f9.w by A1, FUNCT_1:47;
hence f9.v <> f9.w by A3;
end;
hence thesis by Th10;
end;
theorem Th16:
for f1 being VColoring of G1, f2 being VColoring of G2
st G1 == G2 & f1 = f2 & f1 is proper holds f2 is proper
proof
let f1 be VColoring of G1, f2 be VColoring of G2;
assume A1: G1 == G2 & f1 = f2 & f1 is proper;
now
let e,v,w be object;
assume e Joins v,w,G2;
then e Joins v,w,G1 by A1, GLIB_000:88;
hence f2.v <> f2.w by A1, Th10;
end;
hence thesis by Th10;
end;
theorem Th17:
for f1 being VColoring of G1, f2 being VColoring of G2
for v being Vertex of G1, x being object
st G1 == G2 & f2 = f1 +* (v .--> x) & not x in rng f1 & f1 is proper
holds f2 is proper
proof
let f1 be VColoring of G1, f2 be VColoring of G2;
let v be Vertex of G1, x be object;
assume A1: G1 == G2 & f2 = f1 +* (v .--> x) & not x in rng f1 & f1 is proper;
now
let e,u,w be object;
assume e Joins u,w,G2;
then A2: e Joins u,w,G1 by A1, GLIB_000:88;
u in the_Vertices_of G1 & w in the_Vertices_of G1 by A2, GLIB_000:13;
then u in dom f1 & w in dom f1 by PARTFUN1:def 2;
then A3: f1.u in rng f1 & f1.w in rng f1 by FUNCT_1:3;
per cases;
suppose u <> v & w <> v;
then f2.u = f1.u & f2.w = f1.w by A1, FUNCT_4:83;
hence f2.u <> f2.w by A1, A2, Th10;
end;
suppose u = v & w <> v;
then f2.u = x & f2.w = f1.w by A1, FUNCT_4:83, FUNCT_4:113;
hence f2.u <> f2.w by A1, A3;
end;
suppose u <> v & w = v;
then f2.u = f1.u & f2.w = x by A1, FUNCT_4:83, FUNCT_4:113;
hence f2.u <> f2.w by A1, A3;
end;
suppose u = v & w = v;
then G1 is non loopless by A2, GLIB_000:18;
hence f2.u <> f2.w by A1; :: by contradiction
end;
end;
hence thesis by Th10;
end;
Lm1:
for G2 being reverseEdgeDirections of G1, E
for f1 being VColoring of G1, f2 being VColoring of G2
st f1 = f2 & f1 is proper holds f2 is proper
proof
let G2 be reverseEdgeDirections of G1, E;
let f1 be VColoring of G1, f2 be VColoring of G2;
assume f1 = f2 & f1 is proper;
then for e,v,w being object st e Joins v,w,G2 holds f2.v <> f2.w
by Th10, GLIB_007:9;
hence thesis by Th10;
end;
theorem Th18:
for G2 being reverseEdgeDirections of G1, E
for f1 being VColoring of G1, f2 being VColoring of G2
st f1 = f2 holds f1 is proper iff f2 is proper
proof
let G2 be reverseEdgeDirections of G1, E;
let f1 be VColoring of G1, f2 be VColoring of G2;
assume A1: f1 = f2;
hence f1 is proper implies f2 is proper by Lm1;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by A1, Lm1;
end;
theorem Th19:
for G1 being addVertices of G2, V
for f1 being VColoring of G1, f2 being VColoring of G2, h being Function
st dom h = V \ the_Vertices_of G2 & f1 = f2 +* h & f2 is proper
holds f1 is proper
proof
let G1 be addVertices of G2, V;
let f1 be VColoring of G1, f2 be VColoring of G2, h being Function;
assume A1: dom h = V \ the_Vertices_of G2 & f1 = f2 +* h & f2 is proper;
now
let e,v,w be object;
assume e Joins v,w,G1;
then A2: e Joins v,w,G2 by GLIB_006:87;
v in the_Vertices_of G2 & w in the_Vertices_of G2 by A2, GLIB_000:13;
then not v in dom h & not w in dom h by A1, XBOOLE_0:def 5;
then f1.v = f2.v & f1.w = f2.w by A1, FUNCT_4:11;
hence f1.v <> f1.w by A1, A2, Th10;
end;
hence f1 is proper by Th10;
end;
theorem Th20:
for v,w being Vertex of G2, e being object, G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1, f2 being VColoring of G2
st f1 = f2 & v,w are_adjacent & f2 is proper holds f1 is proper
proof
let v,w be Vertex of G2, e be object, G1 be addEdge of G2,v,e,w;
let f1 be VColoring of G1, f2 be VColoring of G2;
assume A1: f1 = f2 & v,w are_adjacent & f2 is proper;
per cases;
suppose A2: not e in the_Edges_of G2;
now
let e9,v9,w9 be object;
assume A3: e9 Joins v9,w9,G1;
then per cases by GLIB_006:72;
suppose e9 Joins v9,w9,G2;
hence f1.v9 <> f1.w9 by A1, Th10;
end;
suppose not e9 in the_Edges_of G2;
then A4: (v9 = v & w9 = w)or(v9 = w & w9 = v) by A2, A3, GLIB_006:107;
consider e1 being object such that
A5: e1 Joins v,w,G2 by A1, CHORD:def 3;
e1 Joins v9,w9,G2 by A4, A5, GLIB_000:14;
hence f1.v9 <> f1.w9 by A1, Th10;
end;
end;
hence thesis by Th10;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by A1, Th16;
end;
end;
theorem Th21:
for v being Vertex of G2, e,w being object, G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1, f2 being VColoring of G2, x being object
st f1=f2+*(v.-->x) & v<>w & not x in rng f2 & f2 is proper holds f1 is proper
proof
let v being Vertex of G2, e,w be object, G1 be addEdge of G2,v,e,w;
let f1 be VColoring of G1, f2 be VColoring of G2, x be object;
assume A1: f1 = f2 +* (v.-->x) & v <> w & not x in rng f2 & f2 is proper;
per cases;
suppose A2: not e in the_Edges_of G2 & v in the_Vertices_of G2 &
w in the_Vertices_of G2;
set h = v .--> x;
now
let e9,v9,w9 be object;
assume A3: e9 Joins v9,w9,G1;
per cases;
suppose e9 in the_Edges_of G2;
then A4: e9 Joins v9,w9,G2 by A3, GLIB_006:72;
v9 in the_Vertices_of G2 & w9 in the_Vertices_of G2 by A4, GLIB_000:13;
then v9 in dom f2 & w9 in dom f2 by PARTFUN1:def 2;
then A5: f2.v9 in rng f2 & f2.w9 in rng f2 by FUNCT_1:3;
per cases;
suppose v9 <> v & w9 <> v;
then f1.v9 = f2.v9 & f1.w9 = f2.w9 by A1, FUNCT_4:83;
hence f1.v9 <> f1.w9 by A1, A4, Th10;
end;
suppose v9 = v & w9 <> v;
then f1.v9 = x & f1.w9 = f2.w9 by A1, FUNCT_4:83, FUNCT_4:113;
hence f1.v9 <> f1.w9 by A1, A5;
end;
suppose v9 <> v & w9 = v;
then f1.v9 = f2.v9 & f1.w9 = x by A1, FUNCT_4:83, FUNCT_4:113;
hence f1.v9 <> f1.w9 by A1, A5;
end;
suppose v9 = v & w9 = v;
then G2 is non loopless by A4, GLIB_000:18;
hence f1.v9 <> f1.w9 by A1; :: by contradiction
end;
end;
suppose A6: not e9 in the_Edges_of G2;
w in dom f2 by A2, PARTFUN1:def 2;
then A7: f2.w in rng f2 by FUNCT_1:3;
per cases by A2, A3, A6, GLIB_006:107;
suppose A8: v9 = w & w9 = v;
then f1.v9 = f2.v9 & f1.w9 = x by A1, FUNCT_4:83, FUNCT_4:113;
hence f1.v9 <> f1.w9 by A1, A8, A7;
end;
suppose A9: v9 = v & w9 = w;
then f1.v9 = x & f1.w9 = f2.w9 by A1, FUNCT_4:83, FUNCT_4:113;
hence f1.v9 <> f1.w9 by A1, A9, A7;
end;
end;
end;
hence f1 is proper by Th10;
end;
suppose not(not e in the_Edges_of G2 & v in the_Vertices_of G2 &
w in the_Vertices_of G2);
then G1 == G2 by GLIB_006:def 11;
hence thesis by A1, Th17;
end;
end;
theorem Th22:
for v,e being object, w being Vertex of G2, G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1, f2 being VColoring of G2, x being object
st f1=f2+*(w.-->x) & v<>w & not x in rng f2 & f2 is proper holds f1 is proper
proof
let v,e be object, w being Vertex of G2, G1 be addEdge of G2,v,e,w;
let f1 be VColoring of G1, f2 be VColoring of G2, x be object;
assume A1: f1 = f2 +* (w.-->x) & v <> w & not x in rng f2 & f2 is proper;
per cases;
suppose A2: not e in the_Edges_of G2;
set G3 = the reverseEdgeDirections of G1, {e};
A3: G3 is addEdge of G2,w,e,v by A2, GLIBPRE1:65;
the_Vertices_of G1 = the_Vertices_of G3 by GLIB_007:4;
then reconsider f3 = f1 as VColoring of G3;
f3 is proper by A1, A3, Th21;
hence thesis by Th18;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
hence thesis by A1, Th17;
end;
end;
theorem Th23:
for v,e,w being object, G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1, f2 being VColoring of G2, x being object
st not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) & x <> f2.w
holds f2 is proper implies f1 is proper
proof
let v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
let f1 be VColoring of G1, f2 be VColoring of G2, x be object;
assume that A1: not v in the_Vertices_of G2 & f1 = f2 +* (v .--> x) and
A2: x <> f2.w & f2 is proper;
dom(v .--> x) = dom{[v,x]} by FUNCT_4:82
.= {v} by RELAT_1:9;
then v in dom(v .--> x) by TARSKI:def 1;
then v in dom f2 \/ dom(v .--> x) by XBOOLE_0:def 3;
then v in dom f1 by A1, FUNCT_4:def 1;
then A3: v in the_Vertices_of G1;
A4: not e in the_Edges_of G2 & w in the_Vertices_of G2
proof
assume e in the_Edges_of G2 or not w in the_Vertices_of G2;
then G1 == G2 by A1, GLIB_006:def 12;
hence contradiction by A1, A3, GLIB_000:def 34;
end;
now
let e9,v9,w9 be object;
assume A5: e9 DJoins v9,w9,G1;
then per cases by GLIB_006:71;
suppose A6: e9 DJoins v9,w9,G2;
then e9 Joins v9,w9,G2 by GLIB_000:16;
then v9 <> v & w9 <> v by A1, GLIB_000:13;
then f1.v9 = f2.v9 & f1.w9 = f2.w9 by A1, FUNCT_4:83;
hence f1.v9 <> f1.w9 by A2, A6, Th11;
end;
suppose A7: not e9 in the_Edges_of G2;
A8: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, A4, GLIB_006:def 12;
e9 in the_Edges_of G1 by A5, GLIB_000:def 14;
then e9 in {e} by A7, A8, XBOOLE_0:def 3;
then A9: e9 = e by TARSKI:def 1;
e DJoins v,w,G1 by A1, A4, GLIB_006:132;
then A10: v = v9 & w = w9 by A5, A9, GLIB_000:125;
f1.v = x & f1.w = f2.w by A1, A4, FUNCT_4:83, FUNCT_4:113;
hence f1.v9 <> f1.w9 by A2, A10;
end;
end;
hence thesis by Th11;
end;
theorem Th24:
for v,e,w being object, G1 being addAdjVertex of G2,v,e,w
for f1 being VColoring of G1, f2 being VColoring of G2, x being object
st not w in the_Vertices_of G2 & f1 = f2 +* (w .--> x) & x <> f2.v
holds f2 is proper implies f1 is proper
proof
let v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
let f1 be VColoring of G1, f2 be VColoring of G2, x be object;
assume that A1: not w in the_Vertices_of G2 & f1 = f2 +* (w .--> x) and
A2: x <> f2.v & f2 is proper;
set G3 = the reverseEdgeDirections of G1, {e};
per cases;
suppose not e in the_Edges_of G2;
then A3: G3 is addAdjVertex of G2,w,e,v by GLIBPRE1:66;
the_Vertices_of G1 = the_Vertices_of G3 by GLIB_007:4;
then reconsider f3 = f1 as VColoring of G3;
f3 is proper by A1, A2, A3, Th23;
hence thesis by Th18;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 12;
then the_Vertices_of G2 = the_Vertices_of G1 by GLIB_000:def 34
.= dom f1 by PARTFUN1:def 2
.= dom f2 \/ dom(w .--> x) by A1, FUNCT_4:def 1
.= dom f2 \/ dom{[w,x]} by FUNCT_4:82
.= dom f2 \/ {w} by RELAT_1:9
.= the_Vertices_of G2 \/ {w} by PARTFUN1:def 2;
hence thesis by A1, ZFMISC_1:39; :: by contradiction
end;
end;
theorem Th25:
for v,x being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2,v,V
for f1 being VColoring of G1, f2 being VColoring of G2
st not v in the_Vertices_of G2 & f1=f2+*(v.-->x) & not x in rng f2
holds f2 is proper implies f1 is proper
proof
let v,x be object, V be Subset of the_Vertices_of G2;
let G1 be addAdjVertexAll of G2,v,V;
let f1 be VColoring of G1, f2 be VColoring of G2;
set h = v .--> x;
assume A1: not v in the_Vertices_of G2 & f1=f2 +* h & not x in rng f2;
then A2: the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by GLIB_007:def 4;
assume A3: f2 is proper;
now
let e,u,w be object;
assume A4: e Joins u,w,G1;
per cases;
suppose A5: u <> v & w <> v;
then A6: e Joins u,w,G2 by A1, A4, GLIB_007:49;
f1.u = f2.u & f1.w = f2.w by A1, A5, FUNCT_4:83;
hence f1.u <> f1.w by A3, A6, Th10;
end;
suppose A7: u = v;
then A8: w <> v by A1, A4, GLIB_007:def 4;
then A9: f1.u = x & f1.w = f2.w by A1, A7, FUNCT_4:83, FUNCT_4:113;
w in the_Vertices_of G1 by A4, GLIB_000:13;
then w in the_Vertices_of G2 by A2, A8, ZFMISC_1:136;
then w in dom f2 by PARTFUN1:def 2;
hence f1.u <> f1.w by A1, A9, FUNCT_1:3;
end;
suppose A10: w = v;
then A11: u <> v by A1, A4, GLIB_007:def 4;
then A12: f1.w = x & f1.u = f2.u by A1, A10, FUNCT_4:83, FUNCT_4:113;
u in the_Vertices_of G1 by A4, GLIB_000:13;
then u in the_Vertices_of G2 by A2, A11, ZFMISC_1:136;
then u in dom f2 by PARTFUN1:def 2;
hence f1.u <> f1.w by A1, A12, FUNCT_1:3;
end;
end;
hence thesis by Th10;
end;
theorem Th26:
for F being PGraphMapping of G1,G, f9 being VColoring of G1
st F is total & f9 = f*F_V & f is proper holds f9 is proper
proof
let F be PGraphMapping of G1, G, f9 be VColoring of G1;
assume A1: F is total & f9 = f*(F_V) & f is proper;
now
let e,v,w be object;
assume A2: e Joins v,w,G1;
then e in the_Edges_of G1 & v in the_Vertices_of G1 &
w in the_Vertices_of G1 by GLIB_000:def 13, GLIB_000:13;
then A3: e in dom F_E & v in dom F_V & w in dom F_V by A1, GLIB_010:def 11;
then F_E.e Joins F_V.v,F_V.w,G by A2, GLIB_010:4;
then f.(F_V.v) <> f.(F_V.w) by A1, Th10;
then (f*F_V).v <> f.(F_V.w) by A3, FUNCT_1:13;
hence f9.v <> f9.w by A1, A3, FUNCT_1:13;
end;
hence thesis by Th10;
end;
definition
let c, G;
attr G is c-vcolorable means
ex f being VColoring of G st f is proper & card rng f c= c;
end;
theorem Th27:
c1 c= c2 & G is c1-vcolorable implies G is c2-vcolorable by XBOOLE_1:1;
:: might need Proof outside this article
theorem
(ex c st G is c-vcolorable) implies G is loopless;
registration
let c;
cluster c-vcolorable -> loopless for _Graph;
coherence;
cluster loopless c-vertex -> c-vcolorable for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is loopless c-vertex;
reconsider f = id the_Vertices_of G as VColoring of G;
card rng f = G.order()
.= c by A1, GLIB_013:def 3;
hence thesis by A1;
end;
end;
registration
cluster -> non 0-vcolorable for _Graph;
coherence by XBOOLE_1:3;
end;
theorem Th29:
G is loopless implies G is G.order()-vcolorable
proof
assume A1: G is loopless;
reconsider f = id the_Vertices_of G as VColoring of G;
card rng f = G.order();
hence G is G.order()-vcolorable by A1;
end;
theorem Th30:
G is edgeless iff G is 1-vcolorable
proof
hereby
set x = the object;
set f = the_Vertices_of G --> x;
reconsider f as VColoring of G;
assume G is edgeless;
then for e,v,w being object st e Joins v,w,G holds f.v<>f.w by GLIB_008:50;
then A1: f is proper by Th10;
card rng f c= card {x} by CARD_1:11, FUNCOP_1:13;
then card rng f c= 1 by CARD_1:30;
hence G is 1-vcolorable by A1;
end;
assume G is 1-vcolorable;
then consider f such that
A2: f is proper & card rng f c= 1;
0 in card rng f by ORDINAL1:14;
then 1 c= card rng f by ZFMISC_1:31, CARD_1:49;
then card rng f = 1 by A2, XBOOLE_0:def 10
.= card {the object} by CARD_1:30;
then consider x being object such that
A3: rng f = {x} by CARD_1:29;
A4: f = dom f --> x by A3, FUNCOP_1:9;
now
set e = the Element of the_Edges_of G;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
assume the_Edges_of G <> {};
then A5: e Joins v,w,G by GLIB_000:def 13;
then v in the_Vertices_of G & w in the_Vertices_of G by GLIB_000:13;
then v in dom f & w in dom f by PARTFUN1:def 2;
then f.v = x & f.w = x by A4, FUNCOP_1:7;
hence contradiction by A2, A5, Th10;
end;
hence thesis;
end;
registration
let c be non zero Cardinal;
cluster c-vcolorable for _Graph;
existence
proof
take the edgeless _Graph;
1 c= c
proof
assume not 1 c= c;
then c in {0} by CARD_1:49, ORDINAL1:16;
hence contradiction by TARSKI:def 1;
end;
hence thesis by Th27, Th30;
end;
end;
theorem Th31:
for H being Subgraph of G holds G is c-vcolorable implies H is c-vcolorable
proof
let H be Subgraph of G;
assume G is c-vcolorable;
then consider f being VColoring of G such that
A1: f is proper & card rng f c= c;
reconsider f9 = f | the_Vertices_of H as VColoring of H by Th3;
card rng f9 c= card rng f by RELAT_1:70, CARD_1:11;
then card rng f9 c= c by A1, XBOOLE_1:1;
hence thesis by A1, Th15;
end;
registration
cluster edgeless -> 1-vcolorable for _Graph;
coherence by Th30;
cluster 1-vcolorable -> edgeless for _Graph;
coherence by Th30;
let c be non zero Cardinal;
let G be c-vcolorable _Graph;
cluster -> c-vcolorable for Subgraph of G;
coherence by Th31;
end;
theorem Th32:
G1 == G2 & G1 is c-vcolorable implies G2 is c-vcolorable
proof
assume A1: G1 == G2 & G1 is c-vcolorable;
then consider f1 being VColoring of G1 such that
A2: f1 is proper & card rng f1 c= c;
the_Vertices_of G1 = the_Vertices_of G2 by A1, GLIB_000:def 34;
then reconsider f2 = f1 as VColoring of G2;
f2 is proper by A1, A2, Th16;
hence thesis by A2;
end;
Lm2:
for G2 being reverseEdgeDirections of G1, E
holds G1 is c-vcolorable implies G2 is c-vcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
assume G1 is c-vcolorable;
then consider f1 being VColoring of G1 such that
A1: f1 is proper & card rng f1 c= c;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_007:4;
then reconsider f2 = f1 as VColoring of G2;
f2 is proper by A1, Lm1;
hence thesis by A1;
end;
theorem Th33:
for G2 being reverseEdgeDirections of G1, E
holds G1 is c-vcolorable iff G2 is c-vcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
thus G1 is c-vcolorable implies G2 is c-vcolorable by Lm2;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by Lm2;
end;
registration
let c be non zero Cardinal;
let G1 be c-vcolorable _Graph;
let E;
cluster -> c-vcolorable for reverseEdgeDirections of G1, E;
coherence by Th33;
end;
Lm3:
for x being object, X being set, f being Function
st x in rng f holds rng(f +* (X --> x)) c= rng f
proof
let x be object, X be set, f be Function;
assume x in rng f;
then rng f \/ {x} = rng f by ZFMISC_1:40;
then A1: rng f \/ rng(X --> x) c= rng f by XBOOLE_1:9;
rng(f +* (X --> x)) c= rng f \/ rng(X --> x) by FUNCT_4:17;
hence rng(f +* (X --> x)) c= rng f by A1, XBOOLE_1:1;
end;
theorem Th34:
for G1 being addVertices of G2, V
holds G1 is c-vcolorable iff G2 is c-vcolorable
proof
let G1 be addVertices of G2, V;
hereby
assume A1: G1 is c-vcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is c-vcolorable by A1, Th31;
end;
assume G2 is c-vcolorable;
:: we choose a proper coloring and color the added vertices
:: in any color of those already taken
then consider f2 being VColoring of G2 such that
A2: f2 is proper & card rng f2 c= c;
set x = the Element of rng f2;
set h = (V \ the_Vertices_of G2) --> x, f1 = f2 +* h;
A3: dom h = V \ the_Vertices_of G2;
then reconsider f1 as VColoring of G1 by Th4;
A4: f1 is proper by A2, A3, Th19;
card rng f1 c= card rng f2 by Lm3, CARD_1:11;
hence thesis by A2, A4, XBOOLE_1:1;
end;
registration
let c be non zero Cardinal;
let G2 be c-vcolorable _Graph;
let V;
cluster -> c-vcolorable for addVertices of G2, V;
coherence by Th34;
end;
theorem
for v,w being Vertex of G2, e being object, G1 being addEdge of G2,v,e,w
st v,w are_adjacent holds G1 is c-vcolorable iff G2 is c-vcolorable
proof
let v,w be Vertex of G2, e be object, G1 be addEdge of G2,v,e,w;
assume A1: v,w are_adjacent;
hereby
assume A2: G1 is c-vcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is c-vcolorable by A2, Th31;
end;
assume G2 is c-vcolorable;
then consider f2 being VColoring of G2 such that
A3: f2 is proper & card rng f2 c= c;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:102;
then reconsider f1 = f2 as VColoring of G1;
f1 is proper by A1, A3, Th20;
hence thesis by A3;
end;
theorem Th36:
for v,e,w being object, G1 being addEdge of G2,v,e,w
st v <> w & G2 is c-vcolorable holds G1 is (c+`1)-vcolorable
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
assume A1: v <> w & G2 is c-vcolorable;
per cases;
suppose A2: not e in the_Edges_of G2 & v in the_Vertices_of G2 &
w in the_Vertices_of G2;
consider f2 being VColoring of G2 such that
A3: f2 is proper & card rng f2 c= c by A1;
:: given a proper coloring of the subgraph, we
:: color one end of the new edge in a new color
set h = w .--> rng f2, f1 = f2 +* h;
reconsider f1 as VColoring of G2 by A2;
the_Vertices_of G1 = the_Vertices_of G2 by A2, GLIB_006:102;
then reconsider f1 as VColoring of G1;
not rng f2 in rng f2;
then A4: f1 is proper by A1, A2, A3, Th22;
rng f2 \/ rng h = rng f2 \/ rng{[w,rng f2]} by FUNCT_4:82
.= rng f2 \/ {rng f2} by RELAT_1:9;
then A5: card rng f1 c= card(rng f2 \/ {rng f2}) by FUNCT_4:17, CARD_1:11;
card(rng f2 \/ {rng f2}) c= card rng f2 +` card{rng f2} by CARD_2:34;
then card(rng f2 \/ {rng f2}) c= card rng f2 +` 1 by CARD_1:30;
then A6: card rng f1 c= card rng f2 +` 1 by A5, XBOOLE_1:1;
card rng f2 +` 1 c= c +` 1 by A3, CARD_2:83;
hence thesis by A4, A6, XBOOLE_1:1;
end;
suppose not(not e in the_Edges_of G2 & v in the_Vertices_of G2 &
w in the_Vertices_of G2);
then G1 == G2 by GLIB_006:def 11;
then G1 is c-vcolorable by A1, Th32;
hence thesis by Th27, CARD_2:94;
end;
end;
Lm4:
for G2 being non edgeless _Graph, v being Vertex of G2, e,w being object
for G1 being addAdjVertex of G2,v,e,w
st not e in the_Edges_of G2 & not w in the_Vertices_of G2
holds G2 is c-vcolorable implies G1 is c-vcolorable
proof
let G2 be non edgeless _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not e in the_Edges_of G2 & not w in the_Vertices_of G2;
assume G2 is c-vcolorable;
then consider f2 being VColoring of G2 such that
A2: f2 is proper & card rng f2 c= c;
set e0 = the Element of the_Edges_of G2;
set x = the Element of (rng f2)\{f2.v};
(rng f2)\{f2.v} <> {}
proof
assume (rng f2)\{f2.v} = {};
then rng f2 = {} or rng f2 = {f2.v} by ZFMISC_1:58;
then card rng f2 = 0 or card rng f2 = 1 by CARD_1:30;
then G2 is 0-vcolorable or G2 is 1-vcolorable by A2;
hence contradiction;
end;
then A3: x in rng f2 & x <> f2.v by ZFMISC_1:56;
set h = w .--> x, f1 = f2 +* h;
reconsider f1 as VColoring of G1 by A1, Th6;
A4: f1 is proper by A1, A2, A3, Th24;
rng f2 \/ rng h = rng f2 \/ rng{[w,x]} by FUNCT_4:82
.= rng f2 \/ {x} by RELAT_1:9
.= rng f2 by A3, ZFMISC_1:40;
then card rng f1 c= card rng f2 by FUNCT_4:17, CARD_1:11;
hence thesis by A2, A4, XBOOLE_1:1;
end;
theorem Th37:
for G2 being non edgeless _Graph, 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
let G2 be non edgeless _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
hereby
assume A1: G1 is c-vcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is c-vcolorable by A1, Th31;
end;
assume A2: G2 is c-vcolorable;
per cases;
suppose not e in the_Edges_of G2 & v in the_Vertices_of G2 &
not w in the_Vertices_of G2;
hence thesis by A2, Lm4;
end;
suppose A3: not e in the_Edges_of G2 & not v in the_Vertices_of G2 &
w in the_Vertices_of G2;
set G3 = the reverseEdgeDirections of G1, {e};
G3 is addAdjVertex of G2,w,e,v by A3, GLIBPRE1:66;
then G3 is c-vcolorable by A2, A3, Lm4;
hence thesis by Th33;
end;
suppose not((not e in the_Edges_of G2 & v in the_Vertices_of G2 &
not w in the_Vertices_of G2) or (not e in the_Edges_of G2 &
not v in the_Vertices_of G2 & w in the_Vertices_of G2));
then G1 == G2 by GLIB_006:def 12;
hence thesis by A2, Th32;
end;
end;
Lm5:
for G2 being edgeless _Graph, v being Vertex of G2, 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
let G2 be edgeless _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not w in the_Vertices_of G2;
A2: not e in the_Edges_of G2;
set x = the object, y = {x};
set h1 = the_Vertices_of G2 --> x, h2 = w .--> y, f = h1 +* h2;
dom f = dom h1 \/ dom h2 by FUNCT_4:def 1
.= the_Vertices_of G2 \/ dom{[w,y]} by FUNCT_4:82
.= the_Vertices_of G2 \/ {w} by RELAT_1:9
.= the_Vertices_of G1 by A1, A2, GLIB_006:def 12;
then reconsider f as VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
now
let e9,v9,w9 be object;
assume A3: e9 DJoins v9,w9,G1;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, GLIB_006:def 12
.= {e};
then e9 in {e} by A3, GLIB_000:def 14;
then A4: e9 = e by TARSKI:def 1;
e DJoins v,w,G1 by A1, A2, GLIB_006:131;
then A5: v = v9 & w = w9 by A3, A4, GLIB_000:125;
v <> w by A1;
then f.v = h1.v & f.w = y by FUNCT_4:83, FUNCT_4:113;
then f.v in f.w;
hence f.v9 <> f.w9 by A5;
end;
then A6: f is proper by Th11;
rng h1 \/ rng h2 = {x} \/ rng h2 by FUNCOP_1:8
.= {x} \/ rng{[w,y]} by FUNCT_4:82
.= {x} \/ {y} by RELAT_1:9
.= {x,y} by ENUMSET1:1;
then A7: card rng f c= card {x,y} by FUNCT_4:17, CARD_1:11;
x in y by TARSKI:def 1;
then x <> y by ORDINAL1:5;
then card rng f c= 2 by A7, CARD_2:57;
hence thesis by A6;
end;
theorem Th38:
for G2 being edgeless _Graph, v,e,w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 2-vcolorable
proof
let G2 be edgeless _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
per cases;
suppose not e in the_Edges_of G2 & v in the_Vertices_of G2 &
not w in the_Vertices_of G2;
hence thesis by Lm5;
end;
suppose A1: not e in the_Edges_of G2 & not v in the_Vertices_of G2 &
w in the_Vertices_of G2;
set G3 = the reverseEdgeDirections of G1, {e};
G3 is addAdjVertex of G2,w,e,v by A1, GLIBPRE1:66;
then G3 is 2-vcolorable by A1, Lm5;
hence thesis by Th33;
end;
suppose not((not e in the_Edges_of G2 & v in the_Vertices_of G2 &
not w in the_Vertices_of G2) or (not e in the_Edges_of G2 &
not v in the_Vertices_of G2 & w in the_Vertices_of G2));
then G1 == G2 & G2 is 1-vcolorable by GLIB_006:def 12;
then G1 is 1-vcolorable by Th32;
hence thesis by Th27, FIELD_5:3;
end;
end;
theorem Th39:
for v being object, G1 being addAdjVertexAll of G2,v,V
st G2 is c-vcolorable holds G1 is (c+`1)-vcolorable
proof
let v be object, G1 be addAdjVertexAll of G2,v,V;
assume A1: G2 is c-vcolorable;
per cases;
suppose A2: not v in the_Vertices_of G2 & V c= the_Vertices_of G2;
consider f2 being VColoring of G2 such that
A3: f2 is proper & card rng f2 c= c by A1;
set h = v .--> rng f2, f1 = f2 +* h;
reconsider f1 as VColoring of G1 by A2, Th7;
not rng f2 in rng f2;
then A4: f1 is proper by A2, A3, Th25;
rng f2 \/ rng h = rng f2 \/ rng{[v,rng f2]} by FUNCT_4:82
.= rng f2 \/ {rng f2} by RELAT_1:9;
then A5: card rng f1 c= card(rng f2 \/ {rng f2}) by FUNCT_4:17, CARD_1:11;
card(rng f2 \/ {rng f2}) c= card rng f2 +` card{rng f2} by CARD_2:34;
then card(rng f2 \/ {rng f2}) c= card rng f2 +` 1 by CARD_1:30;
then A6: card rng f1 c= card rng f2 +` 1 by A5, XBOOLE_1:1;
card rng f2 +` 1 c= c +` 1 by A3, CARD_2:84;
hence thesis by A4, A6, XBOOLE_1:1;
end;
suppose not(not v in the_Vertices_of G2 & V c= the_Vertices_of G2);
then G1 == G2 by GLIB_007:def 4;
then G1 is c-vcolorable by A1, Th32;
hence thesis by Th27, CARD_2:94;
end;
end;
theorem Th40:
for G2 being removeParallelEdges of G1
holds G1 is c-vcolorable iff G2 is c-vcolorable
proof
let G2 be removeParallelEdges of G1;
thus G1 is c-vcolorable implies G2 is c-vcolorable by Th31;
assume G2 is c-vcolorable;
then consider f2 being VColoring of G2 such that
A1: f2 is proper & card rng f2 c= c;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 33;
then reconsider f1 = f2 as VColoring of G1;
now
let v,w be Vertex of G1;
reconsider v9=v, w9=w as Vertex of G2 by GLIB_000:def 33;
assume v,w are_adjacent;
then v9,w9 are_adjacent by GLIBPRE1:75;
hence f1.v <> f1.w by A1;
end;
then f1 is proper;
hence thesis by A1;
end;
registration
let c be non zero Cardinal;
let G1 be c-vcolorable _Graph;
cluster -> c-vcolorable for removeParallelEdges of G1;
coherence;
end;
theorem Th41:
for G2 being removeDParallelEdges of G1
holds G1 is c-vcolorable iff G2 is c-vcolorable
proof
let G2 be removeDParallelEdges of G1;
thus G1 is c-vcolorable implies G2 is c-vcolorable by Th31;
assume A1: G2 is c-vcolorable;
set G3 = the removeParallelEdges of G2;
G3 is c-vcolorable & G3 is removeParallelEdges of G1
by A1, Th31, GLIB_009:95;
hence thesis by Th40;
end;
registration
let c be non zero Cardinal;
let G1 be c-vcolorable _Graph;
cluster -> c-vcolorable for removeDParallelEdges of G1;
coherence;
end;
theorem Th42:
for F being PGraphMapping of G1, G2
st F is weak_SG-embedding & G2 is c-vcolorable holds G1 is c-vcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is c-vcolorable;
then consider f2 being VColoring of G2 such that
A2: f2 is proper & card rng f2 c= c;
reconsider f1 = f2*F_V as VColoring of G1 by A1, Th9;
card rng f1 c= card rng f2 by RELAT_1:26, CARD_1:11;
then card rng f1 c= c by A2, XBOOLE_1:1;
hence thesis by A1, A2, Th26;
end;
theorem Th43:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is c-vcolorable iff G2 is c-vcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
hence G1 is c-vcolorable implies G2 is c-vcolorable by Th42;
thus G2 is c-vcolorable implies G1 is c-vcolorable by A1, Th42;
end;
registration
let c be non zero Cardinal;
let G be c-vcolorable _Graph;
cluster G-isomorphic -> c-vcolorable for _Graph;
coherence
proof
let H be _Graph;
assume H is G-isomorphic;
then consider F being PGraphMapping of G, H such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th43;
end;
end;
definition
let G;
attr G is finite-vcolorable means :: or finitely-vcolorable
:Def3:
ex n st G is n-vcolorable;
end;
registration
cluster finite-vcolorable -> loopless for _Graph;
coherence;
cluster vertex-finite loopless -> finite-vcolorable for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is vertex-finite loopless;
then G is G.order()-vcolorable by Th29;
hence thesis by A1;
end;
cluster edgeless -> finite-vcolorable for _Graph;
coherence by Th30;
let n;
cluster n-vcolorable -> finite-vcolorable for _Graph;
coherence;
end;
registration
cluster finite-vcolorable for _Graph;
existence
proof
take the edgeless _Graph;
thus thesis;
end;
cluster non finite-vcolorable for _Graph;
existence
proof
take the non loopless _Graph;
thus thesis;
end;
end;
registration
let G be finite-vcolorable _Graph;
cluster -> finite-vcolorable for Subgraph of G;
coherence
proof
let H be Subgraph of G;
consider n such that
A1: G is n-vcolorable by Def3;
H is n-vcolorable by A1, Th31;
hence thesis;
end;
end;
registration
let G be non finite-vcolorable _Graph;
cluster -> non finite-vcolorable for Supergraph of G;
coherence
proof
let H be Supergraph of G;
G is Subgraph of H by GLIB_006:57;
hence thesis;
end;
end;
theorem
G1 == G2 & G1 is finite-vcolorable implies G2 is finite-vcolorable
proof
assume A1: G1 == G2 & G1 is finite-vcolorable;
then consider n such that
A2: G1 is n-vcolorable;
G2 is n-vcolorable by A1, A2, Th32;
hence thesis;
end;
Lm6:
for G2 being reverseEdgeDirections of G1, E
st G1 is finite-vcolorable holds G2 is finite-vcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
assume G1 is finite-vcolorable;
then consider n such that
A1: G1 is n-vcolorable;
G2 is n-vcolorable by A1, Lm2;
hence thesis;
end;
theorem Th45:
for G2 being reverseEdgeDirections of G1, E
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable by Lm6;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by Lm6;
end;
registration
let G1 be finite-vcolorable _Graph; let E;
cluster -> finite-vcolorable for reverseEdgeDirections of G1, E;
coherence by Th45;
end;
registration
let G1 be non finite-vcolorable _Graph; let E;
cluster -> non finite-vcolorable for reverseEdgeDirections of G1, E;
coherence by Th45;
end;
theorem Th46:
for G1 being addVertices of G2, V
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let G1 be addVertices of G2, V;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable;
assume G2 is finite-vcolorable;
then consider n such that
A1: G2 is n-vcolorable;
G1 is n-vcolorable by A1, Th34;
hence thesis;
end;
registration
let G2 be finite-vcolorable _Graph; let V;
cluster -> finite-vcolorable for addVertices of G2, V;
coherence by Th46;
end;
theorem
for v,e,w being object, G1 being addEdge of G2,v,e,w st v <> w
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
assume A1: v <> w;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable;
assume G2 is finite-vcolorable;
then consider n such that
A2: G2 is n-vcolorable;
G1 is (n+`1)-vcolorable by A1, A2, Th36;
hence thesis;
end;
theorem Th48:
for v,e,w being object, G1 being addAdjVertex of G2,v,e,w
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable;
assume G2 is finite-vcolorable;
then consider n such that
A1: G2 is n-vcolorable;
per cases;
suppose G2 is non edgeless;
then G1 is n-vcolorable by A1, Th37;
hence thesis;
end;
suppose G2 is edgeless;
then G1 is 2-vcolorable by Th38;
hence thesis;
end;
end;
registration
let G2 be finite-vcolorable _Graph, v,e,w be object;
cluster -> finite-vcolorable for addAdjVertex of G2,v,e,w;
coherence by Th48;
end;
theorem Th49:
for v being object, G1 being addAdjVertexAll of G2,v,V
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let v be object, G1 be addAdjVertexAll of G2,v,V;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable;
assume G2 is finite-vcolorable;
then consider n such that
A1: G2 is n-vcolorable;
G1 is (n+`1)-vcolorable by A1, Th39;
hence thesis;
end;
registration
let G2 be finite-vcolorable _Graph, v be object; let V;
cluster -> finite-vcolorable for addAdjVertexAll of G2,v,V;
coherence by Th49;
end;
theorem Th50:
for G2 being removeParallelEdges of G1
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let G2 be removeParallelEdges of G1;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable;
assume G2 is finite-vcolorable;
then consider n such that
A1: G2 is n-vcolorable;
G1 is n-vcolorable by A1, Th40;
hence thesis;
end;
registration
let G1 be non finite-vcolorable _Graph;
cluster -> non finite-vcolorable for removeParallelEdges of G1;
coherence by Th50;
end;
theorem Th51:
for G2 being removeDParallelEdges of G1
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let G2 be removeDParallelEdges of G1;
thus G1 is finite-vcolorable implies G2 is finite-vcolorable;
assume G2 is finite-vcolorable;
then consider n such that
A1: G2 is n-vcolorable;
G1 is n-vcolorable by A1, Th41;
hence thesis;
end;
registration
let G1 be non finite-vcolorable _Graph;
cluster -> non finite-vcolorable for removeDParallelEdges of G1;
coherence by Th51;
end;
theorem Th52:
for F being PGraphMapping of G1,G2
st F is weak_SG-embedding & G2 is finite-vcolorable
holds G1 is finite-vcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is finite-vcolorable;
then consider n such that
A2: G2 is n-vcolorable;
G1 is n-vcolorable by A1, A2, Th42;
hence thesis;
end;
theorem Th53:
for F being PGraphMapping of G1, G2 st F is isomorphism
holds G1 is finite-vcolorable iff G2 is finite-vcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
hence G1 is finite-vcolorable implies G2 is finite-vcolorable by Th52;
thus G2 is finite-vcolorable implies G1 is finite-vcolorable by A1, Th52;
end;
registration
let G be finite-vcolorable _Graph;
cluster G-isomorphic -> finite-vcolorable for _Graph;
coherence
proof
let H be _Graph;
assume H is G-isomorphic;
then consider F being PGraphMapping of G, H such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th53;
end;
end;
deffunc VColSet(_Graph) =
{ c where c is cardinal Subset of $1.order() : $1 is c-vcolorable };
definition
let G be _Graph;
func G.vChromaticNum() -> Cardinal equals :: chi
meet { c where c is cardinal Subset of G.order() : G is c-vcolorable };
coherence
proof
now
let a be set;
assume a in VColSet(G);
then consider c being cardinal Subset of G.order() such that
A1: a = c & G is c-vcolorable;
thus a is cardinal number by A1;
end;
hence thesis by GLIBPRE0:15;
end;
end;
theorem Th54:
G is loopless implies G is G.vChromaticNum()-vcolorable
proof
assume G is loopless;
then G is G.order()-vcolorable & G.order() c= G.order() by Th29;
then A1: G.order() in VColSet(G);
now
let a be set;
assume a in VColSet(G);
then consider c being cardinal Subset of G.order() such that
A2: a = c & G is c-vcolorable;
thus a is cardinal number by A2;
end;
then consider c being Cardinal such that
A3: c in VColSet(G) & c = G.vChromaticNum() by A1, GLIBPRE0:14;
consider c9 being cardinal Subset of G.order() such that
A4: c = c9 & G is c9-vcolorable by A3;
thus thesis by A3, A4;
end;
theorem Th55:
G is non loopless iff G.vChromaticNum() = 0
proof
hereby
assume A1: G is non loopless;
now
given x being object such that
A2: x in VColSet(G);
consider c being cardinal Subset of G.order() such that
A3: x = c & G is c-vcolorable by A2;
thus contradiction by A1, A3;
end;
hence G.vChromaticNum() = 0 by XBOOLE_0:def 1, SETFAM_1:1;
end;
assume A4: G.vChromaticNum() = 0 & G is loopless;
per cases;
suppose A5: VColSet(G) = {};
G is G.order()-vcolorable & G.order() c= G.order() by A4, Th29;
then G.order() in VColSet(G);
hence contradiction by A5;
end;
suppose A6: VColSet(G) <> {};
now
let a be set;
assume a in VColSet(G);
then consider c being cardinal Subset of G.order() such that
A7: a = c & G is c-vcolorable;
thus a is cardinal number by A7;
end;
then consider c being Cardinal such that
A8: c in VColSet(G) & c = G.vChromaticNum() by A6, GLIBPRE0:14;
consider c9 being cardinal Subset of G.order() such that
A9: c = c9 & G is c9-vcolorable by A8;
thus contradiction by A4, A8, A9;
end;
end;
registration
let G be loopless _Graph;
cluster G.vChromaticNum() -> non zero;
coherence by Th55;
end;
registration
let G be non loopless _Graph;
cluster G.vChromaticNum() -> zero;
coherence by Th55;
end;
theorem Th56:
G.vChromaticNum() c= G.order()
proof
per cases;
suppose G is non loopless;
then G.vChromaticNum() = 0;
hence thesis by XBOOLE_1:2;
end;
suppose G is loopless;
then G is G.order()-vcolorable & G.order() c= G.order() by Th29;
then G.order() in VColSet(G);
hence G.vChromaticNum() c= G.order() by SETFAM_1:3;
end;
end;
theorem Th57:
G is c-vcolorable implies G.vChromaticNum() c= c
proof
assume A1: G is c-vcolorable;
per cases;
suppose not G.order() in c;
then c c= G.order() by ORDINAL1:16;
then c in VColSet(G) by A1;
hence thesis by SETFAM_1:3;
end;
suppose G.order() in c;
then G.vChromaticNum() in c by Th56, ORDINAL1:12;
hence thesis by ORDINAL1:def 2;
end;
end;
theorem Th58:
(G is c-vcolorable & for d being Cardinal st G is d-vcolorable holds c c= d)
implies G.vChromaticNum() = c
proof
assume G is c-vcolorable;
then A1: G.vChromaticNum() c= c & G is loopless by Th57;
assume A2: for d being Cardinal st G is d-vcolorable holds c c= d;
G is G.order()-vcolorable & G.order() c= G.order() by A1, Th29;
then A3: G.order() in VColSet(G);
now
let x be set;
assume x in VColSet(G);
then consider d being cardinal Subset of G.order() such that
A4: x = d & G is d-vcolorable;
thus c c= x by A2, A4;
end;
then c c= G.vChromaticNum() by A3, SETFAM_1:5;
hence thesis by A1, XBOOLE_0:def 10;
end;
registration
let G be finite-vcolorable _Graph;
cluster G.vChromaticNum() -> natural;
coherence
proof
consider n such that
A1: G is n-vcolorable by Def3;
G.vChromaticNum() c= n by A1, Th57;
hence thesis;
end;
end;
definition
let G be finite-vcolorable _Graph;
redefine func G.vChromaticNum() -> Nat; :: redefines .vChromaticNum() (GLCOLO00, definition)
coherence;
end;
theorem Th59:
for G being loopless _Graph holds 1 c= G.vChromaticNum()
proof
let G be loopless _Graph;
assume not 1 c= G.vChromaticNum();
then G.vChromaticNum() in 1 by ORDINAL1:16;
hence contradiction by CARD_1:49, TARSKI:def 1;
end;
theorem Th60:
G is edgeless iff G.vChromaticNum() = 1
proof
hereby
assume A1: G is edgeless;
then A2: G.vChromaticNum() c= 1 by Th57;
1 c= G.vChromaticNum() by A1, Th59;
hence G.vChromaticNum() = 1 by A2, XBOOLE_0:def 10;
end;
assume A3: G.vChromaticNum() = 1;
then G is loopless;
then G is 1-vcolorable by A3, Th54;
hence G is edgeless;
end;
theorem
for G being loopless non edgeless _Graph holds 2 c= G.vChromaticNum()
proof
let G be loopless non edgeless _Graph;
assume not 2 c= G.vChromaticNum();
then G.vChromaticNum() in 2 by ORDINAL1:16;
then G.vChromaticNum() = 1 by CARD_1:50, TARSKI:def 2;
hence contradiction by Th60;
end;
theorem
for G being loopless _Graph
holds G is complete implies G.vChromaticNum() = G.order()
proof
let G be loopless _Graph;
G is G.order()-vcolorable & G.order() c= G.order() by Th29;
then A1: G.order() in VColSet(G);
assume A2: G is complete;
A3: G.vChromaticNum() c= G.order() by Th56;
now
let x be set;
assume x in VColSet(G);
then consider c being cardinal Subset of G.order() such that
A4: x = c & G is c-vcolorable;
consider f being VColoring of G such that
A5: f is proper & card rng f c= c by A4;
thus G.order() c= x
proof
assume not G.order() c= x;
then c in G.order() by A4, ORDINAL1:16;
then card rng f in G.order() by A5, ORDINAL1:12;
then card rng f in card dom f by PARTFUN1:def 2;
then card rng f <> card dom f;
:: use the pigeon hole principle to find two vertices in the same color
then f is non one-to-one by CARD_1:70;
then consider v,w being object such that
A6: v in dom f & w in dom f & f.v = f.w & v <> w by FUNCT_1:def 4;
reconsider v,w as Vertex of G by A6;
v,w are_adjacent by A2, A6, CHORD:def 6;
hence contradiction by A5, A6;
end;
end;
then G.order() c= G.vChromaticNum() by A1, SETFAM_1:5;
hence thesis by A3, XBOOLE_0:def 10;
end;
theorem Th63:
for G being loopless _Graph, H being Subgraph of G
holds H.vChromaticNum() c= G.vChromaticNum()
proof
let G be loopless _Graph, H be Subgraph of G;
G is G.vChromaticNum()-vcolorable by Th54;
hence thesis by Th57;
end;
theorem
G1 == G2 implies G1.vChromaticNum() = G2.vChromaticNum()
proof
assume A1: G1 == G2;
now
let x be object;
hereby
assume x in VColSet(G1);
then consider c being cardinal Subset of G1.order() such that
A2: x = c & G1 is c-vcolorable;
G1.order() = G2.order() & G2 is c-vcolorable
by A1, A2, Th32, GLIB_000:90;
hence x in VColSet(G2) by A2;
end;
assume x in VColSet(G2);
then consider c being cardinal Subset of G2.order() such that
A3: x = c & G2 is c-vcolorable;
G1.order() = G2.order() & G1 is c-vcolorable by A1, A3, Th32, GLIB_000:90;
hence x in VColSet(G1) by A3;
end;
hence thesis by TARSKI:2;
end;
theorem
for G2 being reverseEdgeDirections of G1, E
holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let G2 be reverseEdgeDirections of G1, E;
now
let x be object;
hereby
assume x in VColSet(G1);
then consider c being cardinal Subset of G1.order() such that
A1: x = c & G1 is c-vcolorable;
G1.order() = G2.order() & G2 is c-vcolorable by A1, Th33, GLIB_007:24;
hence x in VColSet(G2) by A1;
end;
assume x in VColSet(G2);
then consider c being cardinal Subset of G2.order() such that
A2: x = c & G2 is c-vcolorable;
G1.order() = G2.order() & G1 is c-vcolorable by A2, Th33, GLIB_007:24;
hence x in VColSet(G1) by A2;
end;
hence thesis by TARSKI:2;
end;
theorem
for G1 being addVertices of G2, V
holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let G1 be addVertices of G2, V;
per cases;
suppose G2 is non loopless;
then G2.vChromaticNum() = 0 & G1.vChromaticNum() = 0;
hence thesis;
end;
suppose A1: G2 is loopless;
now
G1 is G1.vChromaticNum()-vcolorable by A1, Th54;
hence G2 is G1.vChromaticNum()-vcolorable by Th34;
let c;
assume G2 is c-vcolorable;
then G1 is c-vcolorable by Th34;
hence G1.vChromaticNum() c= c by Th57;
end;
hence thesis by Th58;
end;
end;
theorem
for G2 being non edgeless _Graph, v,e,w being object
for G1 being addAdjVertex of G2,v,e,w
holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let G2 be non edgeless _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
per cases;
suppose G2 is non loopless;
then G2.vChromaticNum() = 0 & G1.vChromaticNum() = 0;
hence thesis;
end;
suppose A1: G2 is loopless;
now
G1 is G1.vChromaticNum()-vcolorable by A1, Th54;
hence G2 is G1.vChromaticNum()-vcolorable by Th37;
let c;
assume G2 is c-vcolorable;
then G1 is c-vcolorable by Th37;
hence G1.vChromaticNum() c= c by Th57;
end;
hence thesis by Th58;
end;
end;
theorem
for G2 being edgeless _Graph, v being Vertex of G2, 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
let G2 be edgeless _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not w in the_Vertices_of G2;
now
thus G1 is 2-vcolorable by Th38;
let c;
assume A2: G1 is c-vcolorable;
assume not 2 c= c;
then c in {0,1} by ORDINAL1:16, CARD_1:50;
then per cases by TARSKI:def 2;
suppose c = 0;
hence contradiction by A2;
end;
suppose A3: c = 1;
not e in the_Edges_of G2;
then e DJoins v,w,G1 by A1, GLIB_006:131;
then e in the_Edges_of G1 by GLIB_000:def 14;
hence contradiction by A2, A3;
end;
end;
hence thesis by Th58;
end;
theorem
for G2 being edgeless _Graph, v,e being object, 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
let G2 be edgeless _Graph, v,e be object, w be Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not v in the_Vertices_of G2;
now
thus G1 is 2-vcolorable by Th38;
let c;
assume A2: G1 is c-vcolorable;
assume not 2 c= c;
then c in {0,1} by ORDINAL1:16, CARD_1:50;
then per cases by TARSKI:def 2;
suppose c = 0;
hence contradiction by A2;
end;
suppose A3: c = 1;
not e in the_Edges_of G2;
then e DJoins v,w,G1 by A1, GLIB_006:132;
then e in the_Edges_of G1 by GLIB_000:def 14;
hence contradiction by A2, A3;
end;
end;
hence thesis by Th58;
end;
theorem Th70:
for v being object, G1 being addAdjVertexAll of G2,v,V
holds G1.vChromaticNum() c= G2.vChromaticNum() +` 1
proof
let v be object, G1 be addAdjVertexAll of G2,v,V;
per cases;
suppose G2 is non loopless;
then G1.vChromaticNum() = 0;
hence thesis by XBOOLE_1:2;
end;
suppose G2 is loopless;
then G1 is (G2.vChromaticNum()+`1)-vcolorable by Th54, Th39;
hence thesis by Th57;
end;
end;
theorem
for G2 being loopless _Graph, 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
let G2 be loopless _Graph, v be object;
let G1 be addAdjVertexAll of G2,v;
assume A1: not v in the_Vertices_of G2;
A2: G1.vChromaticNum() c= G2.vChromaticNum() +` 1 by Th70;
A3: G2 is Subgraph of G1 by GLIB_006:57;
then A4: G2.vChromaticNum() c= G1.vChromaticNum() by Th63;
per cases;
suppose G2.vChromaticNum() is finite;
then reconsider C2 = G2.vChromaticNum() as Nat;
A5: G1.vChromaticNum() c= C2 +` 1 by A2;
then reconsider C1 = G1.vChromaticNum() as Nat;
A6: C1 <= C2 + 1 by A5, FIELD_5:3;
now
assume C1 <> C2 + 1;
:: if C2+1 colors are not the minimum, C2 colors are
then C1 < C2 + 1 by A6, XXREAL_0:1;
then A7: C1 <= C2 by NAT_1:13;
C2 <= C1 by A4, FIELD_5:3;
then C1 = C2 by A7, XXREAL_0:1;
then G1 is C2-vcolorable by Th54;
:: show that for C2 colors and a coloring of G1
:: these C2 colors will already be used in the underlying G2
then consider f1 being VColoring of G1 such that
A8: f1 is proper & card rng f1 c= C2;
reconsider R1 = rng f1 as finite set by A8;
reconsider f2 = f1 | the_Vertices_of G2 as proper VColoring of G2
by A3, A8, Th3, Th15;
reconsider R2 = rng f2 as Subset of R1 by RELAT_1:70;
G2 is (card R2)-vcolorable;
then C2 c= card R2 by Th57;
then A9: card R1 c= card R2 by A8, XBOOLE_1:1;
card R2 c= card R1 by CARD_1:11;
then A10: R1 = R2 by A9, XBOOLE_0:def 10, CARD_2:102;
:: conclude that there is always a vertex adjacent to v in G1
:: with the same color
reconsider v as Vertex of G1 by A1, GLIB_007:50;
v in the_Vertices_of G1;
then v in dom f1 by PARTFUN1:def 2;
then f1.v in R2 by A10, FUNCT_1:3;
then consider u being object such that
A11: u in dom f2 & f2.u = f1.v by FUNCT_1:def 3;
A12: f1.u = f1.v by A11, FUNCT_1:47;
A13: u in the_Vertices_of G2 by A11;
then reconsider u as Vertex of G1 by GLIB_006:68;
u in v.allNeighbors() by A1, A13, GLIBPRE0:55;
hence contradiction by A8, A12, GLIBPRE1:41;
end;
then C1 = C2 +` 1;
hence thesis;
end;
suppose A14: G2.vChromaticNum() is infinite;
then A15: omega c= G2.vChromaticNum() by ORDINAL1:16, CARD_1:61;
1 in omega;
then G2.vChromaticNum() = G2.vChromaticNum() +` 1 by A14, A15, CARD_2:76;
hence thesis by A2, A4, XBOOLE_0:def 10;
end;
end;
theorem
for G2 being removeParallelEdges of G1
holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let G2 be removeParallelEdges of G1;
per cases;
suppose G1 is non loopless;
then G1.vChromaticNum() = 0 & G2.vChromaticNum() = 0;
hence thesis;
end;
suppose G1 is loopless;
then G2 is G1.vChromaticNum()-vcolorable & for c st G2 is c-vcolorable
holds G1.vChromaticNum() c= c by Th40, Th54, Th57;
hence thesis by Th58;
end;
end;
theorem
for G2 being removeDParallelEdges of G1
holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let G2 be removeDParallelEdges of G1;
per cases;
suppose G1 is non loopless;
then G1.vChromaticNum() = 0 & G2.vChromaticNum() = 0;
hence thesis;
end;
suppose G1 is loopless;
then G2 is G1.vChromaticNum()-vcolorable & for c st G2 is c-vcolorable
holds G1.vChromaticNum() c= c by Th41, Th54, Th57;
hence thesis by Th58;
end;
end;
theorem
for G1 being _Graph, G2 being loopless _Graph
for F being PGraphMapping of G1, G2 st F is weak_SG-embedding
holds G1.vChromaticNum() c= G2.vChromaticNum()
proof
let G1 be _Graph, G2 be loopless _Graph, F be PGraphMapping of G1, G2;
assume F is weak_SG-embedding;
then G1 is G2.vChromaticNum()-vcolorable by Th42, Th54;
hence thesis by Th57;
end;
theorem Th75:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
per cases;
suppose G1 is non loopless;
then G1 is non loopless & G2 is non loopless by A1, GLIB_010:35;
then G1.vChromaticNum() = 0 & G2.vChromaticNum() = 0;
hence thesis;
end;
suppose A2: G1 is loopless;
now
G1 is G1.vChromaticNum()-vcolorable by A2, Th54;
hence G2 is G1.vChromaticNum()-vcolorable by A1, Th43;
let c;
assume G2 is c-vcolorable;
then G1 is c-vcolorable by A1, Th43;
hence G1.vChromaticNum() c= c by Th57;
end;
hence thesis by Th58;
end;
end;
theorem
for G2 being G1-isomorphic _Graph
holds G1.vChromaticNum() = G2.vChromaticNum()
proof
let G2 be G1-isomorphic _Graph;
consider F being PGraphMapping of G1, G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th75;
end;
begin :: Edge Colorings
definition
let G;
mode EColoring of G is ManySortedSet of the_Edges_of G;
end;
reserve g for EColoring of G;
theorem Th77:
for g9 being Function st rng g c= dom g9 holds g9*g is EColoring of G
proof
let g9 be Function;
assume rng g c= dom g9;
then dom(g9*g) = dom g by RELAT_1:27
.= the_Edges_of G by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
definition
let G, g; let g9 be ManySortedSet of rng g;
redefine func g9*g -> EColoring of G; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
rng g = dom g9 by PARTFUN1:def 2;
hence thesis by Th77;
end;
end;
theorem Th78:
for H being Subgraph of G holds g | the_Edges_of H is EColoring of H
proof
let H be Subgraph of G;
set g9 = g | the_Edges_of H;
the_Edges_of H c= the_Edges_of G;
then the_Edges_of H c= dom g by PARTFUN1:def 2;
then dom g9 = the_Edges_of H by RELAT_1:62;
hence thesis by PARTFUN1:def 2;
end;
theorem Th79:
for e being object, v,w being Vertex of G2, G1 being addEdge of G2,v,e,w
for g being EColoring of G2, x being object st not e in the_Edges_of G2
holds g +* (e .--> x) is EColoring of G1
proof
let e be object, v,w be Vertex of G2, G1 be addEdge of G2,v,e,w;
let g be EColoring of G2, x be object;
assume A1: not e in the_Edges_of G2;
A2: dom(e.-->x) = dom {[e,x]} by FUNCT_4:82
.= {e} by RELAT_1:9;
dom(g+*(e.-->x)) = dom g \/ dom(e.-->x) by FUNCT_4:def 1
.= the_Edges_of G2 \/ {e} by A2, PARTFUN1:def 2
.= the_Edges_of G1 by A1, GLIB_006:def 11;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem
for v,e being object, w being Vertex of G2, G1 being addAdjVertex of G2,v,e,w
for g being EColoring of G2, 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
let v,e be object, w be Vertex of G2, G1 be addAdjVertex of G2,v,e,w;
let g be EColoring of G2, x be object;
assume A1: not e in the_Edges_of G2 & not v in the_Vertices_of G2;
A2: dom(e.-->x) = dom {[e,x]} by FUNCT_4:82
.= {e} by RELAT_1:9;
dom(g+*(e.-->x)) = dom g \/ dom(e.-->x) by FUNCT_4:def 1
.= the_Edges_of G2 \/ {e} by A2, PARTFUN1:def 2
.= the_Edges_of G1 by A1, GLIB_006:def 12;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem
for v being Vertex of G2, e,w being object, G1 being addAdjVertex of G2,v,e,w
for g being EColoring of G2, 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
let v be Vertex of G2, e,w be object, G1 be addAdjVertex of G2,v,e,w;
let g be EColoring of G2, x be object;
assume A1: not e in the_Edges_of G2 & not w in the_Vertices_of G2;
A2: dom(e.-->x) = dom {[e,x]} by FUNCT_4:82
.= {e} by RELAT_1:9;
dom(g+*(e.-->x)) = dom g \/ dom(e.-->x) by FUNCT_4:def 1
.= the_Edges_of G2 \/ {e} by A2, PARTFUN1:def 2
.= the_Edges_of G1 by A1, GLIB_006:def 12;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem Th82:
for v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2,v,V, 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
let v be object, V be Subset of the_Vertices_of G2;
let G1 be addAdjVertexAll of G2,v,V, g2 be EColoring of G2;
let h be Function;
set E = dom h;
assume A1: not v in the_Vertices_of G2 & dom h = G1.edgesBetween(V,{v});
dom(g2+*h) = dom g2 \/ dom h by FUNCT_4:def 1
.= the_Edges_of G2 \/ E by PARTFUN1:def 2
.= the_Edges_of G1 by A1, GLIB_007:59;
hence thesis by RELAT_1:def 18, PARTFUN1:def 2;
end;
theorem Th83:
for F being PGraphMapping of G1,G st dom F_E = the_Edges_of G1
holds g*(F_E) is EColoring of G1
proof
let F be PGraphMapping of G1,G;
assume A1: dom F_E = the_Edges_of G1;
rng F_E c= the_Edges_of G;
then rng F_E c= dom g by PARTFUN1:def 2;
then dom(g*(F_E)) = dom F_E by RELAT_1:27;
hence thesis by A1, PARTFUN1:def 2;
end;
theorem Th84:
for F being PGraphMapping of G1,G st F is total
holds g*(F_E) is EColoring of G1
proof
let F be PGraphMapping of G1, G;
assume F is total;
then dom F_E = the_Edges_of G1 by GLIB_010:def 11;
hence thesis by Th83;
end;
definition
let G, g;
attr g is proper means
:Def5:
for v being Vertex of G holds g | v.edgesInOut() is one-to-one;
end;
theorem Th85:
g is proper iff for v being Vertex of G, e1, e2 being object
st e1 in v.edgesInOut() & e2 in v.edgesInOut() & g.e1 = g.e2 holds e1 = e2
proof
hereby
assume A1: g is proper;
let v be Vertex of G, e1,e2 be object;
set V = v.edgesInOut();
assume A2: e1 in V & e2 in V & g.e1 = g.e2;
V c= the_Edges_of G;
then V c= dom g by PARTFUN1:def 2;
then A3: e1 in dom(g|V) & e2 in dom(g|V) by A2, RELAT_1:62;
then g.e1 = (g|V).e1 & g.e2 = (g|V).e2 by FUNCT_1:47;
then (g|V).e1 = (g|V).e2 & g|V is one-to-one by A1, A2;
hence e1 = e2 by A3, FUNCT_1:def 4;
end;
assume A4: for v being Vertex of G, e1, e2 being object
st e1 in v.edgesInOut() & e2 in v.edgesInOut() & g.e1 = g.e2 holds e1 = e2;
let v be Vertex of G;
set V = v.edgesInOut();
now
let e1,e2 be object;
assume A5: e1 in dom(g|V) & e2 in dom(g|V) & (g|V).e1 = (g|V).e2;
then g.e1 = (g|V).e1 & g.e2 = (g|V).e2 by FUNCT_1:47;
hence e1 = e2 by A5, A4;
end;
hence thesis by FUNCT_1:def 4;
end;
theorem Th86:
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
hereby
assume A1: g is proper;
let e1,e2,v,w1,w2 be object;
assume A2: e1 Joins v,w1,G & e2 Joins v,w2,G & g.e1 = g.e2;
then reconsider v as Vertex of G by GLIB_000:13;
e1 in v.edgesInOut() & e2 in v.edgesInOut() by A2, GLIB_000:62;
hence e1 = e2 by A1, A2, Th85;
end;
assume A3: 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;
now
let v be Vertex of G, e1,e2 be object;
assume A4: e1 in v.edgesInOut() & e2 in v.edgesInOut() & g.e1 = g.e2;
then consider v1 being Vertex of G such that
A5: e1 Joins v,v1,G by GLIB_000:64;
consider v2 being Vertex of G such that
A6: e2 Joins v,v2,G by A4, GLIB_000:64;
thus e1 = e2 by A3, A4, A5, A6;
end;
hence thesis by Th85;
end;
theorem Th87:
for g9 being one-to-one Function, g2 being EColoring of G
st g2 = g9*g & g is proper holds g2 is proper
proof
let g9 be one-to-one Function, g2 be EColoring of G;
assume A1: g2 = g9*g & g is proper;
now
let v be Vertex of G;
set V = v.edgesInOut();
A2: g|V is one-to-one by A1;
g2|V = g9*(g|V) by A1, RELAT_1:83;
hence g2|V is one-to-one by A2;
end;
hence thesis;
end;
theorem
for g9 being one-to-one ManySortedSet of rng g
holds g is proper implies g9*g is proper by Th87;
registration
let G;
cluster one-to-one -> proper for EColoring of G;
coherence by FUNCT_1:52;
end;
registration
let G;
cluster one-to-one proper for EColoring of G;
existence
proof
reconsider g = id the_Edges_of G as EColoring of G;
take g;
thus thesis;
end;
end;
theorem Th89:
for H being Subgraph of G, g9 being EColoring of H
st g9 = g | the_Edges_of H & g is proper holds g9 is proper
proof
let H be Subgraph of G, g9 be EColoring of H;
assume A1: g9 = g | the_Edges_of H & g is proper;
now
let v be Vertex of H, e1, e2 be object;
assume A2: e1 in v.edgesInOut() & e2 in v.edgesInOut() & g9.e1 = g9.e2;
the_Vertices_of H c= the_Vertices_of G & v in the_Vertices_of H;
then reconsider w = v as Vertex of G;
A3: v.edgesInOut() c= w.edgesInOut() by GLIB_000:78;
g9.e1 = g.e1 & g9.e2 = g.e2 by A1, A2, FUNCT_1:49;
hence e1 = e2 by A1, A2, A3, Th85;
end;
hence thesis by Th85;
end;
theorem Th90:
for g1 being EColoring of G1, g2 being EColoring of G2
st G1 == G2 & g1 = g2 & g1 is proper holds g2 is proper
proof
let g1 be EColoring of G1, g2 be EColoring of G2;
assume A1: G1 == G2 & g1 = g2 & g1 is proper;
let v be Vertex of G2;
reconsider w = v as Vertex of G1 by A1, GLIB_000:def 34;
v.edgesInOut() = w.edgesInOut() by A1, GLIB_000:96;
hence g2 | v.edgesInOut() is one-to-one by A1;
end;
Lm7:
for G2 being reverseEdgeDirections of G1, E
for g1 being EColoring of G1, g2 being EColoring of G2
st g1 = g2 & g1 is proper holds g2 is proper
proof
let G2 be reverseEdgeDirections of G1, E;
let g1 be EColoring of G1, g2 be EColoring of G2;
assume A1: g1 = g2 & g1 is proper;
let v be Vertex of G2;
reconsider w = v as Vertex of G1 by GLIB_007:4;
v.edgesInOut() = w.edgesInOut() by GLIBPRE0:54;
hence g2 | v.edgesInOut() is one-to-one by A1;
end;
theorem Th91:
for G2 being reverseEdgeDirections of G1, E
for g1 being EColoring of G1, g2 being EColoring of G2
st g1 = g2 holds g1 is proper iff g2 is proper
proof
let G2 be reverseEdgeDirections of G1, E;
let g1 be EColoring of G1, g2 be EColoring of G2;
assume A1: g1 = g2;
hence g1 is proper implies g2 is proper by Lm7;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by A1, Lm7;
end;
theorem Th92:
for G1 being addVertices of G2, V
for g1 being EColoring of G1, g2 being EColoring of G2 st g1 = g2
holds g2 is proper implies g1 is proper
proof
let G1 be addVertices of G2, V;
let g1 be EColoring of G1, g2 be EColoring of G2;
assume A1: g1 = g2 & g2 is proper;
now
let v be Vertex of G1;
v in the_Vertices_of G1;
then v in the_Vertices_of G2 \/ V by GLIB_006:def 10;
then per cases by XBOOLE_0:def 3;
suppose v in the_Vertices_of G2;
then reconsider w = v as Vertex of G2;
v.edgesInOut() = w.edgesInOut() by GLIBPRE0:45;
hence g1 | v.edgesInOut() is one-to-one by A1;
end;
suppose not v in the_Vertices_of G2 & v in V;
then v in V \ the_Vertices_of G2 by XBOOLE_0:def 5;
then v.edgesInOut() = {} by GLIB_000:def 49, GLIB_006:88;
hence g1 | v.edgesInOut() is one-to-one;
end;
end;
hence thesis;
end;
theorem Th93:
for v,e,w being object, G1 being addEdge of G2,v,e,w
for g1 being EColoring of G1, g2 being EColoring of G2, x being object
st g1 = g2 +* (e .--> x) & not e in the_Edges_of G2 & not x in rng g2
holds g2 is proper implies g1 is proper
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
let g1 be EColoring of G1, g2 be EColoring of G2, x being object;
assume A1: g1 = g2 +* (e .--> x) & not e in the_Edges_of G2;
assume A2: not x in rng g2 & g2 is proper;
dom(e.-->x) = dom {[e,x]} by FUNCT_4:82
.= {e} by RELAT_1:9;
then e in dom(e.-->x) by TARSKI:def 1;
then e in dom g2 \/ dom(e.-->x) by XBOOLE_0:def 3;
then e in dom g1 by A1, FUNCT_4:def 1;
then A3: e in the_Edges_of G1;
A4: rng(e .--> x) = rng{[e,x]} by FUNCT_4:82
.= {x} by RELAT_1:9;
A5: v is Vertex of G2 & w is Vertex of G2
proof
assume not(v is Vertex of G2 & w is Vertex of G2);
then G1 == G2 by GLIB_006:def 11;
hence contradiction by A1, A3, GLIB_000:def 34;
end;
now
let u1 be Vertex of G1;
A6: g1 | u1.edgesInOut() = g2 | u1.edgesInOut()
+* (e .--> x) | u1.edgesInOut() by A1, FUNCT_4:71;
reconsider u2 = u1 as Vertex of G2 by A1, A5, GLIB_006:def 11;
per cases;
suppose u1 <> v & u1 <> w;
then A7: u1.edgesInOut() = u2.edgesInOut() by GLIBPRE0:46;
not e in u2.edgesInOut() by A1;
then (e .--> x) | u1.edgesInOut() = {} by A7, FUNCOP_1:76;
hence g1 | u1.edgesInOut() is one-to-one by A2, A6, A7;
end;
suppose A8: u1 = v or u1 = w;
A9: u1.edgesInOut() = u2.edgesInOut() \/ {e}
proof
per cases by A8;
suppose u1 = v & u1 <> w;
hence thesis by A1, A5, GLIBPRE0:47;
end;
suppose u1 <> v & u1 = w;
hence thesis by A1, A5, GLIBPRE0:48;
end;
suppose u1 = v & u1 = w;
hence thesis by A1, GLIBPRE0:49;
end;
end;
{e} misses the_Edges_of G2 by A1, ZFMISC_1:50;
then {e} misses dom g2 by PARTFUN1:def 2;
then A10: g2 | {e} = {} by RELAT_1:66;
A11: g2 | u1.edgesInOut()
= g2 | u2.edgesInOut() \/ g2 | {e} by A9, RELAT_1:78
.= g2 | u2.edgesInOut() by A10;
not e in u2.edgesInOut() by A1;
then A12: (e .--> x) | u2.edgesInOut() = {} by FUNCOP_1:76;
A13: (e .--> x) | u1.edgesInOut()
= (e .--> x) | u2.edgesInOut() \/ (e .--> x) | {e}
by A9, RELAT_1:78
.= e .--> x by A12;
rng g2 misses rng(e .--> x) by A2, A4, ZFMISC_1:50;
then A14: rng(g2 | u2.edgesInOut()) misses rng(e .--> x)
by RELAT_1:70, XBOOLE_1:63;
A15: g2 | u2.edgesInOut() is one-to-one by A2;
g1 | u1.edgesInOut() = g2 | u2.edgesInOut() +* (e .--> x)
by A6, A11, A13;
hence g1 | u1.edgesInOut() is one-to-one by A14, A15, FUNCT_4:92;
end;
end;
hence thesis;
end;
theorem Th94:
for v,e being object, w being Vertex of G2, G1 being addAdjVertex of G2,v,e,w
for g1 being EColoring of G1, g2 being EColoring of G2, 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
holds g2 is proper implies g1 is proper
proof
let v,e be object, w be Vertex of G2, G1 be addAdjVertex of G2,v,e,w;
let g1 be EColoring of G1, g2 be EColoring of G2, x be object;
assume that A1: g1 = g2 +* (e .--> x) & not x in rng g2 and
A2: not e in the_Edges_of G2 & not v in the_Vertices_of G2 and
A3: g2 is proper;
consider G9 being addVertex of G2,v such that
A4: G1 is addEdge of G9,v,e,w by A2, GLIB_006:126;
A5: the_Edges_of G9 = the_Edges_of G2 by GLIB_006:def 10;
then reconsider g9 = g2 as EColoring of G9;
g9 is proper by A3, Th92;
hence thesis by A1, A2, A4, A5, Th93;
end;
theorem
for v being Vertex of G2, e,w being object, G1 being addAdjVertex of G2,v,e,w
for g1 being EColoring of G1, g2 being EColoring of G2, 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
holds g2 is proper implies g1 is proper
proof
let v be Vertex of G2, e,w be object, G1 be addAdjVertex of G2,v,e,w;
let g1 be EColoring of G1, g2 be EColoring of G2, x be object;
assume that A1: g1 = g2 +* (e .--> x) & not x in rng g2 and
A2: not e in the_Edges_of G2 & not w in the_Vertices_of G2 and
A3: g2 is proper;
consider G9 being addVertex of G2,w such that
A4: G1 is addEdge of G9,v,e,w by A2, GLIB_006:125;
A5: the_Edges_of G9 = the_Edges_of G2 by GLIB_006:def 10;
then reconsider g9 = g2 as EColoring of G9;
g9 is proper by A3, Th92;
hence thesis by A1, A2, A4, A5, Th93;
end;
Lm8:
for X being set, x being object holds dom <: X --> x, id X :> = X
proof
let X be set, x be object;
thus dom <: X --> x, id X :> = dom(X --> x) /\ dom id X by FUNCT_3:def 7
.= X;
end;
Lm9:
for X being set, x, y being object st y in X
holds <: X --> x, id X :>.y = [x,y]
proof
let X be set, x,y be object;
assume A1: y in X;
then y in dom <: X --> x, id X :> by Lm8;
hence <: X --> x, id X :>.y = [(X --> x).y, (id X).y] by FUNCT_3:def 7
.= [x,(id X).y] by A1, FUNCOP_1:7
.= [x,y] by A1, FUNCT_1:18;
end;
Lm10:
for X being set, x being object holds rng <: X --> x, id X :> = [: {x}, X :]
proof
let X be set, x be object;
now
let y be object;
hereby
assume y in [: {x}, X :];
then consider x0, x9 being object such that
A1: x0 in {x} & x9 in X & y = [x0,x9] by ZFMISC_1:def 2;
take x9;
thus x9 in dom <: X --> x, id X :> by A1, Lm8;
thus y = [x,x9] by A1, TARSKI:def 1
.= <: X --> x, id X :>.x9 by A1, Lm9;
end;
given x9 being object such that
A2: x9 in dom <: X --> x, id X :> & y = <: X --> x, id X :>.x9;
A3: x9 in X by A2, Lm8;
then y = [x,x9] by A2, Lm9;
hence y in [: {x}, X :] by A3, ZFMISC_1:105;
end;
hence thesis by FUNCT_1:def 3;
end;
Lm11:
for X, Y being set holds Y misses rng <: X --> Y, id X :>
proof
let X, Y be set;
set h = <: X --> Y, id X :>;
now
given y being object such that
A1: y in Y & y in rng h;
consider x being object such that
A2: x in dom h & y = h.x by A1, FUNCT_1:def 3;
x in X by A2, Lm8;
then A3: y = [Y,x] by A2, Lm9
.= {{Y, x},{Y}} by TARSKI:def 5;
A4: {Y} in {{Y, x},{Y}} by TARSKI:def 2;
Y in {Y} by TARSKI:def 1;
hence contradiction by A1, A3, A4, XREGULAR:7;
end;
hence thesis by XBOOLE_0:3;
end;
theorem Th96:
for v being object, V being Subset of the_Vertices_of G2
for G1 being addAdjVertexAll of G2,v,V, g2 being EColoring of G2
for g1 being EColoring of G1, 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
let v be object, V be Subset of the_Vertices_of G2;
let G1 be addAdjVertexAll of G2,v,V, g2 be EColoring of G2;
let g1 be EColoring of G1, X, E be set;
set h = <: E-->X, id E :>;
assume A1: E = G1.edgesBetween(V,{v}) & rng g2 c= X;
assume A2: g1 = g2+*h & not v in the_Vertices_of G2 & g2 is proper;
consider E0 being set such that
A3: card V = card E0 & E0 misses the_Edges_of G2 and
A4: the_Edges_of G1 = the_Edges_of G2 \/ E0 and
A5: for v1 being object st v1 in V ex e1 being object st e1 in E0 &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A2, GLIB_007:def 4;
A6: E = E0 by A1, A2, A3, A4, GLIB_007:58;
A7: dom h = E by Lm8;
now
let w be Vertex of G1, e1,e2 be object;
assume A8: e1 in w.edgesInOut() & e2 in w.edgesInOut() & g1.e1=g1.e2;
consider u1 being Vertex of G1 such that
A9: e1 Joins w,u1,G1 by A8, GLIB_000:64;
consider u2 being Vertex of G1 such that
A10: e2 Joins w,u2,G1 by A8, GLIB_000:64;
per cases;
suppose A11: w <> v & not w in V;
then A12: not w in {v} & w in the_Vertices_of G1 by TARSKI:def 1;
the_Vertices_of G1 = the_Vertices_of G2 \/ {v} by A2, GLIB_007:def 4;
then reconsider w2 = w as Vertex of G2 by A12, XBOOLE_0:def 3;
A13: w.edgesInOut() = w2.edgesInOut() by A11, GLIBPRE0:56;
then not e1 in E & not e2 in E by A3, A6, A8, XBOOLE_0:3;
then g1.e1 = g2.e1 & g1.e2 = g2.e2 by A2, A7, FUNCT_4:11;
hence e1 = e2 by A2, A8, A13, Th85;
end;
suppose A14: w = v;
A15: e1 Joins u1,v,G1 & e2 Joins u2,v,G1
by A14, A9, A10, GLIB_000:14;
then A16: u1 in V & u2 in V by A2, GLIB_007:def 4;
v in {v} by TARSKI:def 1;
then e1 SJoins V,{v},G1 & e2 SJoins V,{v},G1
by A15, A16, GLIB_000:17;
then A17: e1 in E & e2 in E by A1, GLIB_000:def 30;
A18: g1.e1 = h.e1 by A2, A7, A17, FUNCT_4:13
.= [X,e1] by A17, Lm9;
g1.e2 = h.e2 by A2, A7, A17, FUNCT_4:13
.= [X,e2] by A17, Lm9;
hence e1 = e2 by A8, A18, XTUPLE_0:1;
end;
suppose A19: w <> v & w in V;
per cases;
suppose A20: e1 in E & e2 in E;
then e1 SJoins V,{v},G1 by A1, GLIB_000:def 30;
then consider x1 being object such that
A21: x1 in V & e1 Joins x1,v,G1 by GLIB_000:102;
e2 SJoins V,{v},G1 by A1, A20, GLIB_000:def 30;
then consider x2 being object such that
A22: x2 in V & e2 Joins x2,v,G1 by GLIB_000:102;
A23: u1 = v & u2 = v by A9, A10, A19, A21, A22, GLIB_000:15;
consider e9 being object such that
e9 in E0 & e9 Joins w,v,G1 and
A24: for e8 being object st e8 Joins w,v,G1 holds e8 = e9
by A5, A19;
e1 = e9 & e2 = e9 by A9, A10, A23, A24;
hence e1 = e2;
end;
suppose A25: e1 in E & not e2 in E;
then A26: g1.e1 = h.e1 & g1.e2 = g2.e2 by A2, A7, FUNCT_4:11, 13;
e2 in the_Edges_of G1 by A10, GLIB_000:def 13;
then e2 in the_Edges_of G2 by A4, A6, A25, XBOOLE_0:def 3;
then e2 in dom g2 by PARTFUN1:def 2;
then g1.e1 in rng h & g1.e2 in rng g2 by A7, A25, A26, FUNCT_1:3;
hence e1 = e2 by A1, A8, Lm11, XBOOLE_0:3; :: by contradiction
end;
suppose A27: not e1 in E & e2 in E;
then A28: g1.e1 = g2.e1 & g1.e2 = h.e2 by A2, A7, FUNCT_4:11, 13;
e1 in the_Edges_of G1 by A9, GLIB_000:def 13;
then e1 in the_Edges_of G2 by A4, A6, A27, XBOOLE_0:def 3;
then e1 in dom g2 by PARTFUN1:def 2;
then g1.e1 in rng g2 & g1.e2 in rng h by A7, A27, A28, FUNCT_1:3;
hence e1 = e2 by A1, A8, Lm11, XBOOLE_0:3; :: by contradiction
end;
suppose A29: not e1 in E & not e2 in E;
then A30: g1.e1 = g2.e1 & g1.e2 = g2.e2 by A2, A7, FUNCT_4:11;
e1 in the_Edges_of G2 & e2 in the_Edges_of G2
by A4, A6, A8, A29, XBOOLE_0:def 3;
then e1 Joins w,u1,G2 & e2 Joins w,u2,G2 by A9, A10, GLIB_006:72;
hence e1 = e2 by A2, A8, A30, Th86;
end;
end;
end;
hence thesis by Th85;
end;
theorem Th97:
for F being PGraphMapping of G1,G, 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
let F be PGraphMapping of G1, G, g9 be EColoring of G1;
assume A1: dom F_E = the_Edges_of G1 & F_E is one-to-one &
g9 = g*(F_E) & g is proper;
now
let v be Vertex of G1, e1, e2 be object;
assume A2: e1 in v.edgesInOut() & e2 in v.edgesInOut() & g9.e1 = g9.e2;
then A3: g9.e1 = g.(F_E.e1) & g9.e2 = g.(F_E.e2) by A1, FUNCT_1:13;
(the_Source_of G1).e1 = v or (the_Target_of G1).e1 = v by A2, GLIB_000:61;
then v in dom F_V by A1, A2, GLIB_010:5;
then A4: F_E.:(v.edgesInOut()) c= (F_V/.v).edgesInOut() by GLIBPRE0:80;
F_E.e1 in F_E.:(v.edgesInOut()) & F_E.e2 in F_E.:(v.edgesInOut())
by A1, A2, FUNCT_1:def 6;
then F_E.e1 in (F_V/.v).edgesInOut() & F_E.e2 in (F_V/.v).edgesInOut()
by A4;
then F_E.e1 = F_E.e2 by A1, A2, A3, Th85;
hence e1 = e2 by A1, A2, FUNCT_1:def 4;
end;
hence thesis by Th85;
end;
theorem Th98:
for F being PGraphMapping of G1,G, g9 being EColoring of G1
st F is weak_SG-embedding & g9 = g*(F_E) & g is proper holds g9 is proper
proof
let F be PGraphMapping of G1, G, g9 be EColoring of G1;
assume A1: F is weak_SG-embedding & g9 = g*(F_E) & g is proper;
then dom F_E = the_Edges_of G1 & F_E is one-to-one by GLIB_010:def 11;
hence thesis by A1, Th97;
end;
definition
let c, G;
attr G is c-ecolorable means
:Def6:
ex g being proper EColoring of G st card rng g c= c;
end;
theorem Th99:
c1 c= c2 & G is c1-ecolorable implies G is c2-ecolorable by XBOOLE_1:1;
theorem Th100:
G is G.size()-ecolorable
proof
reconsider g = id the_Edges_of G as proper EColoring of G;
card rng g = G.size();
hence thesis;
end;
theorem Th101:
G is edgeless iff G is 0-ecolorable
proof
hereby
assume G is edgeless;
then G.size() = 0;
hence G is 0-ecolorable by Th100;
end;
assume G is 0-ecolorable;
then consider g being proper EColoring of G such that
A1: card rng g c= 0;
card rng g = 0 by A1, XBOOLE_1:3;
then g = {};
then {} = dom g
.= the_Edges_of G by PARTFUN1:def 2;
hence thesis;
end;
registration
cluster edgeless -> 0-ecolorable for _Graph;
coherence by Th101;
cluster 0-ecolorable -> edgeless for _Graph;
coherence by Th101;
let c;
cluster c-edge -> c-ecolorable for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is c-edge;
reconsider g = id the_Edges_of G as EColoring of G;
card rng g = G.size()
.= c by A1, GLIB_013:def 4;
hence thesis;
end;
cluster c-ecolorable for _Graph;
existence
proof
take the c-edge _Graph;
thus thesis;
end;
end;
theorem Th102:
for H being Subgraph of G holds G is c-ecolorable implies H is c-ecolorable
proof
let H be Subgraph of G;
assume G is c-ecolorable;
then consider g1 being proper EColoring of G such that
A1: card rng g1 c= c;
reconsider g2 = g1 | the_Edges_of H as EColoring of H by Th78;
reconsider g2 as proper EColoring of H by Th89;
card rng g2 c= card rng g1 by RELAT_1:70, CARD_1:11;
hence thesis by A1, XBOOLE_1:1;
end;
registration
let c; let G be c-ecolorable _Graph;
cluster -> c-ecolorable for Subgraph of G;
coherence by Th102;
end;
theorem Th103:
G1 == G2 & G1 is c-ecolorable implies G2 is c-ecolorable
proof
assume A1: G1 == G2 & G1 is c-ecolorable;
then consider g1 being proper EColoring of G1 such that
A2: card rng g1 c= c;
the_Edges_of G1 = the_Edges_of G2 by A1, GLIB_000:def 34;
then reconsider g2 = g1 as EColoring of G2;
g2 is proper by A1, Th90;
hence thesis by A2;
end;
Lm12:
for G2 being reverseEdgeDirections of G1, E
holds G1 is c-ecolorable implies G2 is c-ecolorable
proof
let G2 be reverseEdgeDirections of G1, E;
assume G1 is c-ecolorable;
then consider g1 being proper EColoring of G1 such that
A1: card rng g1 c= c;
the_Edges_of G1 = the_Edges_of G2 by GLIB_007:4;
then reconsider g2 = g1 as EColoring of G2;
g2 is proper by Lm7;
hence thesis by A1;
end;
theorem Th104:
for G2 being reverseEdgeDirections of G1, E
holds G1 is c-ecolorable iff G2 is c-ecolorable
proof
let G2 be reverseEdgeDirections of G1, E;
thus G1 is c-ecolorable implies G2 is c-ecolorable by Lm12;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by Lm12;
end;
registration
let c; let G1 be c-ecolorable _Graph; let E;
cluster -> c-ecolorable for reverseEdgeDirections of G1, E;
coherence by Th104;
end;
theorem Th105:
for G1 being addVertices of G2, V
holds G1 is c-ecolorable iff G2 is c-ecolorable
proof
let G1 be addVertices of G2, V;
G2 is Subgraph of G1 by GLIB_006:57;
hence G1 is c-ecolorable implies G2 is c-ecolorable;
assume G2 is c-ecolorable;
then consider g2 being proper EColoring of G2 such that
A1: card rng g2 c= c;
the_Edges_of G1 = the_Edges_of G2 by GLIB_006:def 10;
then reconsider g1 = g2 as EColoring of G1;
g1 is proper by Th92;
hence thesis by A1;
end;
registration
let c; let G2 be c-ecolorable _Graph; let V;
cluster -> c-ecolorable for addVertices of G2, V;
coherence by Th105;
end;
theorem Th106:
for G2 being c-ecolorable _Graph, v,e,w being object
for G1 being addEdge of G2,v,e,w holds G1 is (c+`1)-ecolorable
proof
let G2 be c-ecolorable _Graph, v,e,w be object;
let G1 be addEdge of G2,v,e,w;
per cases;
suppose A1: v in the_Vertices_of G2 & w in the_Vertices_of G2 &
not e in the_Edges_of G2;
consider g2 being proper EColoring of G2 such that
A2: card rng g2 c= c by Def6;
set y = rng g2, g1 = g2 +* (e .--> y);
reconsider g1 as EColoring of G1 by A1, Th79;
A3: rng(e .--> y) = rng{[e,y]} by FUNCT_4:82
.= {y} by RELAT_1:9;
not y in rng g2;
then reconsider g1 as proper EColoring of G1 by A1, Th93;
A4: card rng g1 c= card(rng g2 \/ {y}) by A3, FUNCT_4:17, CARD_1:11;
not y in rng g2;
then card(rng g2\/{y}) = card rng g2 +` card {y} by CARD_2:35, ZFMISC_1:50
.= card rng g2 +` 1 by CARD_1:30;
then card(rng g2 \/ {y}) c= c +` 1 by A2, CARD_2:84;
hence thesis by A4, XBOOLE_1:1;
end;
suppose not(v in the_Vertices_of G2 & w in the_Vertices_of G2 &
not e in the_Edges_of G2);
then G1 == G2 by GLIB_006:def 11;
then G1 is c-ecolorable by Th103;
hence thesis by Th99, CARD_2:94;
end;
end;
theorem Th107:
for G2 being c-ecolorable _Graph, v,e,w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is (c+`1)-ecolorable
proof
let G2 be c-ecolorable _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
per cases;
suppose v in the_Vertices_of G2 & not w in the_Vertices_of G2 &
not e in the_Edges_of G2;
then consider G9 being addVertex of G2,w such that
A1: G1 is addEdge of G9,v,e,w by GLIB_006:125;
thus G1 is (c+`1)-ecolorable by A1, Th106;
end;
suppose not v in the_Vertices_of G2 & w in the_Vertices_of G2 &
not e in the_Edges_of G2;
then consider G9 being addVertex of G2,v such that
A2: G1 is addEdge of G9,v,e,w by GLIB_006:126;
thus G1 is (c+`1)-ecolorable by A2, Th106;
end;
suppose not((v in the_Vertices_of G2 & not w in the_Vertices_of G2 &
not e in the_Edges_of G2)or(not v in the_Vertices_of G2 &
w in the_Vertices_of G2 & not e in the_Edges_of G2));
then G1 == G2 by GLIB_006:def 12;
then G1 is c-ecolorable by Th103;
hence thesis by Th99, CARD_2:94;
end;
end;
Lm13:
for G2 being edgeless _Graph, v,e being object, 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
let G2 be edgeless _Graph, v,e be object, w being Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not v in the_Vertices_of G2;
set x = the object, g = the_Edges_of G1 --> x;
A2: dom g = the_Edges_of G1;
reconsider g as EColoring of G1;
the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, GLIB_006:def 12
.= {e};
then g is trivial by A2;
then reconsider g as proper EColoring of G1;
card rng g c= card {x} by FUNCOP_1:13, CARD_1:11;
then card rng g c= 1 by CARD_1:30;
hence thesis;
end;
theorem
for G2 being edgeless _Graph, v,e,w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 1-ecolorable
proof
let G2 be edgeless _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
per cases;
suppose not e in the_Edges_of G2 & not v in the_Vertices_of G2 &
w in the_Vertices_of G2;
hence thesis by Lm13;
end;
suppose A1: not e in the_Edges_of G2 & v in the_Vertices_of G2 &
not w in the_Vertices_of G2;
set G3 = the reverseEdgeDirections of G1, {e};
G3 is addAdjVertex of G2,w,e,v by A1, GLIBPRE1:66;
then G3 is 1-ecolorable by A1, Lm13;
hence thesis by Th104;
end;
suppose not((not e in the_Edges_of G2 & v in the_Vertices_of G2 &
not w in the_Vertices_of G2) or (not e in the_Edges_of G2 &
not v in the_Vertices_of G2 & w in the_Vertices_of G2));
then G1 == G2 by GLIB_006:def 12;
then G1 is edgeless by GLIB_008:52;
hence thesis by Th99, XBOOLE_1:2;
end;
end;
registration
let c; let G2 be c-ecolorable _Graph; let v,e,w be object;
cluster -> (c+`1)-ecolorable for addEdge of G2,v,e,w;
coherence by Th106;
cluster -> (c+`1)-ecolorable for addAdjVertex of G2,v,e,w;
coherence by Th107;
end;
theorem Th109:
for G2 being c-ecolorable _Graph, v being object
for G1 being addAdjVertexAll of G2,v,V holds G1 is (c+`card V)-ecolorable
proof
let G2 be c-ecolorable _Graph, v be object;
let G1 be addAdjVertexAll of G2,v,V;
per cases;
suppose A1: not v in the_Vertices_of G2 & V c= the_Vertices_of G2;
consider g2 being proper EColoring of G2 such that
A2: card rng g2 c= c by Def6;
consider E0 being set such that
A3: card V = card E0 & E0 misses the_Edges_of G2 and
A4: the_Edges_of G1 = the_Edges_of G2 \/ E0 and
for v1 being object st v1 in V ex e1 being object st e1 in E0 &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A1, GLIB_007:def 4;
:: construct the coloring
set E=G1.edgesBetween(V,{v}), h = <: E --> rng g2, id E :>, g1 = g2 +* h;
A5: E = E0 by A1, A3, A4, GLIB_007:58;
dom h = E by Lm8;
then reconsider g1 as EColoring of G1 by A1, Th82;
reconsider g1 as proper EColoring of G1 by A1, Th96;
:: count the colors
card rng g1 c= card(rng g2 \/ rng h) by FUNCT_4:17, CARD_1:11;
then A6: card rng g1 c= card rng g2 +` card rng h by Lm11, CARD_2:35;
card rng h = card [: {rng g2}, E :] by Lm10
.= card [: E, {rng g2} :] by CARD_2:4
.= card V by A3, A5, CARD_1:69;
then card rng g2 +` card rng h c= c +` card V by A2, CARD_2:84;
hence thesis by A6, XBOOLE_1:1;
end;
suppose not(not v in the_Vertices_of G2 & V c= the_Vertices_of G2);
then G1 == G2 by GLIB_007:def 4;
then G1 is c-ecolorable by Th103;
hence thesis by Th99, CARD_2:94;
end;
end;
registration
let c; let G2 be c-ecolorable _Graph; let v be object; let V;
cluster -> (c+`card V)-ecolorable for addAdjVertexAll of G2,v,V;
coherence by Th109;
end;
theorem Th110:
for F being PGraphMapping of G1, G2
st F is weak_SG-embedding & G2 is c-ecolorable holds G1 is c-ecolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is c-ecolorable;
then consider g2 being proper EColoring of G2 such that
A2: card rng g2 c= c;
reconsider g1 = g2*(F_E) as EColoring of G1 by A1, Th84;
A3: g1 is proper by A1, Th98;
card rng g1 c= card rng g2 by RELAT_1:26, CARD_1:11;
hence thesis by A2, A3, XBOOLE_1:1;
end;
theorem Th111:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is c-ecolorable iff G2 is c-ecolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
hence G1 is c-ecolorable implies G2 is c-ecolorable by Th110;
thus G2 is c-ecolorable implies G1 is c-ecolorable by A1, Th110;
end;
registration
let c; let G be c-ecolorable _Graph;
cluster G-isomorphic -> c-ecolorable for _Graph;
coherence
proof
let G2 be _Graph;
assume G2 is G-isomorphic;
then consider F being PGraphMapping of G, G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th111;
end;
end;
definition
let G;
attr G is finite-ecolorable means :: or finitely-ecolorable
:Def7:
ex n st G is n-ecolorable;
end;
registration
cluster edge-finite -> finite-ecolorable for _Graph;
coherence
proof
let G be _Graph;
assume A1: G is edge-finite;
G is G.size()-ecolorable by Th100;
hence thesis by A1;
end;
cluster edgeless -> finite-ecolorable for _Graph;
coherence;
cluster finite-ecolorable -> locally-finite for _Graph;
coherence
proof
let G be _Graph;
assume A2: G is finite-ecolorable;
now
let v be Vertex of G;
consider n such that
A3: G is n-ecolorable by A2;
consider g being proper EColoring of G such that
A4: card rng g c= n by A3;
A5: g | v.edgesInOut() is one-to-one by Def5;
rng(g | v.edgesInOut()) c= rng g by RELAT_1:70;
then card rng(g | v.edgesInOut()) c= card rng g by CARD_1:11;
then rng(g | v.edgesInOut()) is finite by A4;
then A6: dom(g | v.edgesInOut()) is finite by A5, CARD_1:59;
dom(g | v.edgesInOut()) = dom g /\ v.edgesInOut() by RELAT_1:61
.= the_Edges_of G /\ v.edgesInOut() by PARTFUN1:def 2
.= v.edgesInOut() by XBOOLE_1:28;
hence v.edgesInOut() is finite by A6;
end;
hence thesis by GLIB_013:def 5;
end;
let n;
cluster n-ecolorable -> finite-ecolorable for _Graph;
coherence;
end;
registration
cluster finite-ecolorable for _Graph;
existence
proof
take the edgeless _Graph;
thus thesis;
end;
cluster non finite-ecolorable for _Graph;
existence
proof
take the non locally-finite _Graph;
thus thesis;
end;
end;
registration
let G be finite-ecolorable _Graph;
cluster -> finite-ecolorable for Subgraph of G;
coherence
proof
let H be Subgraph of G;
consider n such that
A1: G is n-ecolorable by Def7;
thus thesis by A1;
end;
end;
theorem
G1 == G2 & G1 is finite-ecolorable implies G2 is finite-ecolorable
proof
assume A1: G1 == G2 & G1 is finite-ecolorable;
then consider n such that
A2: G1 is n-ecolorable;
G2 is n-ecolorable by A1, A2, Th103;
hence thesis;
end;
theorem Th113:
for G2 being reverseEdgeDirections of G1, E
holds G1 is finite-ecolorable iff G2 is finite-ecolorable
proof
let G2 be reverseEdgeDirections of G1, E;
thus G1 is finite-ecolorable implies G2 is finite-ecolorable;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis;
end;
registration
let G1 be finite-ecolorable _Graph; let E;
cluster -> finite-ecolorable for reverseEdgeDirections of G1, E;
coherence by Th113;
end;
registration
let G1 be non finite-ecolorable _Graph; let E;
cluster -> non finite-ecolorable for reverseEdgeDirections of G1, E;
coherence by Th113;
end;
theorem Th114:
for G1 being addVertices of G2, V
holds G1 is finite-ecolorable iff G2 is finite-ecolorable
proof
let G1 be addVertices of G2, V;
hereby
assume G1 is finite-ecolorable;
then consider n such that
A1: G1 is n-ecolorable;
G2 is n-ecolorable by A1, Th105;
hence G2 is finite-ecolorable;
end;
assume G2 is finite-ecolorable;
then consider n such that
A2: G2 is n-ecolorable;
thus thesis by A2;
end;
registration
let G2 be finite-ecolorable _Graph; let V;
cluster -> finite-ecolorable for addVertices of G2, V;
coherence by Th114;
end;
registration
let G2 be non finite-ecolorable _Graph; let V;
cluster -> non finite-ecolorable for addVertices of G2, V;
coherence by Th114;
end;
theorem Th115:
for v,e,w being object, G1 being addEdge of G2,v,e,w
holds G1 is finite-ecolorable iff G2 is finite-ecolorable
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
hereby
assume A1: G1 is finite-ecolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-ecolorable by A1;
end;
assume G2 is finite-ecolorable;
then consider n such that
A2: G2 is n-ecolorable;
G1 is (n+`1)-ecolorable by A2, Th107;
hence thesis;
end;
registration
let G2 be finite-ecolorable _Graph, v,e,w be object;
cluster -> finite-ecolorable for addEdge of G2,v,e,w;
coherence by Th115;
end;
registration
let G2 be non finite-ecolorable _Graph, v,e,w be object;
cluster -> non finite-ecolorable for addEdge of G2,v,e,w;
coherence by Th115;
end;
theorem Th116:
for v,e,w being object, G1 being addAdjVertex of G2,v,e,w
holds G1 is finite-ecolorable iff G2 is finite-ecolorable
proof
let v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
hereby
assume A1: G1 is finite-ecolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-ecolorable by A1;
end;
assume G2 is finite-ecolorable;
then consider n such that
A2: G2 is n-ecolorable;
reconsider G2 as n-ecolorable _Graph by A2;
G1 is addAdjVertex of G2,v,e,w;
hence thesis;
end;
registration
let G2 be finite-ecolorable _Graph, v,e,w be object;
cluster -> finite-ecolorable for addAdjVertex of G2,v,e,w;
coherence by Th116;
end;
registration
let G2 be non finite-ecolorable _Graph, v,e,w be object;
cluster -> non finite-ecolorable for addAdjVertex of G2,v,e,w;
coherence by Th116;
end;
theorem Th117:
for v being object, V being finite set, G1 being addAdjVertexAll of G2,v,V
holds G1 is finite-ecolorable iff G2 is finite-ecolorable
proof
let v be object, V be finite set, G1 be addAdjVertexAll of G2,v,V;
hereby
assume A1: G1 is finite-ecolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-ecolorable by A1;
end;
assume G2 is finite-ecolorable;
then consider n such that
A2: G2 is n-ecolorable;
reconsider G2 as n-ecolorable _Graph by A2;
G1 is addAdjVertexAll of G2,v,V;
hence thesis;
end;
registration
let G2 be finite-ecolorable _Graph, v be object; let V be finite set;
cluster -> finite-ecolorable for addAdjVertexAll of G2,v,V;
coherence by Th117;
end;
theorem Th118:
for F being PGraphMapping of G1,G2
st F is weak_SG-embedding & G2 is finite-ecolorable
holds G1 is finite-ecolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is finite-ecolorable;
then consider n such that
A2: G2 is n-ecolorable;
G1 is n-ecolorable by A1, A2, Th110;
hence thesis;
end;
theorem Th119:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is finite-ecolorable iff G2 is finite-ecolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
hence G1 is finite-ecolorable implies G2 is finite-ecolorable by Th118;
thus G2 is finite-ecolorable implies G1 is finite-ecolorable by A1, Th118;
end;
registration
let G be finite-ecolorable _Graph;
cluster G-isomorphic -> finite-ecolorable for _Graph;
coherence
proof
let G2 be _Graph;
assume G2 is G-isomorphic;
then consider F being PGraphMapping of G, G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th119;
end;
end;
deffunc EColSet(_Graph) =
{ c where c is cardinal Subset of $1.size() : $1 is c-ecolorable };
definition
let G;
func G.eChromaticNum() -> Cardinal equals :: chi prime
meet { c where c is cardinal Subset of G.size() : G is c-ecolorable };
coherence
proof
now
let a be set;
assume a in EColSet(G);
then consider c being cardinal Subset of G.size() such that
A1: a = c & G is c-ecolorable;
thus a is cardinal number by A1;
end;
hence thesis by GLIBPRE0:15;
end;
end;
Lm14:
G is G.eChromaticNum()-ecolorable
proof
G is G.size()-ecolorable & G.size() c= G.size() by Th100;
then A1: G.size() in EColSet(G);
now
let a be set;
assume a in EColSet(G);
then consider c being cardinal Subset of G.size() such that
A2: a = c & G is c-ecolorable;
thus a is cardinal number by A2;
end;
then consider c being Cardinal such that
A3: c in EColSet(G) & c = G.eChromaticNum() by A1, GLIBPRE0:14;
consider c9 being cardinal Subset of G.size() such that
A4: c = c9 & G is c9-ecolorable by A3;
thus thesis by A3, A4;
end;
theorem Th120:
G.eChromaticNum() c= G.size()
proof
G is G.size()-ecolorable & G.size() c= G.size() by Th100;
then G.size() in EColSet(G);
hence G.eChromaticNum() c= G.size() by SETFAM_1:3;
end;
theorem Th121:
G is edgeless iff G.eChromaticNum() = 0
proof
hereby
assume G is edgeless;
then G.size() = 0;
hence G.eChromaticNum() = 0 by Th120, XBOOLE_1:3;
end;
assume G.eChromaticNum() = 0;
then G is 0-ecolorable by Lm14;
hence thesis;
end;
registration
let G be edgeless _Graph;
cluster G.eChromaticNum() -> zero;
coherence by Th121;
end;
registration
let G be non edgeless _Graph;
cluster G.eChromaticNum() -> non zero;
coherence by Th121;
end;
Lm15:
G is c-ecolorable implies G.eChromaticNum() c= c
proof
assume A1: G is c-ecolorable;
per cases;
suppose not G.size() in c;
then c c= G.size() by ORDINAL1:16;
then c in EColSet(G) by A1;
hence thesis by SETFAM_1:3;
end;
suppose G.size() in c;
then G.eChromaticNum() in c by Th120, ORDINAL1:12;
hence thesis by ORDINAL1:def 2;
end;
end;
theorem Th122:
(G is c-ecolorable & for d being Cardinal st G is d-ecolorable holds c c= d)
iff G.eChromaticNum() = c
proof
G is G.size()-ecolorable & G.size() c= G.size() by Th100;
then A1: G.size() in EColSet(G);
hereby
assume G is c-ecolorable;
then A2: G.eChromaticNum() c= c by Lm15;
assume A3: for d being Cardinal st G is d-ecolorable holds c c= d;
now
let x be set;
assume x in EColSet(G);
then consider d being cardinal Subset of G.size() such that
A4: x = d & G is d-ecolorable;
thus c c= x by A3, A4;
end;
then c c= G.eChromaticNum() by A1, SETFAM_1:5;
hence G.eChromaticNum() = c by A2, XBOOLE_0:def 10;
end;
thus thesis by Lm14, Lm15;
end;
registration
let G be finite-ecolorable _Graph;
cluster G.eChromaticNum() -> natural;
coherence
proof
consider n such that
A1: G is n-ecolorable by Def7;
G.eChromaticNum() c= n by A1, Lm15;
hence thesis;
end;
end;
definition
let G be finite-ecolorable _Graph;
redefine func G.eChromaticNum() -> Nat; :: redefines .eChromaticNum() (GLCOLO00, definition)
coherence;
end;
theorem Th123:
for G being loopless _Graph holds G.supDegree() c= G.eChromaticNum()
proof
let G be loopless _Graph;
G is G.eChromaticNum()-ecolorable by Lm14;
then consider g being proper EColoring of G such that
A1: card rng g c= G.eChromaticNum();
set D = the set of all v.degree() where v is Vertex of G;
now
let x be object;
assume x in G.supDegree();
then x in union D by GLIB_013:def 6;
then consider d being set such that
A2: x in d & d in D by TARSKI:def 4;
consider v being Vertex of G such that
A3: d = v.degree() by A2;
card rng(g|v.edgesInOut()) c= card rng g by RELAT_1:70, CARD_1:11;
then A4: card rng(g|v.edgesInOut()) c= G.eChromaticNum() by A1, XBOOLE_1:1;
g|v.edgesInOut() is one-to-one by Def5;
then card rng(g|v.edgesInOut()) = card dom(g|v.edgesInOut()) by CARD_1:70
.= card(dom g /\ v.edgesInOut()) by RELAT_1:61
.= card(the_Edges_of G /\ v.edgesInOut()) by PARTFUN1:def 2
.= card v.edgesInOut() by XBOOLE_1:28
.= d by A3, GLIB_000:19;
hence x in G.eChromaticNum() by A2, A4;
end;
hence thesis by TARSKI:def 3;
end;
theorem
G1 == G2 implies G1.eChromaticNum() = G2.eChromaticNum()
proof
assume A1: G1 == G2;
then A2: G2 is G1.eChromaticNum()-ecolorable by Lm14, Th103;
for c st G2 is c-ecolorable holds G1.eChromaticNum() c= c by A1, Th103, Lm15;
hence thesis by A2, Th122;
end;
theorem Th125:
for G2 being reverseEdgeDirections of G1, E
holds G1.eChromaticNum() = G2.eChromaticNum()
proof
let G2 be reverseEdgeDirections of G1, E;
A1: G1 is G1.eChromaticNum()-ecolorable by Lm14;
for c st G2 is c-ecolorable holds G1.eChromaticNum() c= c by Th104, Lm15;
hence thesis by A1, Th122;
end;
theorem
for H being Subgraph of G holds H.eChromaticNum() c= G.eChromaticNum()
proof
let H be Subgraph of G;
G is G.eChromaticNum()-ecolorable by Lm14;
hence thesis by Lm15;
end;
theorem
for G1 being addVertices of G2, V
holds G1.eChromaticNum() = G2.eChromaticNum()
proof
let G1 be addVertices of G2, V;
A1: G1 is G1.eChromaticNum()-ecolorable by Lm14;
for c st G2 is c-ecolorable holds G1.eChromaticNum() c= c by Lm15;
hence thesis by A1, Th105, Th122;
end;
theorem
for v,e,w being object, G1 being addEdge of G2,v,e,w
holds G1.eChromaticNum() c= G2.eChromaticNum() +` 1
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
G2 is G2.eChromaticNum()-ecolorable by Lm14;
hence thesis by Th106, Lm15;
end;
theorem
for v,e,w being object, G1 being addAdjVertex of G2,v,e,w
holds G1.eChromaticNum() c= G2.eChromaticNum() +` 1
proof
let v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
G2 is G2.eChromaticNum()-ecolorable by Lm14;
hence thesis by Th107, Lm15;
end;
theorem Th130:
for G2 being edgeless _Graph, v being Vertex of G2, 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
let G2 be edgeless _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not w in the_Vertices_of G2;
now
let c;
assume A2: G1 is c-ecolorable;
assume not 1 c= c;
then c in {0} by CARD_1:49, ORDINAL1:16;
then A3: c = 0 by TARSKI:def 1;
e in the_Edges_of G2 \/ {e} by TARSKI:def 1;
then e in the_Edges_of G1 by A1, GLIB_006:def 12;
hence contradiction by A2, A3;
end;
hence thesis by Th122;
end;
theorem
for G2 being edgeless _Graph, v,e being object, 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
let G2 be edgeless _Graph, v, e be object, w be Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not v in the_Vertices_of G2;
set G3 = the reverseEdgeDirections of G1, {e};
not e in the_Edges_of G2;
then G3 is addAdjVertex of G2,w,e,v by GLIBPRE1:66;
then G3.eChromaticNum() = 1 by A1, Th130;
hence thesis by Th125;
end;
theorem
for v being object, G1 being addAdjVertexAll of G2,v,V
holds G1.eChromaticNum() c= G2.eChromaticNum() +` card V
proof
let v be object, G1 be addAdjVertexAll of G2,v,V;
G2 is G2.eChromaticNum()-ecolorable by Lm14;
hence thesis by Lm15;
end;
theorem Th133:
for F being PGraphMapping of G1, G2 st F is weak_SG-embedding
holds G1.eChromaticNum() c= G2.eChromaticNum()
proof
let F be PGraphMapping of G1, G2;
assume F is weak_SG-embedding;
then G1 is G2.eChromaticNum()-ecolorable by Th110, Lm14;
hence thesis by Lm15;
end;
theorem Th134:
for F being PGraphMapping of G1, G2 st F is isomorphism
holds G1.eChromaticNum() = G2.eChromaticNum()
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
then A2: G2.eChromaticNum() c= G1.eChromaticNum() by Th133;
G1.eChromaticNum() c= G2.eChromaticNum() by A1, Th133;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem
for G2 being G1-isomorphic _Graph
holds G1.eChromaticNum() = G2.eChromaticNum()
proof
let G2 be G1-isomorphic _Graph;
consider F be PGraphMapping of G1, G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th134;
end;
theorem
G is _trivial implies G.eChromaticNum() = G.size()
proof
assume A1: G is _trivial;
now
let c;
assume G is c-ecolorable;
then consider g being proper EColoring of G such that
A2: card rng g c= c;
set v = the Vertex of G;
g | v.edgesInOut() = g | the_Edges_of G by A1, GLIB_000:148
.= g;
then g is one-to-one by Def5;
then card rng g = card dom g by CARD_1:70
.= G.size() by PARTFUN1:def 2;
hence G.size() c= c by A2;
end;
hence thesis by Th100, Th122;
end;
begin :: Total Colorings
definition
let G;
mode TColoring of G means
:Def9:
ex f being VColoring of G, g being EColoring of G st it = [f,g];
existence
proof
set f = the VColoring of G, g = the EColoring of G;
take [f,g],f,g;
thus thesis;
end;
end;
registration
let G;
cluster -> pair for TColoring of G;
coherence
proof
let t be TColoring of G;
consider f being VColoring of G, g being EColoring of G such that
A1: t = [f,g] by Def9;
thus thesis by A1;
end;
end;
reserve t for TColoring of G;
notation
let G, t;
synonym t_V for t`1;
synonym t_E for t`2;
end;
registration
let G, t;
reduce [ t_V , t_E ] to t;
reducibility;
end;
definition
let G, t;
redefine func t_V -> VColoring of G; :: redefines _V (GLCOLO00, synonym) → `1 (XTUPLE_0, definition)
coherence
proof
consider f being VColoring of G, g being EColoring of G such that
A1: t = [f,g] by Def9;
thus thesis by A1;
end;
redefine func t_E -> EColoring of G; :: redefines _E (GLCOLO00, synonym) → `2 (XTUPLE_0, definition)
coherence
proof
consider f being VColoring of G, g being EColoring of G such that
A2: t = [f,g] by Def9;
thus thesis by A2;
end;
end;
definition
let G, f, g;
redefine func [f, g] -> TColoring of G; :: redefines [ (TARSKI, definition)
coherence by Def9;
end;
theorem Th137:
G is edgeless implies [f, {}] is TColoring of G
proof
assume A1: G is edgeless;
reconsider g = id the_Edges_of G as EColoring of G;
g = {} by A1;
hence thesis by Def9;
end;
theorem Th138:
for H being Subgraph of G holds
[ t_V | the_Vertices_of H , t_E | the_Edges_of H ] is TColoring of H
proof
let H be Subgraph of G;
A1: t_V | the_Vertices_of H is VColoring of H by Th3;
t_E | the_Edges_of H is EColoring of H by Th78;
hence thesis by A1, Def9;
end;
theorem Th139:
for G1 being addVertices of G2, V, 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
let G1 be addVertices of G2, V, t be TColoring of G2, h be Function;
assume dom h = V \ the_Vertices_of G2;
then A1: t_V +* h is VColoring of G1 by Th4;
the_Edges_of G1 = the_Edges_of G2 by GLIB_006:def 10;
hence thesis by A1, Def9;
end;
theorem Th140:
for v,x being object, G1 being addVertex of G2,v, t being TColoring of G2
holds [t_V +* (v .--> x), t_E] is TColoring of G1
proof
let v,x be object, G1 be addVertex of G2,v, t be TColoring of G2;
A1: dom(v .--> x) = dom{[v,x]} by FUNCT_4:82
.= {v} by RELAT_1:9;
dom(t_V +* (v .--> x)) = dom t_V \/ dom(v .--> x) by FUNCT_4:def 1
.= the_Vertices_of G2 \/ {v} by A1, PARTFUN1:def 2
.= the_Vertices_of G1 by GLIB_006:def 10;
then A2: t_V+*(v.-->x) is VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
the_Edges_of G1 = the_Edges_of G2 by GLIB_006:def 10;
hence thesis by A2, Def9;
end;
theorem Th141:
for e being object, v,w being Vertex of G2, G1 being addEdge of G2,v,e,w
for t being TColoring of G2, y being object st not e in the_Edges_of G2
holds [t_V, t_E +* (e .--> y)] is TColoring of G1
proof
let e be object, v,w be Vertex of G2, G1 be addEdge of G2,v,e,w;
let t be TColoring of G2, y be object;
assume not e in the_Edges_of G2;
then A1: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 \/ {e} by GLIB_006:def 11;
dom(t_E +* (e .--> y)) = dom t_E \/ dom(e .--> y) by FUNCT_4:def 1
.= the_Edges_of G2 \/ dom(e .--> y) by PARTFUN1:def 2
.= the_Edges_of G2 \/ dom{[e,y]} by FUNCT_4:82
.= the_Edges_of G1 by A1, RELAT_1:9;
then t_E +* (e .--> y) is EColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
hence thesis by A1, Def9;
end;
theorem Th142:
for e being object, v,w,u being Vertex of G2, G1 being addEdge of G2,v,e,w
for t being TColoring of G2, 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
let e be object, v,w,u be Vertex of G2, G1 be addEdge of G2,v,e,w;
let t be TColoring of G2, x,y be object;
assume not e in the_Edges_of G2;
then reconsider t9 = [t_V, t_E +* (e .--> y)] as TColoring of G1 by Th141;
A1: u is Vertex of G1 by GLIB_006:68;
dom(t_V +* (u .--> x)) = dom t9_V \/ dom(u .--> x) by FUNCT_4:def 1
.= the_Vertices_of G1 \/ dom(u .--> x) by PARTFUN1:def 2
.= the_Vertices_of G1 \/ dom{[u,x]} by FUNCT_4:82
.= the_Vertices_of G1 \/ {u} by RELAT_1:9
.= the_Vertices_of G1 by A1, ZFMISC_1:40;
then t9_V +* (u .--> x) is VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;
then [t9_V +* (u .--> x), t9_E] is TColoring of G1 by Def9;
hence thesis;
end;
theorem Th143:
for v,e being object, w being Vertex of G2, G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2, 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
let v,e be object, w be Vertex of G2, G1 be addAdjVertex of G2,v,e,w;
let t be TColoring of G2, x,y be object;
assume A1: not e in the_Edges_of G2 & not v in the_Vertices_of G2;
then consider G3 being addVertex of G2,v such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:126;
reconsider t3 = [t_V +* (v .--> x), t_E] as TColoring of G3 by Th140;
A3: v is Vertex of G3 & w is Vertex of G3 by GLIB_006:68, GLIB_006:94;
not e in the_Edges_of G3 by A1, GLIB_006:def 10;
then [t3_V, t3_E +* (e .--> y)] is TColoring of G1 by A2, A3, Th141;
hence thesis;
end;
theorem Th144:
for v being Vertex of G2, e,w being object, G1 being addAdjVertex of G2,v,e,w
for t being TColoring of G2, 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
let v be Vertex of G2, e,w be object, G1 be addAdjVertex of G2,v,e,w;
let t be TColoring of G2, x,y be object;
assume A1: not e in the_Edges_of G2 & not w in the_Vertices_of G2;
then consider G3 being addVertex of G2,w such that
A2: G1 is addEdge of G3,v,e,w by GLIB_006:125;
reconsider t3 = [t_V +* (w .--> x), t_E] as TColoring of G3 by Th140;
A3: v is Vertex of G3 & w is Vertex of G3 by GLIB_006:68, GLIB_006:94;
not e in the_Edges_of G3 by A1, GLIB_006:def 10;
then [t3_V, t3_E +* (e .--> y)] is TColoring of G1 by A2, A3, Th141;
hence thesis;
end;
theorem Th145:
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
let F be PGraphMapping of G1,G;
assume A1: F is total;
then A2: t_V*(F_V) is VColoring of G1 by Th9;
t_E*(F_E) is EColoring of G1 by A1, Th84;
hence thesis by A2, Def9;
end;
definition
let G, t;
attr t is proper means
:Def10:
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;
theorem Th146:
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
hereby
assume A1: t is proper;
hence t_V is proper & t_E is proper;
let e,v,w be object;
assume A2: e Joins v,w,G;
then reconsider u = v as Vertex of G by GLIB_000:13;
A3: e in u.edgesInOut() by A2, GLIB_000:62;
then e in the_Edges_of G;
then e in dom(t_E) by PARTFUN1:def 2;
then t_E.e in t_E.:u.edgesInOut() by A3, FUNCT_1:def 6;
hence t_V.v <> t_E.e by A1;
end;
assume A4: 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;
hence t_V is proper & t_E is proper;
let v be Vertex of G;
assume t_V.v in t_E.:v.edgesInOut();
then consider e being object such that
A5: e in dom t_E & e in v.edgesInOut() & t_V.v = t_E.e by FUNCT_1:def 6;
consider w being Vertex of G such that
A6: e Joins v,w,G by A5, GLIB_000:64;
thus contradiction by A4, A5, A6;
end;
theorem Th147:
t_V is proper & t_E is proper & rng(t_V) misses rng(t_E) implies t is proper
proof
assume A1: t_V is proper & t_E is proper & rng(t_V) misses rng(t_E);
now
let e,v,w be object;
assume e Joins v,w,G;
then e in the_Edges_of G & v in the_Vertices_of G by GLIB_000:def 13, 13;
then e in dom(t_E) & v in dom(t_V) by PARTFUN1:def 2;
then t_E.e in rng(t_E) & t_V.v in rng(t_V) by FUNCT_1:3;
hence t_V.v <> t_E.e by A1, XBOOLE_0:3;
end;
hence thesis by A1, Th146;
end;
theorem Th148:
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
thus t is proper implies 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)
by Th10, Th86, Th146;
assume A1: 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);
for e,v,w being object st e Joins v,w,G holds t_V.v <> t_V.w by A1;
then A2: t_V is proper by Th10;
for e1,e2,v,w1,w2 be object st e1 Joins v,w1,G & e2 Joins v,w2,G
& t_E.e1 = t_E.e2 holds e1 = e2 by A1;
then A3: t_E is proper by Th86;
for e,v,w being object st e Joins v,w,G holds t_V.v <> t_E.e by A1;
hence thesis by A2, A3, Th146;
end;
theorem Th149:
g is proper implies ex g9 being proper EColoring of G
st rng f misses rng g9 & card rng g = card rng g9
proof
assume A1: g is proper;
set h = <: rng g --> rng f, id rng g :>, g9 = h*g;
A2: dom h = rng g by Lm8;
then reconsider g9 as EColoring of G by Th77;
reconsider g9 as proper EColoring of G by A1, Th87;
take g9;
A3: rng g9 = rng h by A2, RELAT_1:28;
hence rng f misses rng g9 by Lm11;
thus card rng g = card [: rng g, {rng f} :] by CARD_1:69
.= card [: {rng f}, rng g :] by CARD_2:4
.= card rng g9 by A3, Lm10;
end;
theorem Th150:
f is proper implies ex f9 being VColoring of G
st f9 is proper & rng f9 misses rng g & card rng f = card rng f9
proof
assume A1: f is proper;
set h = <: rng f --> rng g, id rng f :>, f9 = h*f;
A2: dom h = rng f by Lm8;
then reconsider f9 as VColoring of G by Th1;
take f9;
thus f9 is proper by A1, A2, Th12;
A3: rng f9 = rng h by A2, RELAT_1:28;
hence rng f9 misses rng g by Lm11;
thus card rng f = card [: rng f, {rng g} :] by CARD_1:69
.= card [: {rng g}, rng f :] by CARD_2:4
.= card rng f9 by A3, Lm10;
end;
registration
let G be loopless _Graph;
cluster proper for TColoring of G;
existence
proof
set f = the proper VColoring of G, g9 = the proper EColoring of G;
consider g being proper EColoring of G such that
A1: rng f misses rng g & card rng g9 = card rng g by Th149;
reconsider t = [f,g] as TColoring of G;
take t;
thus thesis by A1, Th147;
end;
end;
registration
let G be loopless _Graph;
let t be proper TColoring of G;
cluster t_V -> proper for VColoring of G;
coherence by Def10;
cluster t_E -> proper for EColoring of G;
coherence by Def10;
end;
theorem Th151:
for H being Subgraph of G, 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
let H be Subgraph of G, t9 be TColoring of H;
assume A1: t9 = [t_V|the_Vertices_of H, t_E|the_Edges_of H] & t is proper;
then A2: t9_V is proper by Th15;
A3: t9_E is proper by A1, Th89;
now
let e,v,w be object;
assume A4: e Joins v,w,H;
then e in the_Edges_of H & v in the_Vertices_of H by GLIB_000:def 13, 13;
then A5: e in dom(t9_E) & v in dom(t9_V) by PARTFUN1:def 2;
v is set & w is set by TARSKI:1;
then e Joins v,w,G by A4, GLIB_000:72;
then A6: t_V.v <> t_E.e by A1, Th146;
t_V.v = t9_V.v & t_E.e = t9_E.e by A1, A5, FUNCT_1:47;
hence t9_V.v <> t9_E.e by A6;
end;
hence thesis by A2, A3, Th146;
end;
theorem Th152:
for t1 being TColoring of G1, t2 being TColoring of G2
st G1 == G2 & t1 = t2 & t1 is proper holds t2 is proper
proof
let t1 be TColoring of G1, t2 be TColoring of G2;
assume A1: G1 == G2 & t1 = t2 & t1 is proper;
then A2: t2_V is proper by Th16;
A3: t2_E is proper by A1, Th90;
now
let e,v,w be object;
assume e Joins v,w,G2;
then e Joins v,w,G1 by A1, GLIB_000:88;
hence t2_V.v <> t2_E.e by A1, Th146;
end;
hence thesis by A2, A3, Th146;
end;
Lm16:
for G2 being reverseEdgeDirections of G1, E
for t1 being TColoring of G1, t2 being TColoring of G2
st t1 = t2 & t1 is proper holds t2 is proper
proof
let G2 be reverseEdgeDirections of G1, E;
let t1 be TColoring of G1, t2 be TColoring of G2;
assume A1: t1 = t2 & t1 is proper;
then A2: t2_V is proper by Th18;
A3: t2_E is proper by A1, Th91;
now
let e,v,w be object;
assume e Joins v,w,G2;
then e Joins v,w,G1 by GLIB_007:9;
hence t2_V.v <> t2_E.e by A1, Th146;
end;
hence thesis by A2, A3, Th146;
end;
theorem Th153:
for G2 being reverseEdgeDirections of G1, E
for t1 being TColoring of G1, t2 being TColoring of G2
st t1 = t2 holds t1 is proper iff t2 is proper
proof
let G2 be reverseEdgeDirections of G1, E;
let t1 be TColoring of G1, t2 be TColoring of G2;
assume A1: t1 = t2;
hence t1 is proper implies t2 is proper by Lm16;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by A1, Lm16;
end;
theorem Th154:
for G1 being addVertices of G2, V
for t1 being TColoring of G1, t2 being TColoring of G2, 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
let G1 be addVertices of G2, V;
let t1 be TColoring of G1, t2 be TColoring of G2, h be Function;
assume that A1: dom h = V \ the_Vertices_of G2 and
A2: t1_V = t2_V +* h & t1_E = t2_E & t2 is proper;
A3: t1_V is proper & t1_E is proper by A1, A2, Th19, Th92;
now
let v be Vertex of G1;
per cases;
suppose A4: v in the_Vertices_of G2;
then reconsider v2 = v as Vertex of G2;
A5: t1_E.:v.edgesInOut() = t2_E.:v2.edgesInOut() by A2, GLIBPRE0:45;
not v in dom h by A1, A4, XBOOLE_0:def 5;
then t1_V.v = t2_V.v2 by A2, FUNCT_4:11;
hence not t1_V.v in t1_E.:v.edgesInOut() by A2, A5;
end;
suppose A6: not v in the_Vertices_of G2;
the_Vertices_of G1 = the_Vertices_of G2 \/ V by GLIB_006:def 10;
then v in V by A6, XBOOLE_0:def 3;
then v in V \ the_Vertices_of G2 by A6, XBOOLE_0:def 5;
then v.edgesInOut() = {} by GLIB_006:88, GLIB_000:def 49;
hence not t1_V.v in t1_E.:v.edgesInOut();
end;
end;
hence thesis by A3;
end;
theorem Th155:
for y,e being object, v,w being Vertex of G2, G1 being addEdge of G2,v,e,w
for t1 being TColoring of G1, 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
let y,e be object, v,w be Vertex of G2, G1 be addEdge of G2,v,e,w;
let t1 be TColoring of G1, t2 be TColoring of G2;
assume that A1: not e in the_Edges_of G2 & v,w are_adjacent and
A2: t1_V = t2_V & t1_E = t2_E +* (e .--> y) and
A3: not y in (rng t2_V)\/rng t2_E & t2 is proper;
A4: t1_V is proper by A1, A2, A3, Th20;
rng t2_E c= (rng t2_V)\/rng t2_E by XBOOLE_1:7;
then not y in rng t2_E by A3;
then A5: t1_E is proper by A1, A2, A3, Th93;
now
let e9,v9,w9 be object;
assume A6: e9 Joins v9,w9,G1;
then per cases by GLIB_006:72;
suppose A7: e9 Joins v9,w9,G2;
then A8: t2_V.v9 <> t2_E.e9 by A3, Th146;
e9 in the_Edges_of G2 by A7, GLIB_000:def 13;
then not e9 in dom(e.-->y) by A1, TARSKI:def 1;
hence t1_V.v9 <> t1_E.e9 by A2, A8, FUNCT_4:11;
end;
suppose not e9 in the_Edges_of G2;
then e9 = e by A1, A6, GLIB_006:106;
then A9: t1_E.e9 = y by A2, FUNCT_4:113;
v9 in the_Vertices_of G1 by A6, GLIB_000:13;
then v9 in dom t1_V by PARTFUN1:def 2;
then t1_V.v9 in rng t2_V by A2, FUNCT_1:3;
hence t1_V.v9 <> t1_E.e9 by A3, A9, XBOOLE_0:def 3;
end;
end;
hence thesis by A4, A5, Th146;
end;
theorem Th156:
for v,e being object, w being Vertex of G2, G1 being addEdge of G2,v,e,w
for t1 being TColoring of G1, t2 being TColoring of G2, 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
let v,e be object, w being Vertex of G2, G1 be addEdge of G2,v,e,w;
let t1 be TColoring of G1, t2 be TColoring of G2, x,y be object;
assume that A1: not e in the_Edges_of G2 & v <> w and
A2: t1_V = t2_V +* (v .--> x) & t1_E = t2_E +* (e .--> y) and
A3: {x,y} misses (rng t2_V)\/rng t2_E & x <> y & t2 is proper;
A4: dom(v.-->x) = dom {[v,x]} by FUNCT_4:82
.= {v} by RELAT_1:9;
A5: v in the_Vertices_of G2
proof
per cases;
suppose G1 != G2;
hence thesis by GLIB_006:def 11;
end;
suppose A6: G1 == G2;
v in dom(v.-->x) by A4, TARSKI:def 1;
then v in (dom t2_V)\/dom(v.-->x) by XBOOLE_0:def 3;
then v in dom t1_V by A2, FUNCT_4:def 1;
then v in the_Vertices_of G1;
hence thesis by A6, GLIB_000:def 34;
end;
end;
{x,y} misses rng t2_V by A3, XBOOLE_1:7, XBOOLE_1:63;
then A7: t1_V is proper by A1, A2, A3, A5, Th21, ZFMISC_1:49;
{x,y} misses rng t2_E by A3, XBOOLE_1:7, XBOOLE_1:63;
then not y in rng t2_E by ZFMISC_1:49;
then A8: t1_E is proper by A1, A2, A3, Th93;
now
let e9,v9,w9 be object;
assume A9: e9 Joins v9,w9,G1;
then per cases by GLIB_006:72;
suppose A10: e9 Joins v9,w9,G2;
then A11: e9 in the_Edges_of G2 by GLIB_000:def 13;
then not e9 in dom(e.-->y) by A1, TARSKI:def 1;
then A12: t1_E.e9 = t2_E.e9 by A2, FUNCT_4:11;
per cases;
suppose v9 = v;
then A13: t1_V.v9 = x by A2, FUNCT_4:113;
e9 in dom t2_E by A11, PARTFUN1:def 2;
then t2_E.e9 in rng t2_E by FUNCT_1:3;
then t1_E.e9 in (rng t2_V)\/rng t2_E by A12, XBOOLE_0:def 3;
hence t1_V.v9 <> t1_E.e9 by A3, A13, ZFMISC_1:49;
end;
suppose v9 <> v;
then not v9 in dom(v.-->x) by TARSKI:def 1;
then t1_V.v9 = t2_V.v9 by A2, FUNCT_4:11;
hence t1_V.v9 <> t1_E.e9 by A3, A10, A12, Th146;
end;
end;
suppose not e9 in the_Edges_of G2;
then e9 = e by A1, A5, A9, GLIB_006:106;
then A14: t1_E.e9 = y by A2, FUNCT_4:113;
per cases;
suppose v9 = v;
hence t1_V.v9 <> t1_E.e9 by A2, A3, A14, FUNCT_4:113;
end;
suppose v9 <> v;
then not v9 in dom(v.-->x) by TARSKI:def 1;
then A15: t1_V.v9 = t2_V.v9 by A2, FUNCT_4:11;
v9 in the_Vertices_of G1 by A9, GLIB_000:13;
then v9 in the_Vertices_of G2 by A5, GLIB_006:102;
then v9 in dom t2_V by PARTFUN1:def 2;
then t1_V.v9 in rng t2_V by A15, FUNCT_1:3;
then t1_V.v9 in (rng t2_V)\/rng t2_E by XBOOLE_0:def 3;
hence t1_V.v9 <> t1_E.e9 by A3, A14, ZFMISC_1:49;
end;
end;
end;
hence thesis by A7, A8, Th146;
end;
theorem
for v being Vertex of G2, e,w being object, G1 being addEdge of G2,v,e,w
for t1 being TColoring of G1, t2 being TColoring of G2, 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
let v be Vertex of G2, e,w be object, G1 be addEdge of G2,v,e,w;
let t1 be TColoring of G1, t2 be TColoring of G2, x,y be object;
assume that A1: not e in the_Edges_of G2 & v <> w and
A2: t1_V = t2_V +* (w .--> x) & t1_E = t2_E +* (e .--> y) and
A3: {x,y} misses (rng t2_V)\/rng t2_E & x <> y & t2 is proper;
set G3 = the reverseEdgeDirections of G1, {e};
A4: G3 is addEdge of G2,w,e,v by A1, GLIBPRE1:65;
the_Vertices_of G1 = the_Vertices_of G3 by GLIB_007:4;
then reconsider f3 = t1_V as VColoring of G3;
the_Edges_of G1 = the_Edges_of G3 by GLIB_007:4;
then reconsider g3 = t1_E as EColoring of G3;
reconsider t3 = [f3,g3] as TColoring of G3;
t3 is proper by A1, A2, A3, A4, Th156;
hence thesis by Th153;
end;
theorem Th158:
for v,e being object, w being Vertex of G2, G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1, t2 being TColoring of G2, 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
let v,e be object, w be Vertex of G2, G1 be addAdjVertex of G2,v,e,w;
let t1 be TColoring of G1, t2 be TColoring of G2, x,y be object;
assume that A1: not e in the_Edges_of G2 & not v in the_Vertices_of G2 and
A2: t1_V = t2_V +* (v .--> x) & t1_E = t2_E +* (e .--> y) and
A3: not y in (rng t2_V)\/rng t2_E & x <> y & x <> t2_V.w & t2 is proper;
A4: t1_V is proper by A1, A2, A3, Th23;
not y in rng t2_E by A3, XBOOLE_0:def 3;
then A5: t1_E is proper by A1, A2, A3, Th94;
now
let e9,v9,w9 be object;
assume A6: e9 Joins v9,w9,G1;
then per cases by GLIB_006:72;
suppose A7: e9 Joins v9,w9,G2;
then e9 in the_Edges_of G2 by GLIB_000:def 13;
then not e9 in dom(e.-->y) by A1, TARSKI:def 1;
then A8: t1_E.e9 = t2_E.e9 by A2, FUNCT_4:11;
v9 in the_Vertices_of G2 by A7, GLIB_000:13;
then not v9 in dom(v.-->x) by A1, TARSKI:def 1;
then t1_V.v9 = t2_V.v9 by A2, FUNCT_4:11;
hence t1_V.v9 <> t1_E.e9 by A3, A7, A8, Th146;
end;
suppose A9: not e9 in the_Edges_of G2;
A10: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, GLIB_006:def 12;
e9 in the_Edges_of G1 by A6, GLIB_000:def 13;
then e9 in {e} by A9, A10, XBOOLE_0:def 3;
then e9 = e by TARSKI:def 1;
then A11: t1_E.e9 = y by A2, FUNCT_4:113;
per cases;
suppose v9 = v;
hence t1_V.v9 <> t1_E.e9 by A2, A3, A11, FUNCT_4:113;
end;
suppose A12: v9 <> v;
then not v9 in dom(v.-->x) by TARSKI:def 1;
then A13: t1_V.v9 = t2_V.v9 by A2, FUNCT_4:11;
A14: the_Vertices_of G1 = the_Vertices_of G2 \/ {v}
by A1, GLIB_006:def 12;
v9 in the_Vertices_of G1 & not v9 in {v}
by A6, A12, GLIB_000:13, TARSKI:def 1;
then v9 in the_Vertices_of G2 by A14, XBOOLE_0:def 3;
then v9 in dom t2_V by PARTFUN1:def 2;
then t1_V.v9 in rng t2_V by A13, FUNCT_1:3;
hence t1_V.v9 <> t1_E.e9 by A3, A11, XBOOLE_0:def 3;
end;
end;
end;
hence thesis by A4, A5, Th146;
end;
theorem
for v being Vertex of G2, e,w being object, G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1, t2 being TColoring of G2, 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
let v be Vertex of G2, e,w be object, G1 be addAdjVertex of G2,v,e,w;
let t1 be TColoring of G1, t2 be TColoring of G2, x,y be object;
assume that A1: not e in the_Edges_of G2 & not w in the_Vertices_of G2 and
A2: t1_V = t2_V +* (w .--> x) & t1_E = t2_E +* (e .--> y) and
A3: not y in (rng t2_V)\/rng t2_E & x <> y & x <> t2_V.v & t2 is proper;
set G3 = the reverseEdgeDirections of G1, {e};
A4: G3 is addAdjVertex of G2,w,e,v by A1, GLIBPRE1:66;
the_Vertices_of G1 = the_Vertices_of G3 by GLIB_007:4;
then reconsider f3 = t1_V as VColoring of G3;
the_Edges_of G1 = the_Edges_of G3 by GLIB_007:4;
then reconsider g3 = t1_E as EColoring of G3;
reconsider t3 = [f3,g3] as TColoring of G3;
t3 is proper by A1, A2, A3, A4, Th158;
hence thesis by Th153;
end;
theorem Th160:
for F being PGraphMapping of G1,G, 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
let F be PGraphMapping of G1,G, t9 be TColoring of G1;
assume A1: F is weak_SG-embedding & t9 = [t_V*(F_V),t_E*(F_E)] & t is proper;
then A2: t9_V is proper by Th26;
A3: t9_E is proper by A1, Th98;
now
let e,v,w be object;
assume A4: e Joins v,w,G1;
then e in the_Edges_of G1 by GLIB_000:def 13;
then A5: e in dom F_E by A1, GLIB_010:def 11;
((the_Source_of G1).e = v & (the_Target_of G1).e = w) or
((the_Source_of G1).e = w & (the_Target_of G1).e = v)
by A4, GLIB_000:def 13;
then A6: v in dom F_V & w in dom F_V by A5, GLIB_010:5;
then F_E.e Joins F_V.v,F_V.w,G by A4, A5, GLIB_010:4;
then A7: t_V.(F_V.v) <> t_E.(F_E.e) by A1, Th146;
t_V.(F_V.v) = t9_V.v & t_E.(F_E.e) = t9_E.e by A1, A5, A6, FUNCT_1:13;
hence t9_V.v <> t9_E.e by A7;
end;
hence thesis by A2, A3, Th146;
end;
definition
let c, G;
attr G is c-tcolorable means
ex t being TColoring of G st t is proper & card((rng t_V)\/rng t_E) c= c;
end;
theorem Th161:
c1 c= c2 & G is c1-tcolorable implies G is c2-tcolorable by XBOOLE_1:1;
theorem Th162:
G is c-tcolorable implies G is c-vcolorable & G is c-ecolorable
proof
assume G is c-tcolorable;
then consider t being TColoring of G such that
A1: t is proper & card((rng t_V)\/rng t_E) c= c;
card rng t_V c= card((rng t_V)\/rng t_E) by XBOOLE_1:7, CARD_1:11;
hence G is c-vcolorable by A1, XBOOLE_1:1;
card rng t_E c= card((rng t_V)\/rng t_E) by XBOOLE_1:7, CARD_1:11;
hence G is c-ecolorable by A1, XBOOLE_1:1;
end;
theorem Th163:
G is c1-vcolorable c2-ecolorable implies G is (c1+`c2)-tcolorable
proof
assume A1: G is c1-vcolorable c2-ecolorable;
then consider f9 being VColoring of G such that
A2: f9 is proper & card rng f9 c= c1;
consider g being proper EColoring of G such that
A3: card rng g c= c2 by A1;
consider f being VColoring of G such that
A4: f is proper & rng f misses rng g & card rng f9 = card rng f
by A2, Th150;
reconsider t = [f,g] as TColoring of G;
A5: t is proper by A4, Th147;
card((rng t_V)\/rng t_E) = card rng t_V +` card rng t_E by A4, CARD_2:35;
then card((rng t_V)\/rng t_E) c= c1 +` c2
by A2, A3, A4, CARD_2:83;
hence thesis by A5;
end;
:: might need Proof outside this article
theorem
G is edgeless & f is proper & t = [ f , {} ] implies t is proper;
theorem Th165:
G is edgeless iff G is 1-tcolorable
proof
hereby
assume A1: G is edgeless;
then G is 1-vcolorable;
then consider f being VColoring of G such that
A2: f is proper & card rng f c= 1;
reconsider t = [f,{}] as TColoring of G by A1, Th137;
A3: t is proper by A2;
card((rng t_V)\/rng t_E) = card((rng t_V)\/rng {})
.= card rng t_V;
hence G is 1-tcolorable by A2, A3;
end;
assume G is 1-tcolorable;
then G is 1-vcolorable by Th162;
hence thesis;
end;
registration
let c be non zero Cardinal;
cluster c-tcolorable for _Graph;
existence
proof
take the edgeless _Graph;
1 c= c
proof
assume not 1 c= c;
then c in {0} by CARD_1:49, ORDINAL1:16;
hence contradiction by TARSKI:def 1;
end;
hence thesis by Th161, Th165;
end;
end;
theorem Th166:
for H being Subgraph of G holds G is c-tcolorable implies H is c-tcolorable
proof
let H be Subgraph of G;
assume G is c-tcolorable;
then consider t being TColoring of G such that
A1: t is proper & card((rng t_V)\/rng t_E) c= c;
reconsider t9 = [ t_V | the_Vertices_of H , t_E | the_Edges_of H ]
as TColoring of H by Th138;
rng t9_V c= rng t_V & rng t9_E c= rng t_E by RELAT_1:70;
then (rng t9_V)\/rng t9_E c= (rng t_V)\/rng t_E by XBOOLE_1:13;
then card((rng t9_V)\/rng t9_E) c= card((rng t_V)\/rng t_E) by CARD_1:11;
then card((rng t9_V)\/rng t9_E) c= c by A1, XBOOLE_1:1;
hence thesis by A1, Th151;
end;
registration
cluster -> non 0-tcolorable for _Graph;
coherence by Th162;
cluster edgeless -> 1-tcolorable for _Graph;
coherence by Th165;
cluster 1-tcolorable -> edgeless for _Graph;
coherence by Th165;
let c be non zero Cardinal;
let G be c-tcolorable _Graph;
cluster -> c-tcolorable for Subgraph of G;
coherence by Th166;
end;
registration
let c;
cluster c-tcolorable -> loopless for _Graph;
coherence
proof
let G be _Graph;
assume G is c-tcolorable;
then G is c-vcolorable by Th162;
hence thesis;
end;
end;
theorem Th167:
G1 == G2 & G1 is c-tcolorable implies G2 is c-tcolorable
proof
assume A1: G1 == G2 & G1 is c-tcolorable;
then consider t1 being TColoring of G1 such that
A2: t1 is proper & card((rng t1_V)\/rng t1_E) c= c;
A3: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by A1, GLIB_000:def 34;
then reconsider f = t1_V as VColoring of G2;
reconsider g = t1_E as EColoring of G2 by A3;
reconsider t2 = [f,g] as TColoring of G2;
t2 is proper by A1, A2, Th152;
hence thesis by A2;
end;
Lm17:
for G2 being reverseEdgeDirections of G1, E
st G1 is c-tcolorable holds G2 is c-tcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
assume G1 is c-tcolorable;
then consider t1 being TColoring of G1 such that
A1: t1 is proper & card((rng t1_V)\/rng t1_E) c= c;
A2: the_Vertices_of G1 = the_Vertices_of G2 &
the_Edges_of G1 = the_Edges_of G2 by GLIB_007:4;
then reconsider f = t1_V as VColoring of G2;
reconsider g = t1_E as EColoring of G2 by A2;
reconsider t2 = [f,g] as TColoring of G2;
t2 is proper by A1, Th153;
hence thesis by A1;
end;
theorem Th168:
for G2 being reverseEdgeDirections of G1, E
holds G1 is c-tcolorable iff G2 is c-tcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
thus G1 is c-tcolorable implies G2 is c-tcolorable by Lm17;
G1 is reverseEdgeDirections of G2, E by GLIB_007:3;
hence thesis by Lm17;
end;
registration
let c be non zero Cardinal;
let G1 be c-tcolorable _Graph;
let E;
cluster -> c-tcolorable for reverseEdgeDirections of G1, E;
coherence by Th168;
end;
theorem Th169:
for G1 being addVertices of G2, V
holds G1 is c-tcolorable iff G2 is c-tcolorable
proof
let G1 be addVertices of G2, V;
G2 is Subgraph of G1 by GLIB_006:57;
hence G1 is c-tcolorable implies G2 is c-tcolorable by Th166;
assume G2 is c-tcolorable;
then consider t2 being TColoring of G2 such that
A1: t2 is proper & card((rng t2_V)\/rng t2_E) c= c;
set x = the Element of rng t2_V;
set h = (V \ the_Vertices_of G2) --> x, f = t2_V +* h;
A2: dom h = V \ the_Vertices_of G2;
then reconsider t1 = [f, t2_E] as TColoring of G1 by Th139;
t1_E = t2_E & t1_V = t2_V +* h;
then A3: t1 is proper by A1, A2, Th154;
(rng f)\/rng t1_E c= (rng t2_V)\/rng t2_E by Lm3, XBOOLE_1:9;
then card((rng f)\/rng t1_E) c= card((rng t2_V)\/rng t2_E) by CARD_1:11;
hence thesis by A1, A3, XBOOLE_1:1;
end;
registration
let c be non zero Cardinal;
let G2 be c-tcolorable _Graph;
let V;
cluster -> c-tcolorable for addVertices of G2, V;
coherence by Th169;
end;
theorem
for e being object, v,w being Vertex of G2, G1 being addEdge of G2,v,e,w
st v,w are_adjacent & G2 is c-tcolorable holds G1 is (c+`1)-tcolorable
proof
let e be object, v,w be Vertex of G2, G1 be addEdge of G2,v,e,w;
assume A1: v,w are_adjacent & G2 is c-tcolorable;
per cases;
suppose A2: not e in the_Edges_of G2;
consider t being TColoring of G2 such that
A3: t is proper & card((rng t_V)\/rng t_E) c= c by A1;
set V = rng t_V, E = rng t_E;
set y = V \/ E, g = t_E +* (e .--> y);
reconsider t1 = [t_V, g] as TColoring of G1 by A2, Th141;
not y in V \/ E & t1_V = t_V & t1_E = t_E +* (e .--> y);
then A4: t1 is proper by A1, A2, A3, Th155;
rng(e .--> y) = rng{[e,y]} by FUNCT_4:82
.= {y} by RELAT_1:9;
then V \/ rng g c= V \/ (E \/ {y}) by FUNCT_4:17, XBOOLE_1:9;
then V \/ rng g c= (V \/ E) \/ {y} by XBOOLE_1:4;
then A5: card(V \/ rng g) c= card((V \/ E) \/ {y}) by CARD_1:11;
not y in V \/ E;
then card((V\/E)\/{y}) = card(V \/ E) +` card {y} by ZFMISC_1:50, CARD_2:35
.= card(V \/ E) +` 1 by CARD_1:30;
then card((V \/ E) \/ {y}) c= c +` 1 by A3, CARD_2:84;
hence thesis by A4, A5, XBOOLE_1:1;
end;
suppose e in the_Edges_of G2;
then G1 == G2 by GLIB_006:def 11;
then G1 is c-tcolorable by A1, Th167;
hence thesis by Th161, CARD_2:94;
end;
end;
theorem Th171:
for v,e,w being object, G1 being addEdge of G2,v,e,w
st v <> w & G2 is c-tcolorable holds G1 is (c+`2)-tcolorable
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
assume A1: v <> w & G2 is c-tcolorable;
per cases;
suppose A2: v is Vertex of G2 & w is Vertex of G2 & not e in the_Edges_of G2;
consider t being TColoring of G2 such that
A3: t is proper & card((rng t_V)\/rng t_E) c= c by A1;
set V = rng t_V, E = rng t_E;
set x = V \/ E, y = {x}, f = t_V +* (v .--> x), g = t_E +* (e .--> y);
reconsider t1 = [f, g] as TColoring of G1 by A2, Th142;
A4: {x,y} misses V \/ E & x <> y
proof
A5: not x in V \/ E;
not y in V \/ E by TARSKI:def 1;
hence {x,y} misses V \/ E by A5, ZFMISC_1:51;
x in y by TARSKI:def 1;
hence thesis;
end;
t1_V = t_V +* (v .--> x) & t1_E = t_E +* (e .--> y);
then A6: t1 is proper by A1, A2, A3, A4, Th156;
rng(e .--> y) = rng{[e,y]} by FUNCT_4:82
.= {y} by RELAT_1:9;
then A7: rng g c= E \/ {y} by FUNCT_4:17;
rng(v .--> x) = rng{[v,x]} by FUNCT_4:82
.= {x} by RELAT_1:9;
then rng f c= V \/ {x} by FUNCT_4:17;
then A8: rng f \/ rng g c= (V \/ {x}) \/ (E \/ {y}) by A7, XBOOLE_1:13;
A9: (V \/ {x}) \/ (E \/ {y}) = V \/ ({x} \/ (E \/ {y})) by XBOOLE_1:4
.= V \/ (({x} \/ {y}) \/ E) by XBOOLE_1:4
.= (V \/ E) \/ ({x} \/ {y}) by XBOOLE_1:4
.= (V \/ E) \/ {x,y} by ENUMSET1:1;
card((V \/ E) \/ {x,y}) = card(V \/ E) +` card {x,y} by A4, CARD_2:35
.= card(V \/ E) +` 2 by A4, CARD_2:57;
then A10: card((V \/ E) \/ {x,y}) c= c +` 2 by A3, CARD_2:84;
card(rng f \/ rng g) c= card((V \/ E) \/ {x,y}) by A8, A9, CARD_1:11;
hence thesis by A6, A10, XBOOLE_1:1;
end;
suppose not(v is Vertex of G2 & w is Vertex of G2 &
not e in the_Edges_of G2);
then G1 == G2 by GLIB_006:def 11;
then G1 is c-tcolorable by A1, Th167;
hence thesis by Th161, CARD_2:94;
end;
end;
Lm18:
for G2 being non edgeless _Graph, v,e being object, w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
st not e in the_Edges_of G2 & not v in the_Vertices_of G2
holds G2 is c-tcolorable implies G1 is (c+`1)-tcolorable
proof
let G2 be non edgeless _Graph, v,e be object, w being Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not e in the_Edges_of G2 & not v in the_Vertices_of G2;
assume G2 is c-tcolorable;
then consider t2 being TColoring of G2 such that
A2: t2 is proper & card((rng t2_V)\/rng t2_E) c= c;
set V = rng t2_V, E = rng t2_E;
set x = the Element of V\{t2_V.w}, y = V \/ E;
V\{t2_V.w} <> {}
proof
assume V\{t2_V.w} = {};
then V = {} or V = {t2_V.w} by ZFMISC_1:58;
then card V = 0 or card V = 1 by CARD_1:30;
then G2 is 0-vcolorable or G2 is 1-vcolorable by A2;
hence contradiction;
end;
then A3: x in V & x <> t2_V.w by ZFMISC_1:56;
set f = t2_V +* (v .--> x), g = t2_E +* (e .--> y);
reconsider t1 = [f, g] as TColoring of G1 by A1, Th143;
x in V \/ E by A3, XBOOLE_0:def 3;
then x<>y & not y in V\/E & t1_V = t2_V+*(v.-->x) & t1_E = t2_E+*(e .--> y);
then A4: t1 is proper by A1, A2, A3, Th158;
rng(e .--> y) = rng{[e,y]} by FUNCT_4:82
.= {y} by RELAT_1:9;
then A5: rng g c= E \/ {y} by FUNCT_4:17;
f = t2_V +* ({v} --> x) by FUNCOP_1:def 9;
then rng f c= V by A3, Lm3;
then rng f \/ rng g c= V \/ (E \/ {y}) by A5, XBOOLE_1:13;
then rng f \/ rng g c= (V \/ E) \/ {y} by XBOOLE_1:4;
then A6: card(rng f \/ rng g) c= card((V \/ E) \/ {y}) by CARD_1:11;
not y in V \/ E;
then card((V\/E)\/{y}) = card(V \/ E) +` card {y} by ZFMISC_1:50, CARD_2:35
.= card(V \/ E) +` 1 by CARD_1:30;
then card((V \/ E) \/ {y}) c= c +` 1 by A2, CARD_2:84;
hence thesis by A4, A6, XBOOLE_1:1;
end;
theorem Th172:
for G2 being non edgeless _Graph, 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
let G2 be non edgeless _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: G2 is c-tcolorable;
per cases;
suppose not e in the_Edges_of G2 & not v in the_Vertices_of G2
& w in the_Vertices_of G2;
hence thesis by A1, Lm18;
end;
suppose A2: not e in the_Edges_of G2 & v in the_Vertices_of G2
& not w in the_Vertices_of G2;
set G3 = the reverseEdgeDirections of G1, {e};
G3 is addAdjVertex of G2,w,e,v by A2, GLIBPRE1:66;
then G3 is (c+`1)-tcolorable by A1, A2, Lm18;
hence thesis by Th168;
end;
suppose not((not e in the_Edges_of G2 & not v in the_Vertices_of G2
& w in the_Vertices_of G2)or(not e in the_Edges_of G2
& v in the_Vertices_of G2 & not w in the_Vertices_of G2));
then G1 == G2 by GLIB_006:def 12;
then G1 is c-tcolorable by A1, Th167;
hence thesis by Th161, CARD_2:94;
end;
end;
Lm19:
for f being Function, x,y being object holds rng(f+*(x.-->y)) c= rng f \/ {y}
proof
let f be Function, x,y be object;
rng(x.-->y) = rng{[x,y]} by FUNCT_4:82
.= {y} by RELAT_1:9;
hence thesis by FUNCT_4:17;
end;
theorem
for v being Vertex of G2, e,w being object, 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
holds G2 is c-tcolorable implies G1 is c-tcolorable
proof
let v be Vertex of G2, e,w be object, G1 be addAdjVertex of G2,v,e,w;
assume A1: not e in the_Edges_of G2 & not w in the_Vertices_of G2;
assume A2: v is endvertex & G2 is c-tcolorable;
then consider t2 being TColoring of G2 such that
A3: t2 is proper & card((rng t2_V)\/rng t2_E) c= c;
consider e9 being object such that
A4: v.edgesInOut() = {e9} & not e9 Joins v,v,G2 by A2, GLIB_000:def 51;
e9 in v.edgesInOut() by A4, TARSKI:def 1;
then consider v9 being Vertex of G2 such that
A5: e9 Joins v,v9,G2 by GLIB_000:64;
set f = t2_V +* (w .--> t2_E.e9), g = t2_E +* (e .--> t2_V.v9);
reconsider t1 = [f, g] as TColoring of G1 by A1, Th144;
:: show that the coloring is proper
now
let e1,e2,u,w1,w2 be object;
A6: e Joins v,w,G1 by A1, GLIB_006:131;
A7: the_Edges_of G1 = the_Edges_of G2 \/ {e} by A1, GLIB_006:def 12;
assume A8: e1 Joins u,w1,G1 & e2 Joins u,w2,G1;
then per cases by GLIB_006:72;
suppose A9: e1 Joins u,w1,G2 & e2 Joins u,w2,G2;
then e1 in the_Edges_of G2 & e2 in the_Edges_of G2 by GLIB_000:def 13;
then A10: t1_E.e1 = t2_E.e1 & t1_E.e2 = t2_E.e2 by A1, FUNCT_4:83;
u in the_Vertices_of G2 & w1 in the_Vertices_of G2 by A9, GLIB_000:13;
then t1_V.u = t2_V.u & t1_V.w1 = t2_V.w1 by A1, FUNCT_4:83;
hence t1_V.u <> t1_V.w1 & t1_V.u <> t1_E.e1 by A3, A9, A10, Th148;
thus e1 <> e2 implies t1_E.e1 <> t1_E.e2 by A3, A9, A10, Th148;
end;
suppose A11: e1 Joins u,w1,G2 & not e2 in the_Edges_of G2;
e2 in the_Edges_of G1 by A8, GLIB_000:def 13;
then e1 in the_Edges_of G2 & e2 in {e}
by A7, A11, GLIB_000:def 13, XBOOLE_0:def 3;
then A12: e1 <> e & e2 = e by A1, TARSKI:def 1;
then A13: t1_E.e1=t2_E.e1 & t1_E.e2 = t2_V.v9 by FUNCT_4:83, FUNCT_4:113;
u in the_Vertices_of G2 & w1 in the_Vertices_of G2 by A11, GLIB_000:13;
then t1_V.u = t2_V.u & t1_V.w1 = t2_V.w1 by A1, FUNCT_4:83;
hence t1_V.u <> t1_V.w1 & t1_V.u <> t1_E.e1 by A3, A11, A13, Th148;
assume e1 <> e2 & t1_E.e1 = t1_E.e2;
then A14: t2_E.e1 = t2_V.v9 & e9 Joins v9,v,G2 by A5, A13, GLIB_000:14;
u in the_Vertices_of G2 by A11, GLIB_000:13;
then u = v & w2 = w by A1, A6, A8, A12, GLIB_000:15;
then e1 in v.edgesInOut() by A11, GLIB_000:62;
then e1 = e9 by A4, TARSKI:def 1;
hence contradiction by A3, A14, Th148;
end;
suppose A15: not e1 in the_Edges_of G2 & e2 Joins u,w2,G2;
e1 in the_Edges_of G1 by A8, GLIB_000:def 13;
then e2 in the_Edges_of G2 & e1 in {e}
by A7, A15, GLIB_000:def 13, XBOOLE_0:def 3;
then A16: e2 <> e & e1 = e by A1, TARSKI:def 1;
then A17: t1_E.e2=t2_E.e2 & t1_E.e1 = t2_V.v9 by FUNCT_4:83, FUNCT_4:113;
A18: u in the_Vertices_of G2 by A15, GLIB_000:13;
then A19: t1_V.u = t2_V.u by A1, FUNCT_4:83;
A20: u = v & w1 = w by A1, A6, A8, A16, A18, GLIB_000:15;
then t1_V.w1 = t2_E.e9 by FUNCT_4:113;
hence t1_V.u <> t1_V.w1 by A3, A5, A19, A20, Th148;
thus t1_V.u <> t1_E.e1 by A3, A5, A17, A19, A20, Th148;
assume e1 <> e2 & t1_E.e1 = t1_E.e2;
then A21: t2_E.e2 = t2_V.v9 & e9 Joins v9,v,G2 by A5, A17, GLIB_000:14;
e2 in v.edgesInOut() by A15, A20, GLIB_000:62;
then e2 = e9 by A4, TARSKI:def 1;
hence contradiction by A3, A21, Th148;
end;
suppose A22: not e1 in the_Edges_of G2 & not e2 in the_Edges_of G2;
A23: v <> w by A1;
e1 in the_Edges_of G1 & e2 in the_Edges_of G1 by A8, GLIB_000:def 13;
then e1 in {e} & e2 in {e} by A7, A22, XBOOLE_0:def 3;
then A24: e2 = e & e1 = e by TARSKI:def 1;
then per cases by A6, A8, GLIB_000:15;
suppose u = v & w1 = w;
then A25: t1_V.u = t2_V.v & t1_V.w1 = t2_E.e9
by A23, FUNCT_4:83, FUNCT_4:113;
hence t1_V.u <> t1_V.w1 by A3, A5, Th148;
t1_E.e1 = t2_V.v9 by A24, FUNCT_4:113;
hence t1_V.u <> t1_E.e1 by A3, A5, A25, Th148;
thus e1 <> e2 implies t1_E.e1 <> t1_E.e2 by A24;
end;
suppose u = w & w1 = v;
then A26: t1_V.u = t2_E.e9 & t1_V.w1 = t2_V.v
by A23, FUNCT_4:83, FUNCT_4:113;
hence t1_V.u <> t1_V.w1 by A3, A5, Th148;
t1_E.e1 = t2_V.v9 & e9 Joins v9,v,G2
by A5, A24, FUNCT_4:113, GLIB_000:14;
hence t1_V.u <> t1_E.e1 by A3, A26, Th148;
thus e1 <> e2 implies t1_E.e1 <> t1_E.e2 by A24;
end;
end;
end;
then A27: t1 is proper by Th148;
:: count the number of colors
e9 in the_Edges_of G2 & v9 in the_Vertices_of G2 by A5, GLIB_000:def 13;
then e9 in dom t2_E & v9 in dom t2_V by PARTFUN1:def 2;
then t2_E.e9 in rng t2_E & t2_V.v9 in rng t2_V by FUNCT_1:3;
then A28: {t2_E.e9} c= rng t2_E & {t2_V.v9} c= rng t2_V by ZFMISC_1:31;
A29: rng t2_V \/ {t2_E.e9} \/ (rng t2_E \/{t2_V.v9})
= rng t2_V \/ {t2_E.e9} \/ rng t2_E \/ {t2_V.v9} by XBOOLE_1:4
.= ({t2_E.e9} \/ rng t2_E) \/ rng t2_V \/ {t2_V.v9} by XBOOLE_1:4
.= rng t2_E \/ rng t2_V \/ {t2_V.v9} by A28, XBOOLE_1:12
.= rng t2_E \/ (rng t2_V \/ {t2_V.v9}) by XBOOLE_1:4
.= rng t2_V \/ rng t2_E by A28, XBOOLE_1:12;
rng t1_V c= rng t2_V \/{t2_E.e9} & rng t1_E c= rng t2_E \/{t2_V.v9} by Lm19;
then rng t1_V \/ rng t1_E c= rng t2_V \/ rng t2_E by A29, XBOOLE_1:13;
then card(rng t1_V \/ rng t1_E) c= card(rng t2_V \/ rng t2_E) by CARD_1:11;
hence thesis by A3, A27, XBOOLE_1:1;
end;
theorem Th174:
for G2 being edgeless _Graph, v,e,w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is 3-tcolorable
proof
let G2 be edgeless _Graph, v,e,w being object;
let G1 be addAdjVertex of G2,v,e,w;
G1 is 2-vcolorable 1-ecolorable by Th38;
then G1 is (2+`1)-tcolorable by Th163;
hence thesis;
end;
Lm20:
for X, Y being set holds not Y in rng <: X --> Y, id X :>
proof
let X, Y be set;
set h = <: X --> Y, id X :>;
assume Y in rng h;
then consider x being object such that
A1: x in dom h & h.x = Y by FUNCT_1:def 3;
x in X by A1, Lm8;
then Y = [Y,x] by A1, Lm9
.= {{Y,x},{Y}} by TARSKI:def 5;
then {Y} in Y & Y in {Y} by TARSKI:def 1, TARSKI:def 2;
hence contradiction;
end;
Lm21:
for X, Y being set holds Y \/ {Y} misses rng <: X --> Y, id X :>
proof
let X, Y be set;
set h = <: X --> Y, id X :>;
A1: Y misses rng h by Lm11;
{Y} misses rng h by Lm20, ZFMISC_1:50;
hence thesis by A1, XBOOLE_1:70;
end;
theorem Th175:
for v being object, G1 being addAdjVertexAll of G2,v,V
st G2 is c-tcolorable holds G1 is (c+`1+`card V)-tcolorable
proof
let v be object, G1 be addAdjVertexAll of G2,v,V;
assume A1: G2 is c-tcolorable;
per cases;
suppose A2: not v in the_Vertices_of G2 & V c= the_Vertices_of G2;
:: construct the coloring
consider t0 being TColoring of G2 such that
A3: t0 is proper & card((rng t0_V) \/ rng t0_E) c= c by A1;
set R = (rng t0_V) \/ rng t0_E, E = G1.edgesBetween(V,{v});
set h = <: E --> R, id E :>, g = t0_E +* h, f = t0_V +* (v .--> R);
A4: dom h = E & rng t0_E c= R by Lm8, XBOOLE_1:7;
then reconsider g as EColoring of G1 by A2, Th82;
reconsider f as VColoring of G1 by A2, Th7;
:: show it is proper
reconsider g as proper EColoring of G1 by A2, A3, A4, Th96;
reconsider t = [f,g] as TColoring of G1;
not R in rng t0_V
proof
assume A5: R in rng t0_V;
rng t0_V c= R by XBOOLE_1:7;
then R in R by A5;
hence contradiction;
end;
then A6: t_V is proper by A2, A3, Th25;
now
let e,u,w be object;
assume A7: e Joins u,w,G1;
per cases by A7, GLIB_006:72;
suppose A8: not e in the_Edges_of G2;
A9: the_Edges_of G1 = the_Edges_of G2 \/ E by A2, GLIB_007:59;
e in the_Edges_of G1 by A7, GLIB_000:def 13;
then A10: e in E by A8, A9, XBOOLE_0:def 3;
then e SJoins V,{v},G1 by GLIB_000:def 30;
then consider x being object such that
A11: x in V & e Joins x,v,G1 by GLIB_000:102;
A12: x <> v by A2, A11;
e in dom h by A10, Lm8;
then A13: t_E.e = h.e by FUNCT_4:13
.= [R,e] by A10, Lm9;
per cases by A7, A11, GLIB_000:15;
suppose A14: u = x & w = v;
then A15: t_V.u = t0_V.u by A12, FUNCT_4:83;
u in the_Vertices_of G2 by A2, A11, A14;
then u in dom t0_V by PARTFUN1:def 2;
then A16: t0_V.u in rng t0_V by FUNCT_1:3;
assume t_V.u = t_E.e;
then A17: [R,e] in rng t0_V by A13, A15, A16;
rng t0_V c= R by XBOOLE_1:7;
then [R,e] in R by A17;
then A18: {{R,e},{R}} in R by TARSKI:def 5;
A19: R in {R} by TARSKI:def 1;
{R} in {{R,e},{R}} by TARSKI:def 2;
hence contradiction by A18, A19, XREGULAR:7;
end;
suppose u = v & w = x;
then A20: t_V.u = R by FUNCT_4:113;
assume t_V.u = t_E.e;
then R = {{R,e},{R}} by A13, A20, TARSKI:def 5;
then R in {R} & {R} in R by TARSKI:def 1, TARSKI:def 2;
hence contradiction;
end;
end;
suppose A21: e Joins u,w,G2;
then A22: t0_V.u <> t0_E.e by A3, Th146;
A23: e in the_Edges_of G2 & u in the_Vertices_of G2
by A21, GLIB_000:def 13, GLIB_000:13;
the_Edges_of G2 misses E by A2, GLIB_007:59;
then not e in E by A23, XBOOLE_0:3;
then not e in dom h by Lm8;
then A24: t_E.e = t0_E.e by FUNCT_4:11;
t_V.u = t0_V.u by A2, A23, FUNCT_4:83;
hence t_V.u <> t_E.e by A22, A24;
end;
end;
then A25: t is proper by A6, Th146;
:: count the colors
rng t0_V \/ rng(v.-->R) = rng t0_V \/ rng{[v,R]} by FUNCT_4:82
.= rng t0_V \/ {R} by RELAT_1:9;
then A26: rng f c= rng t0_V \/ {R} by FUNCT_4:17;
A27: rng g c= rng t0_E \/ rng h by FUNCT_4:17;
(rng t0_V \/ {R}) \/ (rng t0_E \/ rng h)
= (rng t0_V \/ {R} \/ rng t0_E) \/ rng h by XBOOLE_1:4
.= R \/ {R} \/ rng h by XBOOLE_1:4;
then rng f \/ rng g c= R \/ {R} \/ rng h by A26, A27, XBOOLE_1:13;
then A28: card(rng f \/ rng g) c= card(R \/ {R} \/ rng h) by CARD_1:11;
not R in R;
then A29: R misses {R} by ZFMISC_1:50;
A30: card E = card V
proof
consider E0 being set such that
A31: card V = card E0 & E0 misses the_Edges_of G2 and
A32: the_Edges_of G1 = the_Edges_of G2 \/ E0 and
for v1 being object st v1 in V ex e1 being object st e1 in E0 &
e1 Joins v1,v,G1 &
for e2 being object st e2 Joins v1,v,G1 holds e1 = e2
by A2, GLIB_007:def 4;
thus thesis by A2, A31, A32, GLIB_007:58;
end;
card(R \/ {R} \/ rng h)
= card(R \/ {R}) +` card rng h by Lm21, CARD_2:35
.= card R +` card {R} +` card rng h by A29, CARD_2:35
.= card R +` 1 +` card rng h by CARD_1:30
.= card R +` 1 +` card [: {R}, E :] by Lm10
.= card R +` 1 +` card [: E, {R} :] by CARD_2:4
.= card R +` 1 +` card E by CARD_1:69
.= card R +` (1 +` card V) by A30, CARD_2:19;
then card(R \/ {R} \/ rng h) c= c +` (1 +` card V) by A3, CARD_2:84;
then card(R \/ {R} \/ rng h) c= c +` 1 +` card V by CARD_2:19;
hence thesis by A25, A28, XBOOLE_1:1;
end;
suppose not(not v in the_Vertices_of G2 & V c= the_Vertices_of G2);
then G1 == G2 by GLIB_007:def 4;
then G1 is c-tcolorable by A1, Th167;
then G1 is (c+`1)-tcolorable by Th161, CARD_2:94;
hence thesis by Th161, CARD_2:94;
end;
end;
theorem Th176:
for F being PGraphMapping of G1, G2
st F is weak_SG-embedding & G2 is c-tcolorable holds G1 is c-tcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is c-tcolorable;
then consider t2 being TColoring of G2 such that
A2: t2 is proper & card((rng t2_V)\/rng t2_E) c= c;
reconsider t1 = [ t2_V*(F_V) , t2_E*(F_E) ] as TColoring of G1 by A1, Th145;
A3: t1 is proper by A1, A2, Th160;
rng t1_V c= rng t2_V & rng t1_E c= rng t2_E by RELAT_1:26;
then (rng t1_V)\/rng t1_E c= (rng t2_V)\/rng t2_E by XBOOLE_1:13;
then card((rng t1_V)\/rng t1_E) c= card((rng t2_V)\/rng t2_E) by CARD_1:11;
hence thesis by A2, A3, XBOOLE_1:1;
end;
theorem Th177:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is c-tcolorable iff G2 is c-tcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
hence G1 is c-tcolorable implies G2 is c-tcolorable by Th176;
thus G2 is c-tcolorable implies G1 is c-tcolorable by A1, Th176;
end;
registration
let c be non zero Cardinal;
let G be c-tcolorable _Graph;
cluster G-isomorphic -> c-tcolorable for _Graph;
coherence
proof
let H be _Graph;
assume H is G-isomorphic;
then consider F being PGraphMapping of G,H such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th177;
end;
end;
definition
let G;
attr G is finite-tcolorable means :: or finitely-tcolorable
:Def12:
ex n st G is n-tcolorable;
end;
registration
cluster finite-tcolorable -> loopless for _Graph;
coherence;
cluster edgeless -> finite-tcolorable for _Graph;
coherence
proof
let G be _Graph;
assume G is edgeless;
then G is 1-tcolorable;
hence thesis;
end;
let n;
cluster n-tcolorable -> finite-tcolorable for _Graph;
coherence;
end;
registration
cluster finite-tcolorable for _Graph;
existence
proof
take the edgeless _Graph;
thus thesis;
end;
cluster non finite-tcolorable for _Graph;
existence
proof
take the non loopless _Graph;
thus thesis;
end;
end;
registration
let G be finite-tcolorable _Graph;
cluster -> finite-tcolorable for Subgraph of G;
coherence
proof
let H be Subgraph of G;
consider n such that
A1: G is n-tcolorable by Def12;
H is n-tcolorable by A1, Th166;
hence thesis;
end;
end;
theorem
G1 == G2 & G1 is finite-tcolorable implies G2 is finite-tcolorable
proof
assume A1: G1 == G2 & G1 is finite-tcolorable;
then consider n such that
A2: G1 is n-tcolorable;
G2 is n-tcolorable by A1, A2, Th167;
hence thesis;
end;
theorem Th179:
for G2 being reverseEdgeDirections of G1, E
holds G1 is finite-tcolorable iff G2 is finite-tcolorable
proof
let G2 be reverseEdgeDirections of G1, E;
hereby
assume G1 is finite-tcolorable;
then consider n such that
A1: G1 is n-tcolorable;
G2 is n-tcolorable by A1, Th168;
hence G2 is finite-tcolorable;
end;
assume G2 is finite-tcolorable;
then consider n such that
A2: G2 is n-tcolorable;
thus G1 is finite-tcolorable by A2, Def12, Th168;
end;
registration
let G1 be finite-tcolorable _Graph; let E;
cluster -> finite-tcolorable for reverseEdgeDirections of G1, E;
coherence by Th179;
end;
registration
let G1 be non finite-tcolorable _Graph; let E;
cluster -> non finite-tcolorable for reverseEdgeDirections of G1, E;
coherence by Th179;
end;
theorem Th180:
for G1 being addVertices of G2, V
holds G1 is finite-tcolorable iff G2 is finite-tcolorable
proof
let G1 be addVertices of G2, V;
hereby
assume A1: G1 is finite-tcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-tcolorable by A1;
end;
assume G2 is finite-tcolorable;
then consider n such that
A2: G2 is n-tcolorable;
G1 is n-tcolorable by A2, Th169;
hence thesis;
end;
registration
let G2 be finite-tcolorable _Graph; let V;
cluster -> finite-tcolorable for addVertices of G2, V;
coherence by Th180;
end;
registration
let G2 be non finite-tcolorable _Graph; let V;
cluster -> non finite-tcolorable for addVertices of G2, V;
coherence by Th180;
end;
theorem
for v,e,w being object, G1 being addEdge of G2,v,e,w
st v <> w holds G1 is finite-tcolorable iff G2 is finite-tcolorable
proof
let v,e,w be object, G1 be addEdge of G2,v,e,w;
assume A1: v <> w;
hereby
assume A2: G1 is finite-tcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-tcolorable by A2;
end;
assume G2 is finite-tcolorable;
then consider n such that
A3: G2 is n-tcolorable;
G1 is (n+`2)-tcolorable by A1, A3, Th171;
hence thesis;
end;
theorem Th182:
for v,e,w being object, G1 being addAdjVertex of G2,v,e,w
holds G1 is finite-tcolorable iff G2 is finite-tcolorable
proof
let v,e,w be object, G1 be addAdjVertex of G2,v,e,w;
hereby
assume A1: G1 is finite-tcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-tcolorable by A1;
end;
assume G2 is finite-tcolorable;
then consider n such that
A2: G2 is n-tcolorable;
per cases;
suppose G2 is non edgeless;
then G1 is (n+`1)-tcolorable by A2, Th172;
hence thesis;
end;
suppose G2 is edgeless;
then G1 is 3-tcolorable by Th174;
hence thesis;
end;
end;
registration
let G2 be finite-tcolorable _Graph, v,e,w be object;
cluster -> finite-tcolorable for addAdjVertex of G2,v,e,w;
coherence by Th182;
end;
registration
let G2 be non finite-tcolorable _Graph, v,e,w be object;
cluster -> non finite-tcolorable for addAdjVertex of G2,v,e,w;
coherence by Th182;
end;
theorem Th183:
for v being object, V being finite set, G1 being addAdjVertexAll of G2,v,V
holds G1 is finite-tcolorable iff G2 is finite-tcolorable
proof
let v be object, V be finite set, G1 be addAdjVertexAll of G2,v,V;
hereby
assume A1: G1 is finite-tcolorable;
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-tcolorable by A1;
end;
assume G2 is finite-tcolorable;
then consider n such that
A2: G2 is n-tcolorable;
G1 is (n+`1+`card V)-tcolorable by A2, Th175;
hence thesis;
end;
registration
let G2 be finite-tcolorable _Graph, v be object; let V be finite set;
cluster -> finite-tcolorable for addAdjVertexAll of G2,v,V;
coherence by Th183;
end;
theorem Th184:
for F being PGraphMapping of G1,G2
st F is weak_SG-embedding & G2 is finite-tcolorable
holds G1 is finite-tcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is weak_SG-embedding & G2 is finite-tcolorable;
then consider n such that
A2: G2 is n-tcolorable;
G1 is n-tcolorable by A1, A2, Th176;
hence thesis;
end;
theorem Th185:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1 is finite-tcolorable iff G2 is finite-tcolorable
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
then reconsider F0 = F as one-to-one PGraphMapping of G1, G2;
F0" is isomorphism by A1, GLIB_010:75;
hence G1 is finite-tcolorable implies G2 is finite-tcolorable by Th184;
thus G2 is finite-tcolorable implies G1 is finite-tcolorable by A1, Th184;
end;
registration
let G be finite-tcolorable _Graph;
cluster G-isomorphic -> finite-tcolorable for _Graph;
coherence
proof
let H be _Graph;
assume H is G-isomorphic;
then consider F being PGraphMapping of G,H such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th185;
end;
end;
deffunc TColSet(_Graph) =
{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 :: chi double prime
meet { c where c is cardinal Subset of G.order()+`G.size()
: G is c-tcolorable };
coherence
proof
now
let a be set;
assume a in TColSet(G);
then consider c being cardinal Subset of G.order()+`G.size() such that
A1: a = c & G is c-tcolorable;
thus a is cardinal number by A1;
end;
hence thesis by GLIBPRE0:15;
end;
end;
theorem Th186:
G is loopless implies G is G.tChromaticNum()-tcolorable
proof
assume G is loopless;
then G is G.order()-vcolorable & G is G.size()-ecolorable by Th29, Th100;
then A1: G is (G.order()+`G.size())-tcolorable by Th163;
G.order()+`G.size() c= G.order()+`G.size();
then A2: G.order()+`G.size() in TColSet(G) by A1;
now
let a be set;
assume a in TColSet(G);
then consider c being cardinal Subset of G.order()+`G.size() such that
A3: a = c & G is c-tcolorable;
thus a is cardinal number by A3;
end;
then consider c being Cardinal such that
A4: c in TColSet(G) & c = G.tChromaticNum() by A2, GLIBPRE0:14;
consider c9 being cardinal Subset of G.order()+`G.size() such that
A5: c = c9 & G is c9-tcolorable by A4;
thus thesis by A4, A5;
end;
theorem Th187:
G is non loopless iff G.tChromaticNum() = 0
proof
hereby
assume A1: G is non loopless;
now
given x being object such that
A2: x in TColSet(G);
consider c being cardinal Subset of G.order()+`G.size() such that
A3: x = c & G is c-tcolorable by A2;
thus contradiction by A1, A3;
end;
hence G.tChromaticNum() = 0 by XBOOLE_0:def 1, SETFAM_1:1;
end;
assume A4: G.tChromaticNum() = 0 & G is loopless;
per cases;
suppose A5: TColSet(G) = {};
G is G.order()-vcolorable & G is G.size()-ecolorable by A4, Th29, Th100;
then A6: G is (G.order()+`G.size())-tcolorable by Th163;
G.order()+`G.size() c= G.order()+`G.size();
then G.order()+`G.size() in TColSet(G) by A6;
hence contradiction by A5;
end;
suppose A7: TColSet(G) <> {};
now
let a be set;
assume a in TColSet(G);
then consider c being cardinal Subset of G.order()+`G.size() such that
A8: a = c & G is c-tcolorable;
thus a is cardinal number by A8;
end;
then consider c being Cardinal such that
A9: c in TColSet(G) & c = G.tChromaticNum() by A7, GLIBPRE0:14;
consider c9 being cardinal Subset of G.order()+`G.size() such that
A10: c = c9 & G is c9-tcolorable by A9;
thus contradiction by A4, A9, A10;
end;
end;
registration
let G be loopless _Graph;
cluster G.tChromaticNum() -> non zero;
coherence by Th187;
end;
registration
let G be non loopless _Graph;
cluster G.tChromaticNum() -> zero;
coherence by Th187;
end;
theorem Th188:
G.tChromaticNum() c= G.order()+`G.size()
proof
per cases;
suppose G is non loopless;
then G.tChromaticNum() = 0;
hence thesis by XBOOLE_1:2;
end;
suppose G is loopless;
then G is G.order()-vcolorable & G is G.size()-ecolorable by Th29, Th100;
then A1: G is (G.order()+`G.size())-tcolorable by Th163;
G.order()+`G.size() c= G.order()+`G.size();
then G.order()+`G.size() in TColSet(G) by A1;
hence G.tChromaticNum() c= G.order()+`G.size() by SETFAM_1:3;
end;
end;
theorem Th189:
G is c-tcolorable implies G.tChromaticNum() c= c
proof
assume A1: G is c-tcolorable;
per cases;
suppose not G.order()+`G.size() in c;
then c c= G.order()+`G.size() by ORDINAL1:16;
then c in TColSet(G) by A1;
hence thesis by SETFAM_1:3;
end;
suppose G.order()+`G.size() in c;
then G.tChromaticNum() in c by Th188, ORDINAL1:12;
hence thesis by ORDINAL1:def 2;
end;
end;
theorem Th190:
(G is c-tcolorable & for d being Cardinal st G is d-tcolorable holds c c= d)
implies G.tChromaticNum() = c
proof
assume G is c-tcolorable;
then A1: G.tChromaticNum() c= c & G is loopless by Th189;
assume A2: for d being Cardinal st G is d-tcolorable holds c c= d;
G is G.order()-vcolorable & G is G.size()-ecolorable by A1, Th29, Th100;
then A3: G is (G.order()+`G.size())-tcolorable by Th163;
G.order()+`G.size() c= G.order()+`G.size();
then A4: G.order()+`G.size() in TColSet(G) by A3;
now
let x be set;
assume x in TColSet(G);
then consider d being cardinal Subset of G.order()+`G.size() such that
A5: x = d & G is d-tcolorable;
thus c c= x by A2, A5;
end;
then c c= G.tChromaticNum() by A4, SETFAM_1:5;
hence thesis by A1, XBOOLE_0:def 10;
end;
registration
let G be finite-tcolorable _Graph;
cluster G.tChromaticNum() -> natural;
coherence
proof
consider n such that
A1: G is n-tcolorable by Def12;
G.tChromaticNum() c= n by A1, Th189;
hence thesis;
end;
end;
definition
let G be finite-tcolorable _Graph;
redefine func G.tChromaticNum() -> Nat; :: redefines .tChromaticNum() (GLCOLO00, definition)
coherence;
end;
theorem
G.vChromaticNum() c= G.tChromaticNum()
proof
per cases;
suppose G is non loopless;
hence thesis;
end;
suppose G is loopless;
then G is G.tChromaticNum()-tcolorable by Th186;
hence thesis by Th57, Th162;
end;
end;
theorem Th192:
for G being loopless _Graph holds G.eChromaticNum() c= G.tChromaticNum()
proof
let G be loopless _Graph;
G is G.tChromaticNum()-tcolorable by Th186;
hence thesis by Th162, Lm15;
end;
theorem
G.tChromaticNum() c= G.vChromaticNum() +` G.eChromaticNum()
proof
per cases;
suppose G is non loopless;
then G.tChromaticNum() = 0;
hence thesis by XBOOLE_1:2;
end;
suppose G is loopless;
then G is G.vChromaticNum()-vcolorable G.eChromaticNum()-ecolorable
by Th54, Th122;
hence thesis by Th163, Th189;
end;
end;
theorem
for G being loopless _Graph holds G.supDegree()+`1 c= G.tChromaticNum()
proof
let G be loopless _Graph;
G is G.tChromaticNum()-tcolorable by Th186;
then consider t being proper TColoring of G such that
A1: card((rng t_V)\/rng t_E) c= G.tChromaticNum();
set D = the set of all v.degree() where v is Vertex of G;
per cases;
suppose G.supDegree() is finite;
then reconsider s = G.supDegree() as Nat;
now
let x be object;
assume A2: x in G.supDegree()+`1;
then reconsider k = x as Ordinal;
G.supDegree()+`1 = s+`1 .= s+1;
then A3: x in s+1 by A2;
then k in omega by ORDINAL1:10;
then reconsider k as Nat;
per cases;
suppose A4: k = 0;
assume not x in G.tChromaticNum();
hence contradiction by A4, ORDINAL1:16, XBOOLE_1:3;
end;
suppose 0 < k;
then reconsider l = k-1 as Nat by CHORD:1;
k in Segm(s+1) by A3;
then l+1 < s+1 by NAT_1:44;
then l in Segm(s) by XREAL_1:6, NAT_1:44;
then l in union D by GLIB_013:def 6;
then consider d being set such that
A5: l in d & d in D by TARSKI:def 4;
consider v being Vertex of G such that
A6: d = v.degree() by A5;
reconsider d as Cardinal by A6;
d c= s by A6, GLIB_013:35;
then reconsider d as Nat;
A7: rng(t_E|v.edgesInOut()) c= rng t_E by RELAT_1:70;
{t_V.v} misses t_E.:v.edgesInOut() by Def10, ZFMISC_1:50;
then A8: {t_V.v} misses rng(t_E|v.edgesInOut()) by RELAT_1:115;
v in the_Vertices_of G;
then v in dom t_V by PARTFUN1:def 2;
then {t_V.v} c= rng t_V by FUNCT_1:3, ZFMISC_1:31;
then A9: {t_V.v} \/ rng(t_E|v.edgesInOut()) c= (rng t_V) \/ rng t_E
by A7, XBOOLE_1:13;
card({t_V.v} \/ rng(t_E|v.edgesInOut()))
= card{t_V.v} +` card rng(t_E|v.edgesInOut()) by A8, CARD_2:35
.= card rng(t_E|v.edgesInOut()) +` 1 by CARD_1:30;
then card rng(t_E|v.edgesInOut()) +` 1 c= card((rng t_V) \/ rng t_E)
by A9, CARD_1:11;
then A10: card rng(t_E|v.edgesInOut()) +` 1 c= G.tChromaticNum()
by A1, XBOOLE_1:1;
t_E|v.edgesInOut() is one-to-one by Def5;
then card rng(t_E|v.edgesInOut())
= card dom(t_E|v.edgesInOut()) by CARD_1:70
.= card(dom t_E /\ v.edgesInOut()) by RELAT_1:61
.= card(the_Edges_of G /\ v.edgesInOut()) by PARTFUN1:def 2
.= card v.edgesInOut() by XBOOLE_1:28
.= d by A6, GLIB_000:19;
then A11: d+`1 c= G.tChromaticNum() by A10;
succ Segm l in succ Segm d by A5, ORDINAL3:3;
then Segm(l+1) in succ Segm d by NAT_1:38;
then Segm(l+1) in Segm(d+1) by NAT_1:38;
hence x in G.tChromaticNum() by A11;
end;
end;
hence thesis by TARSKI:def 3;
end;
suppose A12: G.supDegree() is infinite;
then 1 in G.supDegree() by CARD_3:85, TARSKI:def 3;
then A13: G.supDegree()+`1 = G.supDegree() by A12, CARD_2:76;
A14: G.supDegree() c= G.eChromaticNum() by Th123;
G.eChromaticNum() c= G.tChromaticNum() by Th192;
hence thesis by A13, A14, XBOOLE_1:1;
end;
end;
theorem Th195:
G is edgeless iff G.tChromaticNum() = 1
proof
hereby
assume A1: G is edgeless;
now
let c;
assume A2: G is c-tcolorable;
assume not 1 c= c;
then c in 1 by ORDINAL1:16;
then c = 0 by CARD_1:49, TARSKI:def 1;
hence contradiction by A2;
end;
hence G.tChromaticNum() = 1 by A1, Th190;
end;
assume G.tChromaticNum() = 1;
then G is 1-tcolorable by Th186, Th187;
hence thesis;
end;
theorem Th196:
for G being loopless non edgeless _Graph holds 3 c= G.tChromaticNum()
proof
let G be loopless non edgeless _Graph;
assume not 3 c= G.tChromaticNum();
then G.tChromaticNum() in 3 by ORDINAL1:16;
then per cases by CARD_1:51, ENUMSET1:def 1;
suppose G.tChromaticNum() = 0;
hence contradiction;
end;
suppose G.tChromaticNum() = 1;
hence contradiction by Th195;
end;
suppose G.tChromaticNum() = 2;
then G is 2-tcolorable by Th186;
then consider t being TColoring of G such that
A1: t is proper & card((rng t_V)\/rng t_E) c= 2;
2 c= card((rng t_V)\/rng t_E)
proof
assume not 2 c= card((rng t_V)\/rng t_E);
then card((rng t_V)\/rng t_E) in 2 by ORDINAL1:16;
then per cases by CARD_1:50, TARSKI:def 2;
suppose card((rng t_V)\/rng t_E) = 0;
hence contradiction;
end;
suppose card((rng t_V)\/rng t_E) = 1;
then G is 1-tcolorable by A1;
hence contradiction;
end;
end;
then consider a,b being object such that
A2: a<>b & (rng t_V)\/rng t_E = {a,b} by A1, XBOOLE_0:def 10, CARD_2:60;
set e = the Element of the_Edges_of G;
set v = (the_Source_of G).e, w = (the_Target_of G).e;
e Joins v,w,G & e Joins w,v,G by GLIB_000:def 13;
then A3: t_V.v <> t_V.w & t_V.v <> t_E.e & t_V.w <> t_E.e by A1, Th148;
e in the_Edges_of G;
then e in dom t_E by PARTFUN1:def 2;
then t_E.e in rng t_E by FUNCT_1:3;
then t_E.e in {a,b} by A2, XBOOLE_0:def 3;
then A4: t_E.e = a or t_E.e = b by TARSKI:def 2;
v in the_Vertices_of G & w in the_Vertices_of G;
then v in dom t_V & w in dom t_V by PARTFUN1:def 2;
then t_V.v in rng t_V & t_V.w in rng t_V by FUNCT_1:3;
then t_V.v in {a,b} & t_V.w in {a,b} by A2, XBOOLE_0:def 3;
then (t_V.v = a or t_V.v = b) & (t_V.w = a or t_V.w = b) by TARSKI:def 2;
hence contradiction by A3, A4;
end;
end;
theorem
for G being loopless _Graph, H being Subgraph of G
holds H.tChromaticNum() c= G.tChromaticNum()
proof
let G be loopless _Graph, H be Subgraph of G;
G is G.tChromaticNum()-tcolorable by Th186;
hence thesis by Th189;
end;
theorem
G1 == G2 implies G1.tChromaticNum() = G2.tChromaticNum()
proof
assume A1: G1 == G2;
per cases;
suppose G1 is non loopless;
then G1 is non loopless & G2 is non loopless by A1, GLIB_000:89;
then G1.tChromaticNum() = 0 & G2.tChromaticNum() = 0;
hence thesis;
end;
suppose G1 is loopless;
then G2 is G1.tChromaticNum()-tcolorable &
for c st G2 is c-tcolorable holds G1.tChromaticNum() c= c
by A1, Th167, Th186, Th189;
hence thesis by Th190;
end;
end;
theorem
for G2 being reverseEdgeDirections of G1, E
holds G1.tChromaticNum() = G2.tChromaticNum()
proof
let G2 be reverseEdgeDirections of G1, E;
per cases;
suppose G1 is non loopless;
then G1.tChromaticNum() = 0 & G2.tChromaticNum() = 0;
hence thesis;
end;
suppose G1 is loopless;
then G2 is G1.tChromaticNum()-tcolorable &
for c st G2 is c-tcolorable holds G1.tChromaticNum() c= c
by Th168, Th186, Th189;
hence thesis by Th190;
end;
end;
theorem
for G1 being addVertices of G2, V
holds G1.tChromaticNum() = G2.tChromaticNum()
proof
let G1 be addVertices of G2, V;
per cases;
suppose G2 is non loopless;
then G1.tChromaticNum() = 0 & G2.tChromaticNum() = 0;
hence thesis;
end;
suppose G2 is loopless;
then G1 is G2.tChromaticNum()-tcolorable &
for c st G1 is c-tcolorable holds G2.tChromaticNum() c= c
by Th169, Th186, Th189;
hence thesis by Th190;
end;
end;
theorem
for G2 being non edgeless _Graph, v,e,w being object
for G1 being addAdjVertex of G2,v,e,w
holds G1.tChromaticNum() c= G2.tChromaticNum() +` 1
proof
let G2 be non edgeless _Graph, v,e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
per cases;
suppose G1 is non loopless;
then G1.tChromaticNum() = 0;
hence thesis by XBOOLE_1:2;
end;
suppose G1 is loopless;
then G2 is loopless;
then A1: G2 is G2.tChromaticNum()-tcolorable by Th186;
G1 is (G2.tChromaticNum()+`1)-tcolorable by A1, Th172;
hence thesis by Th189;
end;
end;
theorem
for G2 being edgeless _Graph, v being Vertex of G2, 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
let G2 be edgeless _Graph, v be Vertex of G2, e,w be object;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not w in the_Vertices_of G2;
not e in the_Edges_of G2;
then G1 is non edgeless by A1, GLIB_006:131, GLIB_008:50;
then A2: 3 c= G1.tChromaticNum() by Th196;
G1 is 3-tcolorable by Th174;
then G1.tChromaticNum() c= 3 by Th189;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem
for G2 being edgeless _Graph, v,e being object, 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
let G2 be edgeless _Graph, v,e be object, w be Vertex of G2;
let G1 be addAdjVertex of G2,v,e,w;
assume A1: not v in the_Vertices_of G2;
not e in the_Edges_of G2;
then G1 is non edgeless by A1, GLIB_006:132, GLIB_008:50;
then A2: 3 c= G1.tChromaticNum() by Th196;
G1 is 3-tcolorable by Th174;
then G1.tChromaticNum() c= 3 by Th189;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem
for v being object, G1 being addAdjVertexAll of G2,v,V
holds G1.tChromaticNum() c= G2.tChromaticNum() +` 1 +` card V
proof
let v be object, G1 be addAdjVertexAll of G2,v,V;
per cases;
suppose G2 is non loopless;
then G1.tChromaticNum() = 0;
hence thesis by XBOOLE_1:2;
end;
suppose G2 is loopless;
then G1 is (G2.tChromaticNum()+`1+`card V)-tcolorable by Th186, Th175;
hence thesis by Th189;
end;
end;
theorem
for G1 being _Graph, G2 being loopless _Graph
for F being PGraphMapping of G1, G2 st F is weak_SG-embedding
holds G1.tChromaticNum() c= G2.tChromaticNum()
proof
let G1 be _Graph, G2 be loopless _Graph, F be PGraphMapping of G1, G2;
assume F is weak_SG-embedding;
then G1 is G2.tChromaticNum()-tcolorable by Th186, Th176;
hence thesis by Th189;
end;
theorem Th206:
for F being PGraphMapping of G1, G2
st F is isomorphism holds G1.tChromaticNum() = G2.tChromaticNum()
proof
let F be PGraphMapping of G1, G2;
assume A1: F is isomorphism;
per cases;
suppose G1 is non loopless;
then G1 is non loopless & G2 is non loopless by A1, GLIB_010:35;
then G1.tChromaticNum() = 0 & G2.tChromaticNum() = 0;
hence thesis;
end;
suppose A2: G1 is loopless;
now
G1 is G1.tChromaticNum()-tcolorable by A2, Th186;
hence G2 is G1.tChromaticNum()-tcolorable by A1, Th177;
let c;
assume G2 is c-tcolorable;
then G1 is c-tcolorable by A1, Th177;
hence G1.tChromaticNum() c= c by Th189;
end;
hence thesis by Th190;
end;
end;
theorem
for G2 being G1-isomorphic _Graph
holds G1.tChromaticNum() = G2.tChromaticNum()
proof
let G2 be G1-isomorphic _Graph;
consider F being PGraphMapping of G1, G2 such that
A1: F is isomorphism by GLIB_010:def 23;
thus thesis by A1, Th206;
end;