:: The {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received July 2, 2010
:: Copyright (c) 2010-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 MYCIELSK, FINSET_1, DILWORTH, CARD_1, ARYTM_3, ARYTM_1, FUNCT_1,
RELAT_1, RELAT_2, YELLOW_0, TARSKI, EQREL_1, CIRCUIT2, SUBSET_1,
COMBGRAS, NECKLACE, NEWTON, XXREAL_0, NAT_1, XBOOLE_0, ORDERS_2,
STRUCT_0, ZFMISC_1, FUNCT_2, NUMBERS, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, FINSET_1, SUBSET_1, STRUCT_0, ORDINAL1,
CARD_1, ORDERS_2, XCMPLX_0, XXREAL_0, XREAL_0, NAT_D, RELAT_1, RELSET_1,
RELAT_2, EQREL_1, FUNCT_1, FUNCT_2, NEWTON, YELLOW_0, NECKLACE, DILWORTH,
NUMBERS;
constructors NECKLACE, RELSET_1, NAT_1, NAT_D, NEWTON, YELLOW_0, DILWORTH,
DOMAIN_1;
registrations SUBSET_1, XBOOLE_0, STRUCT_0, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, CARD_1, RELSET_1, ORDINAL1, EQREL_1, NECKLA_3, FUNCT_2, FINSET_1,
DILWORTH, NEWTON, ORDERS_2;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, DILWORTH, NECKLACE;
equalities STRUCT_0, TARSKI, SUBSET_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, DILWORTH, NECKLACE;
theorems NEWTON, NAT_1, NAT_D, XREAL_0, XREAL_1, XXREAL_0, ORDINAL1, FUNCT_1,
DILWORTH, XBOOLE_0, XBOOLE_1, TARSKI, NECKLACE, PENCIL_1, ZFMISC_1,
ORDERS_2, EULER_1, CARD_2, CARD_1, YELLOW_0, RELSET_1, EQREL_1, FUNCT_2,
RELAT_1, FINSET_1, FINSEQ_4, RELAT_2, SUBSET_1, XTUPLE_0;
schemes RECDEF_1, NAT_1, CLASSES1, PRE_CIRC, FUNCT_1, FUNCT_2, DILWORTH;
begin :: MML Remarks
:: Note: PUA2MSS1:11 can be now proven without non empty for X
:: See func P | S below
begin :: Preliminaries
:: Facts that I could not find in MML.
defpred P[set] means not contradiction;
theorem :: TimesM:
for x, y, z being Real st 0 <= x holds x*(y-'z) = x*y -' x*z
proof let x, y, z be Real;
assume A1: x >= 0;
per cases;
suppose A2: y-z >= 0;
A3: x*(y-z) >= 0 by A1,A2;
thus x*(y-'z) = x*(y-z) by A2,XREAL_0:def 2
.= x*y - x*z
.= x*y -' x*z by A3,XREAL_0:def 2;
end;
suppose A4: y-z < 0;
per cases by A1;
suppose A5: x = 0;
thus x*(y-'z) = x*y -' x*z by A5,XREAL_1:232;
end;
suppose A6: x > 0;
x*(y-z) < 0 by A4,A6;
then A7: x*y - x*z < 0;
thus x*(y-'z) = x*0 by A4,XREAL_0:def 2
.= x*y -' x*z by A7,XREAL_0:def 2;
end;
end;
end;
theorem Th2: :: Nat0:
for x, y, z being Nat holds x in Segm y \ Segm z iff z <= x & x < y
proof
let x, y, z be Nat;
hereby assume
A1: x in Segm y \ Segm z;
not x in Segm z by A1,XBOOLE_0:def 5;
hence z <= x by NAT_1:44;
x in Segm y by A1,XBOOLE_0:def 5;
hence x < y by NAT_1:44;
end;
assume z <= x & x < y;
then x in Segm y & not x in Segm z by NAT_1:44;
hence x in Segm y \ Segm z by XBOOLE_0:def 5;
end;
theorem Th3: :: U5s:
for A, B, C, D, E, X being set
st X c= A or X c= B or X c= C or X c= D or X c= E
holds X c= A \/ B \/ C \/ D \/ E
proof
let A, B, C, D, E, X be set;
assume A1: X c= A or X c= B or X c= C or X c= D or X c= E;
per cases by A1;
suppose X c= A;
then X c= A \/ B by XBOOLE_1:10;
then X c= A \/ B \/ C by XBOOLE_1:10;
then X c= A \/ B \/ C \/ D by XBOOLE_1:10;
hence X c= A \/ B \/ C \/ D \/ E by XBOOLE_1:10;
end;
suppose X c= B;
then X c= A \/ B by XBOOLE_1:10;
then X c= A \/ B \/ C by XBOOLE_1:10;
then X c= A \/ B \/ C \/ D by XBOOLE_1:10;
hence X c= A \/ B \/ C \/ D \/ E by XBOOLE_1:10;
end;
suppose X c= C;
then X c= A \/ B \/ C by XBOOLE_1:10;
then X c= A \/ B \/ C \/ D by XBOOLE_1:10;
hence X c= A \/ B \/ C \/ D \/ E by XBOOLE_1:10;
end;
suppose X c= D;
then X c= A \/ B \/ C \/ D by XBOOLE_1:10;
hence X c= A \/ B \/ C \/ D \/ E by XBOOLE_1:10;
end;
suppose X c= E;
hence X c= A \/ B \/ C \/ D \/ E by XBOOLE_1:10;
end;
end;
theorem Th4: :: U5:
for A, B, C, D, E, x being set holds
x in A \/ B \/ C \/ D \/ E iff x in A or x in B or x in C or x in D or x in E
proof
let A, B, C, D, E, x be set;
hereby
assume x in A \/ B \/ C \/ D \/ E;
then x in A \/ B \/ C \/ D or x in E by XBOOLE_0:def 3;
then x in A \/ B \/ C or x in D or x in E by XBOOLE_0:def 3;
then x in A \/ B or x in C or x in D or x in E by XBOOLE_0:def 3;
hence x in A or x in B or x in C or x in D or x in E by XBOOLE_0:def 3;
end;
assume A1: x in A or x in B or x in C or x in D or x in E;
per cases by A1;
suppose x in A;
then x in A \/ B by XBOOLE_0:def 3;
then x in A \/ B \/ C by XBOOLE_0:def 3;
then x in A \/ B \/ C \/ D by XBOOLE_0:def 3;
hence x in A \/ B \/ C \/ D \/ E by XBOOLE_0:def 3;
end;
suppose x in B;
then x in A \/ B by XBOOLE_0:def 3;
then x in A \/ B \/ C by XBOOLE_0:def 3;
then x in A \/ B \/ C \/ D by XBOOLE_0:def 3;
hence x in A \/ B \/ C \/ D \/ E by XBOOLE_0:def 3;
end;
suppose x in C;
then x in A \/ B \/ C by XBOOLE_0:def 3;
then x in A \/ B \/ C \/ D by XBOOLE_0:def 3;
hence x in A \/ B \/ C \/ D \/ E by XBOOLE_0:def 3;
end;
suppose x in D;
then x in A \/ B \/ C \/ D by XBOOLE_0:def 3;
hence x in A \/ B \/ C \/ D \/ E by XBOOLE_0:def 3;
end;
suppose x in E;
hence x in A \/ B \/ C \/ D \/ E by XBOOLE_0:def 3;
end;
end;
theorem Th5: :: Sym0a:
for R being symmetric RelStr, x, y being set
st x in the carrier of R & y in the carrier of R &
[x,y] in the InternalRel of R
holds [y,x] in the InternalRel of R
by NECKLACE:def 3,RELAT_2:def 3;
theorem Th6: :: Sym0:
for R being symmetric RelStr, x, y being Element of R st x <= y holds y <= x
proof
let R be symmetric RelStr, x, y be Element of R; assume
A1: x <= y;
set cR = the carrier of R, iR = the InternalRel of R;
A2: iR is_symmetric_in cR by NECKLACE:def 3;
A3: [x,y] in iR by A1,ORDERS_2:def 5;
then x in cR & y in cR by ZFMISC_1:87;
then [y,x] in iR by A2,A3;
hence y <= x by ORDERS_2:def 5;
end;
begin :: Partitions
theorem Th7: :: Partcard:
for X being set, P being a_partition of X holds card P c= card X
proof
let X be set, P be a_partition of X;
defpred P[object,object] means
ex D1 being set st D1 = $1 & $2 = the Element of D1;
:: !!! ChoiceFunc
A1: for e being object st e in P ex u being object st P[e,u]
proof let e be object;
assume e in P;
reconsider ee = e as set by TARSKI:1;
take u = the Element of ee;
thus P[e,u];
end;
consider f being Function such that
A2: dom f = P and
A3: for e being object st e in P holds P[e,f.e] from CLASSES1:sch 1(A1);
A4: f is one-to-one proof
let x1, x2 be object such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f.x1 = f.x2;
A8: x1 <> {} by A2,A5;
A9: x2 <> {} by A2,A6;
reconsider xx1=x1, xx2=x2 as set by TARSKI:1;
P[x1,f.x1] & P[x2,f.x2] by A5,A6,A2,A3;
then f.x1 = the Element of xx1 & f.x2 = the Element of xx2;
then xx1 meets xx2 by A7,A8,A9,XBOOLE_0:3;
hence x1 = x2 by A5,A6,A2,EQREL_1:def 4;
end;
rng f c= X proof
let y be object;
assume y in rng f;
then consider x being object such that
A10: x in dom f and
A11: y = f.x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
P[x,f.x] by A2,A3,A10;
then
A12: f.x = the Element of x;
x <> {} by A2,A10;
then f.x in x by A12;
hence y in X by A10,A2,A11;
end;
hence card P c= card X by A2,A4,CARD_1:10;
end;
definition
let X be set, P be a_partition of X, S be Subset of X;
func P | S -> a_partition of S equals
{x /\ S where x is Element of P: x meets S};
:: Note: PUA2MSS1:11 can be now proven without non empty for X
:: replace?
coherence proof
set D = {x /\ S where x is Element of P: x meets S};
A1: D c= bool S proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in D;
then consider x being Element of P such that
A2: a = x /\ S and
x meets S;
aa c= S by A2,XBOOLE_1:17;
hence thesis;
end;
A3: union D = S proof
thus union D c= S proof
let x be object;
assume x in union D;
then consider Y being set such that
A4: x in Y and
A5: Y in D by TARSKI:def 4;
thus x in S by A4,A1,A5;
end;
thus S c= union D proof
let s be object;
assume A6: s in S;
then s in X;
then s in union P by EQREL_1:def 4;
then consider p being set such that
A7: s in p and
A8: p in P by TARSKI:def 4;
p meets S by A7,A6,XBOOLE_0:3;
then
A9: p /\ S in D by A8;
s in p /\ S by A7,A6,XBOOLE_0:def 4;
hence s in union D by A9,TARSKI:def 4;
end;
end;
now
let A be Subset of S;
assume A in D;
then consider x being Element of P such that
A10: A = x /\ S and
A11: x meets S;
consider z being object such that
A12: z in x and
A13: z in S by A11,XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A13;
reconsider Pp1 = P as a_partition of Xp1;
thus A<>{} by A12,A13,A10,XBOOLE_0:def 4;
let B be Subset of S;
assume B in D;
then consider y being Element of P such that
A14: B = y /\ S and y meets S;
A15: x in Pp1 & y in Pp1;
per cases by A15,EQREL_1:def 4;
suppose x = y;
hence A = B or A misses B by A10,A14;
end;
suppose x misses y;
hence A = B or A misses B by A10,A14,XBOOLE_1:76;
end;
end;
hence thesis by A1,A3,EQREL_1:def 4;
end;
end;
registration
let X be set;
cluster finite for a_partition of X;
existence proof
per cases;
suppose X = {};
hence thesis by EQREL_1:45;
end;
suppose X <> {};
then {X} is a_partition of X by EQREL_1:39;
hence thesis;
end;
end;
end;
registration
let X be set, P be finite a_partition of X, S be Subset of X;
cluster P | S -> finite;
coherence proof :: f: P -> P |(S) and rng is finite
defpred P[object,object] means
ex D1 being set st D1 = $1 & $2 = D1 /\ S;
A1: for e being object st e in P ex u being object st P[e,u]
proof let e be object;
assume e in P;
reconsider ee = e as set by TARSKI:1;
take ee /\ S;
thus thesis;
end;
consider f being Function such that
A2: dom f = P and
A3: for e being object st e in P holds P[e,f.e] from CLASSES1:sch 1(A1);
A4: rng f is finite by A2,FINSET_1:8;
P |(S) c= rng f proof
let x be object;
assume x in P |(S);
then consider xx being Element of P such that
A5: x = xx /\ S and
A6: xx meets S;
consider y being object such that y in xx and
A7: y in S by A6,XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A7;
A8: P is a_partition of Xp1;
then P[xx,f.xx] by A3;
then x = f.xx by A5;
hence x in rng f by A8,A2,FUNCT_1:def 3;
end;
hence thesis by A4;
end;
end;
theorem Th8: :: Tpart0:
for X being set, P being finite a_partition of X, S being Subset of X
holds card (P | S) <= card P
proof
let X be set, P be finite a_partition of X, S be Subset of X;
per cases;
suppose X = {}; then
S = {};
hence card (P | S) <= card P;
end;
suppose X <> {};
then reconsider Pp1 = P as finite non empty set;
defpred P[set] means $1 meets S;
deffunc F(set) = $1 /\ S;
A3: P | S = {F(x) where x is Element of Pp1: P[x]};
card (P | S) <= card Pp1 from DILWORTH:sch 1(A3);
hence thesis;
end;
end;
theorem Th9: :: Tpart1:
for X being set, P being finite a_partition of X, S being Subset of X
holds (for p being set st p in P holds p meets S)
iff card (P | S) = card P
proof
let X be set, P be finite a_partition of X, S be Subset of X;
per cases;
suppose X = {};
hence thesis;
end;
suppose A2: X <> {};
set PS = P | S;
reconsider Pp1 = P as finite non empty set by A2;
hereby
assume A3: for p being set st p in P holds p meets S;
set p = the Element of P;
p in Pp1;
then p meets S by A3;
then p /\ S in PS;
then reconsider PSp1 = PS as non empty finite set;
defpred P[object,object] means
ex D1 being set st D1 = $1 & $1 in P & $2 = D1 /\ S;
A4: for x being object st x in P ex y being object st y in PSp1 & P[x,y]
proof
let x be object;
assume A5: x in P;
reconsider xx=x as set by TARSKI:1;
take xx /\ S;
xx meets S by A5,A3;
hence thesis by A5;
end;
consider f being Function of P,PSp1 such that
A6: for x being object st x in P holds P[x,f.x] from FUNCT_2:sch 1(A4);
now
let x1,x2 be object such that
A7: x1 in P and
A8: x2 in P and
A9: f.x1 = f.x2;
reconsider xx1=x1, xx2=x2 as set by TARSKI:1;
P[x1,f.x1] by A7,A6;
then
A10: f.x1 = xx1 /\ S;
P[x2,f.x2] by A8,A6;
then
A11: f.x2 = xx2 /\ S;
xx1 meets S by A7,A3;
then f.x1 in PS by A10,A7;
then f.x1 <> {};
then consider x being object such that
A12: x in f.x1 by XBOOLE_0:def 1;
x in xx1 & x in xx2 by A12,A9,A10,A11,XBOOLE_0:def 4;
then xx1 meets xx2 by XBOOLE_0:3;
hence x1 = x2 by A7,A8,EQREL_1:def 4;
end;
then A13: f is one-to-one by FUNCT_2:19;
rng f = PSp1 proof
thus rng f c= PSp1 proof
let y be object;
assume y in rng f;
then consider x being object such that
A14: x in P and
A15: f.x = y by FUNCT_2:11;
reconsider x as set by TARSKI:1;
A16: x meets S by A3,A14;
P[x,f.x] by A14,A6;
then consider D1 being set such that
A17: D1 = x & x in P & f.x = D1 /\ S;
thus y in PSp1 by A15,A17,A16;
end;
thus PSp1 c= rng f proof
let y be object;
assume y in PSp1;
then consider p being Element of P such that
A18: y = p /\ S and p meets S;
A19: p in Pp1;
P[p,f.p] by A6,A19;
then f.p = p /\ S;
hence y in rng f by A18,A19,FUNCT_2:4;
end;
end;
then f is onto by FUNCT_2:def 3;
hence card (P | S) = card P by A13,EULER_1:11;
end;
assume A20: card (P | S) = card P;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in PS & $2 in Pp1 & $1 = D2 /\ S;
A21: for x being object st x in PS
ex y being object st y in Pp1 & P[x,y]
proof
let x be object;
assume A22: x in PS;
then consider p being Element of P such that
A23: x = p /\ S and p meets S;
take p;
thus thesis by A22,A23;
end;
consider f being Function of PS,Pp1 such that
A24: for x being object st x in PS holds P[x,f.x] from FUNCT_2:sch 1(A21);
A25: f is one-to-one proof
let x1,x2 be object such that
A26: x1 in dom f and
A27: x2 in dom f and
A28: f.x1 = f.x2;
A29: P[x2,f.x2] by A27,A24;
P[x1,f.x1] by A26,A24;
then x1 = f.x1 /\ S;
hence x1 = x2 by A28,A29;
end;
f is onto by A20,A25,FINSEQ_4:63; then
A30: rng f = P by FUNCT_2:def 3;
let p be set;
assume p in P;
then consider ps being object such that
A31: ps in dom f and
A32: p = f.ps by A30,FUNCT_1:def 3;
P[ps,f.ps] by A31,A24;
then
A33: ps = p /\ S by A32;
reconsider ps as set by TARSKI:1;
ps is non empty by A31;
then ex x being object st x in ps;
hence p meets S by A33;
end;
end;
theorem Th10: :: Tsr0:
for R being RelStr, C being Coloring of R, S being Subset of R
holds C | S is Coloring of subrelstr S
proof
let R be RelStr, C be Coloring of R, S be Subset of R;
set sS = subrelstr S;
A1: the carrier of sS = S by YELLOW_0:def 15;
now
let x be set;
assume x in C | S;
then consider c being Element of C such that
A2: x = c /\ S and
A3: c meets S;
consider z being object such that z in c and
A4: z in S by A3,XBOOLE_0:3;
A5: sS is non empty by A4,YELLOW_0:def 15;
A6: R is non empty by A4;
reconsider Rp1 = R as non empty RelStr by A4;
reconsider xp1= x as Subset of sS by A1,A2,XBOOLE_1:17;
xp1 is stable proof
let a, b be Element of sS such that
A7: a in xp1 and
A8: b in xp1 and
A9: a <> b;
A10: a in c & b in c by A7,A8,A2,XBOOLE_0:def 4;
reconsider ap1 = a, bp1 = b as Element of R by A5,A6,YELLOW_0:58;
C is Coloring of Rp1;
then c in C;
then reconsider cp1 = c as Subset of R;
A11: cp1 is stable by DILWORTH:def 12;
assume a <= b or b <= a;
then ap1 <= bp1 or bp1 <= ap1 by YELLOW_0:59;
hence contradiction by A9,A10,A11;
end;
hence x is StableSet of sS;
end;
hence C | S is Coloring of sS by A1,DILWORTH:def 12;
end;
begin :: Chromatic number and clique cover number
:: This section could be moved to DILWORTH or better yet to some
:: article with preliminaries where RelStr represents a graph.
:: But then some stuff from NECKLACE would have to be moved.
:: I decided not to move stuff around until there is much more
:: material and then a bigger reorganisation would be in place
:: 2009.08.06
definition
let R be RelStr; :: finitely_colorable sounds better
attr R is with_finite_chromatic# means :Def2:
ex C being Coloring of R st C is finite;
end;
registration
cluster with_finite_chromatic# for RelStr;
existence proof
take R = the empty RelStr;
reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
take S;
thus S is finite;
end;
end;
registration
cluster finite -> with_finite_chromatic# for RelStr;
coherence proof
let R be RelStr; set cR = the carrier of R;
assume A1: R is finite;
per cases;
suppose R is empty;
then reconsider S = {} as a_partition of cR by EQREL_1:45;
for x being set st x in S holds x is StableSet of R;
then reconsider S as Coloring of R by DILWORTH:def 12;
take S;
thus S is finite;
end;
suppose A2: R is non empty;
reconsider cRp1 = cR as finite non empty set by A2,A1;
set S = SmallestPartition cR;
deffunc F(set) = {$1};
A3: S = {F(x) where x is Element of cRp1: P[x]} by EQREL_1:37;
A4: {F(x) where x is Element of cRp1: P[x]} is finite from PRE_CIRC:sch 1;
now let z being set;
assume z in S;
then ex x being Element of cR st z = {x} by A3;
hence z is StableSet of R by A2,SUBSET_1:33;
end;
then reconsider S as Coloring of R by DILWORTH:def 12;
take S;
thus thesis by A4;
end;
end;
end;
registration
let R be with_finite_chromatic# RelStr;
cluster finite for Coloring of R;
existence by Def2;
end;
registration
let R be with_finite_chromatic# RelStr, S be Subset of R;
cluster subrelstr S -> with_finite_chromatic#;
coherence proof
set sS = subrelstr S;
consider C being Coloring of R such that
A1: C is finite by Def2;
A2: the carrier of sS = S by YELLOW_0:def 15;
reconsider CS = C | S as a_partition of S;
for x being set st x in CS holds x is StableSet of sS proof
let x be set;
assume x in CS;
then consider X being Element of C such that
A3: x = X /\ S and
A4: X meets S;
ex y being object st y in X & y in S by A4,XBOOLE_0:3;
then X is StableSet of R by DILWORTH:def 12;
hence x is StableSet of sS by A3,DILWORTH:31;
end;
then CS is Coloring of sS by A2,DILWORTH:def 12;
hence thesis by A1;
end;
end;
definition
let R be with_finite_chromatic# RelStr;
func chromatic# R -> Nat means :Def3:
(ex C being finite Coloring of R st card C = it)
& for C being finite Coloring of R holds it <= card C;
existence proof
defpred P[Nat] means ex C being finite Coloring of R st card C = $1;
consider C being Coloring of R such that
A1: C is finite by Def2;
card C = card C; then
A2: ex k being Nat st P[k] by A1;
consider n being Nat such that
A3: P[n] and
A4: for k being Nat st P[k] holds n <= k from NAT_1:sch 5(A2);
take n;
thus ex C being finite Coloring of R st card C = n by A3;
let C be finite Coloring of R;
thus n <= card C by A4;
end;
uniqueness proof
let it1, it2 be Nat such that
A5: ex C being finite Coloring of R st card C = it1 and
A6: for C being finite Coloring of R holds it1 <= card C and
A7: ex C being finite Coloring of R st card C = it2 and
A8: for C being finite Coloring of R holds it2 <= card C;
consider C1 being finite Coloring of R such that
A9: card C1 = it1 by A5;
consider C2 being finite Coloring of R such that
A10: card C2 = it2 by A7;
it1 <= card C2 & it2 <= card C1 by A6,A8;
hence it1 = it2 by A9,A10,XXREAL_0:1;
end;
end;
registration
let R be empty RelStr;
cluster chromatic# R -> empty;
coherence proof
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
thus thesis by A1;
end;
end;
registration
let R be non empty with_finite_chromatic# RelStr;
cluster chromatic# R -> positive;
coherence proof
ex C being finite Coloring of R st card C = chromatic# R by Def3;
hence thesis;
end;
end;
definition
let R be RelStr;
attr R is with_finite_cliquecover# means :Def4:
ex C being Clique-partition of R st C is finite;
end;
registration
cluster with_finite_cliquecover# for RelStr;
existence proof
take R = the empty RelStr;
reconsider S = {} as a_partition of the carrier of R by EQREL_1:45;
reconsider S as Clique-partition of R;
take S;
thus S is finite;
end;
end;
registration
cluster finite -> with_finite_cliquecover# for RelStr;
coherence proof
let R be RelStr; set cR = the carrier of R;
assume A1: R is finite;
per cases;
suppose R is empty;
then reconsider S = {} as a_partition of cR by EQREL_1:45;
for x being set st x in S holds x is Clique of R;
then reconsider S as Clique-partition of R by DILWORTH:def 11;
take S;
thus S is finite;
end;
suppose A2: R is non empty;
reconsider cRp1 = cR as finite non empty set by A2,A1;
set S = SmallestPartition cR;
deffunc F(set) = {$1};
A3: S = {F(x) where x is Element of cRp1: P[x]} by EQREL_1:37;
A4: {F(x) where x is Element of cRp1: P[x]} is finite from PRE_CIRC:sch 1;
now let z being set;
assume A5: z in S;
ex x being Element of cR st z = {x} by A5,A3;
hence z is Clique of R by A2,SUBSET_1:33;
end;
then reconsider S as Clique-partition of R by DILWORTH:def 11;
take S;
thus thesis by A4;
end;
end;
end;
registration
let R be with_finite_cliquecover# RelStr;
cluster finite for Clique-partition of R;
existence by Def4;
end;
registration
let R be with_finite_cliquecover# RelStr, S be Subset of R;
cluster subrelstr S -> with_finite_cliquecover#;
coherence proof
set sS = subrelstr S;
consider C being Clique-partition of R such that
A1: C is finite by Def4;
A2: the carrier of sS = S by YELLOW_0:def 15;
reconsider CS = C | S as a_partition of S;
for x being set st x in CS holds x is Clique of sS proof
let x be set;
assume x in CS;
then consider X being Element of C such that
A3: x = X /\ S and
A4: X meets S;
ex y being object st y in X & y in S by A4,XBOOLE_0:3;
then X is Clique of R by DILWORTH:def 11;
hence x is Clique of sS by A3,DILWORTH:29;
end;
then CS is Clique-partition of sS by A2,DILWORTH:def 11;
hence thesis by A1;
end;
end;
definition
let R be with_finite_cliquecover# RelStr;
func cliquecover# R -> Nat means :Def5:
(ex C being finite Clique-partition of R st card C = it)
& for C being finite Clique-partition of R holds it <= card C;
existence proof
defpred P[Nat] means ex C being finite Clique-partition of R st card C = $1;
consider C being Clique-partition of R such that
A1: C is finite by Def4;
card C = card C; then
A2: ex k being Nat st P[k] by A1;
consider n being Nat such that
A3: P[n] and
A4: for k being Nat st P[k] holds n <= k from NAT_1:sch 5(A2);
take n;
thus ex C being finite Clique-partition of R st card C = n by A3;
let C be finite Clique-partition of R;
thus n <= card C by A4;
end;
uniqueness proof
let it1, it2 be Nat such that
A5: ex C being finite Clique-partition of R st card C = it1 and
A6: for C being finite Clique-partition of R holds it1 <= card C and
A7: ex C being finite Clique-partition of R st card C = it2 and
A8: for C being finite Clique-partition of R holds it2 <= card C;
consider C1 being finite Clique-partition of R such that
A9: card C1 = it1 by A5;
consider C2 being finite Clique-partition of R such that
A10: card C2 = it2 by A7;
it1 <= card C2 & it2 <= card C1 by A6,A8;
hence it1 = it2 by A9,A10,XXREAL_0:1;
end;
end;
registration
let R be empty RelStr;
cluster cliquecover# R -> empty;
coherence proof
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
thus thesis by A1;
end;
end;
registration
let R be non empty with_finite_cliquecover# RelStr;
cluster cliquecover# R -> positive;
coherence proof
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
thus thesis by A1;
end;
end;
:: Note: for empty RelStr clique# = 0, stability# = 0, chromatic# = 0,
:: cliquecover# = 0 follows from clusters.
theorem Th11: :: Maxclique:
for R being finite RelStr holds clique# R <= card the carrier of R
proof
let R be finite RelStr;
consider C being finite Clique of R such that
A1: card C = clique# R by DILWORTH:def 4;
Segm card C c= Segm card the carrier of R by CARD_1:11;
hence clique# R <= card the carrier of R by A1,NAT_1:39;
end;
theorem :: Maxstability:
for R being finite RelStr holds stability# R <= card the carrier of R
proof
let R be finite RelStr;
consider C being finite StableSet of R such that
A1: card C = stability# R by DILWORTH:def 6;
Segm card C c= Segm card the carrier of R by CARD_1:11;
hence stability# R <= card the carrier of R by A1,NAT_1:39;
end;
theorem Th13: :: Maxchromatic:
for R being finite RelStr holds chromatic# R <= card the carrier of R
proof
let R be finite RelStr;
consider C being finite Coloring of R such that
A1: card C = chromatic# R by Def3;
Segm card C c= Segm card the carrier of R by Th7;
hence chromatic# R <= card the carrier of R by A1,NAT_1:39;
end;
theorem :: Maxclicover:
for R being finite RelStr holds cliquecover# R <= card the carrier of R
proof
let R be finite RelStr;
consider C being finite Clique-partition of R such that
A1: card C = cliquecover# R by Def5;
Segm card C c= Segm card the carrier of R by Th7;
hence cliquecover# R <= card the carrier of R by A1,NAT_1:39;
end;
theorem Th15: :: CliChr:
:: more general than DILWORTH:50 for finite RelStr
for R being with_finite_clique# with_finite_chromatic# RelStr
holds clique# R <= chromatic# R
proof
let P be with_finite_clique# with_finite_chromatic# RelStr;
assume A1: clique# P > chromatic# P;
consider A being Clique of P such that
A2: card A = clique# P by DILWORTH:def 4;
consider C being finite Coloring of P such that
A3: card C = chromatic# P by Def3;
card Segm card C = card C & card Segm card A = card A;
then A4: card C in card A by A3,A1,A2,NAT_1:41;
set cP = the carrier of P;
per cases;
suppose P is empty;
hence contradiction by A1;
end;
suppose A5: P is non empty;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in A & $2 in C & $1 in D2;
A6: for x being object st x in A ex y being object st y in C & P[x,y]
proof
let x be object; assume
A7: x in A; then
reconsider xp1 = x as Element of P;
cP is non empty by A5;
then xp1 in cP;
then x in union C by EQREL_1:def 4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def 4;
take y;
thus thesis by A7,A8,A9;
end;
consider f being Function of A, C such that
A10: for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A6);
consider x,y being object such that
A11: x in A and
A12: y in A and
A13: x <> y and
A14: f.x = f.y by A5,A4,FINSEQ_4:65;
f.x in C by A11,FUNCT_2:5; then
A15: f.x is StableSet of P by DILWORTH:def 12;
P[x,f.x] & P[y,f.y] by A11,A12,A10;
then x in f.x & y in f.x by A14;
hence contradiction by A15,A11,A12,A13,DILWORTH:15;
end;
end;
theorem :: StaCov:
:: more general than DILWORTH:46 for finite RelStr
for R being with_finite_stability# with_finite_cliquecover# RelStr
holds stability# R <= cliquecover# R
proof
let R be with_finite_stability# with_finite_cliquecover# RelStr;
assume A1: stability# R > cliquecover# R;
consider A being StableSet of R such that
A2: card A = stability# R by DILWORTH:def 6;
consider C being finite Clique-partition of R such that
A3: card C = cliquecover# R by Def5;
card Segm card C = card C & card Segm card A = card A;
then A4: card C in card A by A3,A1,A2,NAT_1:41;
set cR = the carrier of R;
per cases;
suppose R is empty;
hence contradiction by A1;
end;
suppose A5: R is non empty;
defpred P[object,object] means
ex D2 being set st D2 = $2 & $1 in A & $2 in C & $1 in D2;
A6: for x being object st x in A ex y being object st y in C & P[x,y]
proof
let x be object such that
A7: x in A;
reconsider xp1 = x as Element of R by A7;
cR is non empty by A5;
then xp1 in cR;
then x in union C by EQREL_1:def 4;
then consider y being set such that
A8: x in y and
A9: y in C by TARSKI:def 4;
take y;
thus thesis by A7,A8,A9;
end;
consider f being Function of A, C such that
A10: for x being object st x in A holds P[x,f.x] from FUNCT_2:sch 1(A6);
consider x,y being object such that
A11: x in A and
A12: y in A and
A13: x <> y and
A14: f.x = f.y by A5,A4,FINSEQ_4:65;
f.x in C by A11,FUNCT_2:5; then
A15: f.x is Clique of R by DILWORTH:def 11;
P[x,f.x] & P[y,f.y] by A11,A12,A10;
then x in f.x & y in f.x by A14;
hence contradiction by A15,A11,A12,A13,DILWORTH:15;
end;
end;
begin :: Complement
theorem Th17: :: DCompl:
for R being RelStr, x, y being Element of R,
a, b being Element of ComplRelStr R
st x = a & y = b & x <= y holds not a <= b
proof
let R be RelStr, x, y be Element of R,
a, b be Element of ComplRelStr R such that
A1: x = a and
A2: y = b;
set cR = the carrier of R, iR = the InternalRel of R;
set CR = ComplRelStr R;
set iCR = the InternalRel of CR;
A3: iCR = iR` \ id cR by NECKLACE:def 8;
assume x <= y;
then [x,y] in iR by ORDERS_2:def 5;
then not [x,y] in iR` by XBOOLE_0:def 5;
then not [x,y] in iCR by A3,XBOOLE_0:def 5;
hence not a <= b by A1,A2,ORDERS_2:def 5;
end;
theorem Th18: :: DCompl1:
for R being RelStr, x, y being Element of R,
a, b being Element of ComplRelStr R
st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds x <= y
proof
let R be RelStr, x, y be Element of R,
a, b be Element of ComplRelStr R such that
A1: x = a and
A2: y = b and
A3: x <> y and
A4: x in the carrier of R;
set cR = the carrier of R, iR = the InternalRel of R;
set CR = ComplRelStr R;
set iCR = the InternalRel of CR;
A5: iCR = iR` \ id cR by NECKLACE:def 8;
A6: [x,y] in [:cR,cR:] by A4,ZFMISC_1:def 2;
assume not a <= b;
then A7: not [x,y] in iCR by A1,A2,ORDERS_2:def 5;
not [x,y] in id cR by A3,RELAT_1:def 10;
then not [x,y] in iR` by A5,A7,XBOOLE_0:def 5;
then [x,y] in iR by A6,XBOOLE_0:def 5;
hence x <= y by ORDERS_2:def 5;
end;
registration
let R be finite RelStr;
cluster ComplRelStr R -> finite;
coherence proof
the carrier of R = the carrier of ComplRelStr R by NECKLACE:def 8;
hence thesis;
end;
end;
theorem Th19: :: CliStaCompl:
for R being symmetric RelStr, C being Clique of R
holds C is StableSet of ComplRelStr R
proof
let R be symmetric RelStr, C be Clique of R;
now
let x, y be Element of ComplRelStr R such that
A1: x in C and
A2: y in C and
A3: x <> y;
reconsider a = x, b = y as Element of R by NECKLACE:def 8;
a <= b or b <= a by A1,A2,A3,DILWORTH:6;
then a <= b & b <= a by Th6;
hence not x <= y & not y <= x by Th17;
end;
hence C is StableSet of ComplRelStr R by DILWORTH:def 2,NECKLACE:def 8;
end;
theorem Th20: :: CliComplSta:
for R being symmetric RelStr, C being Clique of ComplRelStr R
holds C is StableSet of R
proof
let R be symmetric RelStr, C be Clique of ComplRelStr R;
now
let x, y be Element of R such that
A1: x in C and
A2: y in C and
A3: x <> y;
reconsider a = x, b = y as Element of ComplRelStr R by NECKLACE:def 8;
a <= b or b <= a by A1,A2,A3,DILWORTH:6;
then a <= b & b <= a by Th6;
hence not x <= y & not y <= x by Th17;
end;
hence C is StableSet of R by DILWORTH:def 2,NECKLACE:def 8;
end;
theorem Th21: :: StaCliCompl:
for R being RelStr, C being StableSet of R holds C is Clique of ComplRelStr R
proof
let R be RelStr, C be StableSet of R;
set CR = ComplRelStr R;
A1: C is Subset of CR by NECKLACE:def 8;
now
let a, b be Element of CR such that
A2: a in C and
A3: b in C and
A4: a <> b;
reconsider ap1 = a, bp1 = b as Element of R by NECKLACE:def 8;
not ap1 <= bp1 & not bp1 <= ap1 by A2,A3,A4,DILWORTH:def 2;
hence a <= b or b <= a by A2,A4,Th18;
end;
hence C is Clique of ComplRelStr R by A1,DILWORTH:6;
end;
theorem Th22: :: StaComplCli:
for R being RelStr, C being StableSet of ComplRelStr R holds C is Clique of R
proof
let R be RelStr, C be StableSet of ComplRelStr R;
A1: the carrier of R = the carrier of ComplRelStr R by NECKLACE:def 8;
now
let a, b be Element of R such that
A2: a in C and
A3: b in C and
A4: a <> b;
reconsider ap1 = a, bp1 = b as Element of ComplRelStr R by NECKLACE:def 8;
not ap1 <= bp1 & not bp1 <= ap1 by A2,A3,A4,DILWORTH:def 2;
hence a <= b or b <= a by A4,A2,A1,Th18;
end;
hence C is Clique of R by DILWORTH:6,NECKLACE:def 8;
end;
registration
let R be with_finite_clique# RelStr;
cluster ComplRelStr R -> with_finite_stability#;
coherence proof
set CR = ComplRelStr R;
consider C be finite Clique of R such that
A1: for D being finite Clique of R holds card D <= card C by DILWORTH:def 3;
assume not thesis;
then
A2: for A being finite StableSet of CR
ex B being finite StableSet of CR st card B > card A;
defpred P[Nat] means
ex S being finite StableSet of CR st card S > $1;
consider B being finite StableSet of CR such that
A3: card B > card {}CR by A2;
A4: P[0] by A3;
A5: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
assume P[n];
then consider S being finite StableSet of CR such that
A6: card S > n;
consider T being finite StableSet of CR such that
A7: card T > card S by A2;
card S >= n+1 by A6,NAT_1:13;
then card T > n+1 by A7,XXREAL_0:2;
hence P[n+1];
end;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A5);
then consider S being finite StableSet of CR such that
A8: card S > card C;
S is Clique of R by Th22;
hence contradiction by A1,A8;
end;
end;
registration
let R be with_finite_stability# symmetric RelStr;
cluster ComplRelStr R -> with_finite_clique#;
coherence proof
set CR = ComplRelStr R;
consider C be finite StableSet of R such that
A1: for D being finite StableSet of R holds card D <= card C
by DILWORTH:def 5;
assume not thesis;
then
A2: for C being finite Clique of CR
ex D being finite Clique of CR st card D > card C;
defpred P[Nat] means
ex S being finite Clique of CR st card S > $1;
consider B being finite Clique of CR such that
A3: card B > card {}CR by A2;
A4: P[0] by A3;
A5: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
assume P[n];
then consider S being finite Clique of CR such that
A6: card S > n;
consider T being finite Clique of CR such that
A7: card T > card S by A2;
card S >= n+1 by A6,NAT_1:13;
then card T > n+1 by A7,XXREAL_0:2;
hence P[n+1];
end;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A5);
then consider S being finite Clique of CR such that
A8: card S > card C;
S is StableSet of R by Th20;
hence contradiction by A1,A8;
end;
end;
theorem Th23: :: cliRstaCR:
for R being with_finite_clique# symmetric RelStr
holds clique# R = stability# ComplRelStr R
proof
let R be with_finite_clique# symmetric RelStr;
set k = stability# ComplRelStr R;
consider A being finite StableSet of ComplRelStr R such that
A1: card(A) = k by DILWORTH:def 6;
A is Clique of R by Th22;
then
A2: ex C being finite Clique of R st card C = k by A1;
now let T be finite Clique of R;
T is StableSet of ComplRelStr R by Th19;
hence card T <= k by DILWORTH:def 6;
end;
hence clique# R = stability# ComplRelStr R by A2,DILWORTH:def 4;
end;
theorem :: staRcliCR:
for R being with_finite_stability# symmetric RelStr
holds stability# R = clique# ComplRelStr R
proof
let R be with_finite_stability# symmetric RelStr;
set CR = ComplRelStr R; set k = clique# CR;
consider A being finite Clique of CR such that
A1: card A = k by DILWORTH:def 4;
A is StableSet of R by Th20;
then
A2: ex C being finite StableSet of R st card C = k by A1;
now let T be finite StableSet of R;
T is Clique of CR by Th21;
hence card T <= k by DILWORTH:def 4;
end;
hence stability# R = clique# ComplRelStr R by A2,DILWORTH:def 6;
end;
theorem Th25: :: ChrClicoCompl:
for R being RelStr, C being Coloring of R
holds C is Clique-partition of ComplRelStr R
proof
let R be RelStr, C be Coloring of R;
A1: the carrier of R = the carrier of ComplRelStr R by NECKLACE:def 8;
now
let x be set;
assume x in C;
then x is StableSet of R by DILWORTH:def 12;
hence x is Clique of ComplRelStr R by Th21;
end;
hence C is Clique-partition of ComplRelStr R by A1,DILWORTH:def 11;
end;
theorem Th26: :: ClicoComplChr:
for R being symmetric RelStr, C being Clique-partition of ComplRelStr R
holds C is Coloring of R
proof
let R be symmetric RelStr, C being Clique-partition of ComplRelStr R;
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of CR by NECKLACE:def 8;
now
let x be set;
assume x in C;
then x is Clique of CR by DILWORTH:def 11;
hence x is StableSet of R by Th20;
end;
hence C is Coloring of R by A1,DILWORTH:def 12;
end;
theorem Th27: :: ClicoChrCompl:
for R being symmetric RelStr, C being Clique-partition of R
holds C is Coloring of ComplRelStr R
proof
let R be symmetric RelStr, C being Clique-partition of R;
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of CR by NECKLACE:def 8;
now
let x be set;
assume x in C;
then x is Clique of R by DILWORTH:def 11;
hence x is StableSet of CR by Th19;
end;
hence C is Coloring of ComplRelStr R by A1,DILWORTH:def 12;
end;
theorem Th28: :: ChrComplClico:
for R being RelStr, C being Coloring of ComplRelStr R
holds C is Clique-partition of R
proof
let R be RelStr, C being Coloring of ComplRelStr R;
set CR = ComplRelStr R;
A1: the carrier of R = the carrier of CR by NECKLACE:def 8;
now
let x be set;
assume x in C;
then x is StableSet of CR by DILWORTH:def 12;
hence x is Clique of R by Th22;
end;
hence C is Clique-partition of R by A1,DILWORTH:def 11;
end;
registration
let R be with_finite_chromatic# RelStr;
cluster ComplRelStr R -> with_finite_cliquecover#;
coherence proof
consider C being Coloring of R such that
A1: C is finite by Def2;
C is Clique-partition of ComplRelStr R by Th25;
hence thesis by A1;
end;
end;
registration
let R be with_finite_cliquecover# symmetric RelStr;
cluster ComplRelStr R -> with_finite_chromatic#;
coherence proof
consider C being Clique-partition of R such that
A1: C is finite by Def4;
C is Coloring of ComplRelStr R by Th27;
hence thesis by A1;
end;
end;
theorem Th29: :: chrRcovCR:
for R being with_finite_chromatic# symmetric RelStr
holds chromatic# R = cliquecover# ComplRelStr R
proof
let R be with_finite_chromatic# symmetric RelStr;
set CR = ComplRelStr R; set k = cliquecover# CR;
consider C being finite Clique-partition of CR such that
A1: card C = k by Def5;
C is Coloring of R by Th26;
then
A2: ex C being finite Coloring of R st card C = k by A1;
now
let C be finite Coloring of R;
assume A3: k > card C;
C is Clique-partition of CR by Th25;
hence contradiction by A3,Def5;
end;
hence chromatic# R = cliquecover# CR by A2,Def3;
end;
theorem :: covRchrCR:
for R being with_finite_cliquecover# symmetric RelStr
holds cliquecover# R = chromatic# ComplRelStr R
proof
let R be with_finite_cliquecover# symmetric RelStr;
set CR = ComplRelStr R; set k = chromatic# CR;
consider C being finite Coloring of CR such that
A1: card C = k by Def3;
C is Clique-partition of R by Th28;
then
A2: ex C being finite Clique-partition of R st card C = k by A1;
now
let C be finite Clique-partition of R;
assume A3: k > card C;
C is Coloring of CR by Th27;
hence contradiction by A3,Def3;
end;
hence cliquecover# R = chromatic# CR by A2,Def5;
end;
begin :: Adjacent set
definition
let R be RelStr, v be Element of R;
func Adjacent v -> Subset of R means :Def6:
for x being Element of R holds x in it iff x < v or v < x;
existence proof
set D = {x where x is Element of R : x < v or v < x};
set cR = the carrier of R, iR = the InternalRel of R;
D c= the carrier of R proof
let x be object;
assume x in D;
then consider a being Element of R such that
A1: x = a and
A2: a < v or v < a;
per cases by A2;
suppose a < v;
then a <= v by ORDERS_2:def 6;
then [a,v] in iR by ORDERS_2:def 5;
then [a,v] in [:cR,cR:];
hence x in the carrier of R by A1,ZFMISC_1:87;
end;
suppose v < a;
then v <= a by ORDERS_2:def 6;
then [v,a] in iR by ORDERS_2:def 5;
then [v,a] in [:cR,cR:];
hence x in the carrier of R by A1,ZFMISC_1:87;
end;
end;
then reconsider D as Subset of R;
take D;
let x be Element of R;
hereby
assume x in D;
then consider a being Element of R such that
A3: x = a and
A4: a < v or v < a;
thus x < v or v < x by A3,A4;
end;
assume x < v or v < x;
hence x in D;
end;
uniqueness proof
let it1, it2 be Subset of R such that
A5: for x being Element of R
holds x in it1 iff x < v or v < x and
A6: for x being Element of R
holds x in it2 iff x < v or v < x;
hereby
let x be object;
assume A7: x in it1;
then reconsider xp1 = x as Element of R;
xp1 < v or v < xp1 by A5,A7;
hence x in it2 by A6;
end;
let x be object;
assume A8: x in it2;
then reconsider xp1 = x as Element of R;
xp1 < v or v < xp1 by A6,A8;
hence x in it1 by A5;
end;
end;
theorem Th31: :: AdjCol:
for R being with_finite_chromatic# RelStr,
C being finite Coloring of R, c being set
st c in C & card C = chromatic# R
ex v being Element of R st v in c &
for d being Element of C st d <> c
ex w being Element of R st w in Adjacent(v) & w in d
proof
let R be with_finite_chromatic# RelStr,
C be finite Coloring of R, c be set such that
A1: c in C and
A2: card C = chromatic# R;
assume
A3: not thesis;
set cR = the carrier of R;
A4: union C = cR by EQREL_1:def 4;
reconsider c as Subset of cR by A1;
A5: c <> {} by A1;
set Cc = C\{c};
A6: c in {c} by TARSKI:def 1;
per cases;
suppose A7: Cc is empty;
consider v being object such that
A8: v in c by A5,XBOOLE_0:def 1;
reconsider v as Element of R by A8;
consider d being Element of C such that
A9: d <> c and for w being Element of R
holds not (w in Adjacent(v) & w in d) by A8,A3;
0 = card C - card{c} by A1,A7,CARD_1:27,EULER_1:4;
then 0+1 = card C - 1 +1 by CARD_1:30;
then consider x being object such that
A10: C = {x} by CARD_2:42;
c = x & d = x by A1,A10,TARSKI:def 1;
hence thesis by A9;
end;
suppose Cc is non empty;
then reconsider Cc as non empty set;
defpred P[object, object] means
ex D2 being set st D2 = $2 &
for vv being Element of cR st $1 = vv
holds $2 <> c & $2 in C &
for w being Element of R holds not (w in Adjacent(vv) & w in D2);
A11: for e being object st e in c ex u being object st P[e,u]
proof
let v be object such that
A12: v in c;
reconsider vv = v as Element of cR by A12;
consider d being Element of C such that
A13: d <> c and
A14: for w being Element of R
holds not (w in Adjacent(vv) & w in d) by A12,A3;
take d,d;
thus thesis by A13,A14,A1;
end;
consider r being Function such that
A15: dom r = c and
A16: for e being object st e in c holds P[e,r.e] from CLASSES1:sch 1(A11);
deffunc DF(set) = $1 \/ r"{$1};
reconsider Cc as finite non empty set;
set D = { DF(d) where d is Element of Cc : P[d] };
consider d being object such that
A17: d in Cc by XBOOLE_0:def 1;
reconsider d as set by TARSKI:1;
A18: d \/ r"{d} in D by A17;
A19: D c= bool cR proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in D;
then consider d being Element of Cc such that
A20: x = d \/ r"{d};
A21: r"{d} c= c by A15,RELAT_1:132;
A22: r"{d} c= cR by A21,XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then xx c= cR by A20,A22,XBOOLE_1:8;
hence x in bool cR;
end;
A23: union D = cR proof
thus union D c= cR proof
let x be object;
assume x in union D;
then consider Y being set such that
A24: x in Y and
A25: Y in D by TARSKI:def 4;
thus x in cR by A24,A25,A19;
end;
thus cR c= union D proof
let x be object;
assume A26: x in cR;
then consider d being set such that
A27: x in d and
A28: d in C by A4,TARSKI:def 4;
reconsider xp1 = x as Element of cR by A26;
per cases;
suppose A29: d = c;
then
A30: P[xp1,r.xp1] by A27,A16;
then r.xp1 <> c;
then A31: not r.xp1 in {c} by TARSKI:def 1;
r.xp1 in C by A30; then
A32: r.xp1 in Cc by A31,XBOOLE_0:def 5;
r.xp1 in {r.xp1} by TARSKI:def 1;
then x in r"{r.xp1} by A27,A29,A15,FUNCT_1:def 7;
then A33: x in r.xp1 \/ r"{r.xp1} by XBOOLE_0:def 3;
r.xp1 \/ r"{r.xp1} in D by A32;
hence x in union D by A33,TARSKI:def 4;
end;
suppose d <> c;
then not d in {c} by TARSKI:def 1;
then d in Cc by A28,XBOOLE_0:def 5;
then A34: d \/ r"{d} in D;
x in d \/ r"{d} by A27,XBOOLE_0:def 3;
hence x in union D by A34,TARSKI:def 4;
end;
end;
end;
A35: for A being Subset of cR st A in D holds A <> {} &
for B being Subset of cR st B in D holds A = B or A misses B proof
let A be Subset of cR;
assume A in D;
then consider da being Element of Cc such that
A36: A = da \/ r"{da};
A37: da in C by XBOOLE_0:def 5;
then da is non empty;
hence A <> {} by A36;
let B be Subset of cR;
assume B in D;
then consider db being Element of Cc such that
A38: B = db \/ r"{db};
A39: db in C by XBOOLE_0:def 5;
per cases;
suppose da = db;
hence A = B or A misses B by A36,A38;
end;
suppose A40: da <> db;
then A41: da misses db by A37,A39,EQREL_1:def 4;
A42: r"{da} misses r"{db} by A40,FUNCT_1:71,ZFMISC_1:11;
assume A <> B;
assume A meets B;
then consider x being object such that
A43: x in A and
A44: x in B by XBOOLE_0:3;
per cases by A43,A44,A36,A38,XBOOLE_0:def 3;
suppose x in da & x in db;
hence contradiction by A41,XBOOLE_0:3;
end;
suppose that A45: x in da and A46: x in r"{db};
A47: da <> c by A6,XBOOLE_0:def 5;
r"{db} c= c by A15,RELAT_1:132;
then da meets c by A45,A46,XBOOLE_0:3;
hence contradiction by A47,A37,A1,EQREL_1:def 4;
end;
suppose that A48: x in r"{da} and A49: x in db;
A50: db <> c by A6,XBOOLE_0:def 5;
r"{da} c= c by A15,RELAT_1:132;
then db meets c by A48,A49,XBOOLE_0:3;
hence contradiction by A50,A39,A1,EQREL_1:def 4;
end;
suppose x in r"{da} & x in r"{db};
hence contradiction by A42,XBOOLE_0:3;
end;
end;
end;
reconsider D as a_partition of cR by A19,A23,A35,EQREL_1:def 4;
now
let x be set;
assume A51: x in D;
then reconsider S = x as Subset of R;
consider d being Element of Cc such that
A52: x = d \/ r"{d} by A51;
A53: r"{d} c= c by A15,RELAT_1:132;
A54: d in C by XBOOLE_0:def 5;
A55: d is StableSet of R by A54,DILWORTH:def 12;
A56: c is StableSet of R by A1,DILWORTH:def 12;
S is stable proof
let a, b be Element of R such that
A57: a in S and
A58: b in S and
A59: a <> b;
per cases by A57,A58,A52,XBOOLE_0:def 3;
suppose a in d & b in d;
hence not a <= b & not b <= a by A55,A59,DILWORTH:def 2;
end;
suppose that A60: a in d and A61: b in r"{d};
r.b in {d} by A61,FUNCT_1:def 7;
then
A62: r.b = d by TARSKI:def 1;
P[b,r.b] by A53,A61,A16;
then not a in Adjacent(b) by A60,A62;
then not a < b & not b < a by Def6;
hence not a <= b & not b <= a by A59,ORDERS_2:def 6;
end;
suppose that A63: a in r"{d} and A64: b in d;
r.a in {d} by A63,FUNCT_1:def 7;
then
A65: r.a = d by TARSKI:def 1;
P[a,r.a] by A53,A63,A16;
then not b in Adjacent(a) by A64,A65;
then not a < b & not b < a by Def6;
hence not a <= b & not b <= a by A59,ORDERS_2:def 6;
end;
suppose a in r"{d} & b in r"{d};
hence not a <= b & not b <= a by A53,A56,A59,DILWORTH:def 2;
end;
end;
hence x is StableSet of R;
end;
then reconsider D as Coloring of R by DILWORTH:def 12;
card Cc = card C - card{c} by A1,EULER_1:4;
then card Cc + 1 = card C -1+1 by CARD_1:30;
then A66: card Cc < card C by NAT_1:13;
deffunc FS(set) = $1 \/ r"{$1};
consider s being Function such that
A67: dom s = Cc and
A68: for x being set st x in Cc holds s.x = FS(x) from FUNCT_1:sch 5;
A69: rng s c= D proof
let y be object;
assume y in rng s;
then consider d being object such that
A70: d in dom s and
A71: y = s.d by FUNCT_1:def 3;
reconsider d as set by TARSKI:1;
y = d \/ r"{d} by A67,A68,A70,A71;
hence y in D by A70,A67;
end;
then reconsider s as Function of Cc, D by A67,FUNCT_2:2;
A72: s is one-to-one proof
let x1, x2 be object such that
A73: x1 in dom s and
A74: x2 in dom s and
A75: s.x1 = s.x2;
reconsider x1,x2 as set by TARSKI:1;
A76: s.x1 = x1 \/ r"{x1} by A73,A68;
A77: s.x2 = x2 \/ r"{x2} by A74,A68;
A78: x1 c= x2 proof
let x be object;
assume A79: x in x1;
then A80: x in s.x1 by A76,XBOOLE_0:def 3;
per cases by A80,A75,A77,XBOOLE_0:def 3;
suppose x in x2;
hence thesis;
end;
suppose A81: x in r"{x2};
A82: r"{x2} c= dom r by RELAT_1:132;
A83: x1 in C by A73,XBOOLE_0:def 5;
then reconsider x1 as Subset of cR;
x1 meets c by A82,A81,A15,A79,XBOOLE_0:3;
then x1 = c by A83,A1,EQREL_1:def 4;
hence thesis by A6,A73,XBOOLE_0:def 5;
end;
end;
x2 c= x1 proof
let x be object;
assume A84: x in x2;
then A85: x in s.x2 by A77,XBOOLE_0:def 3;
per cases by A85,A75,A76,XBOOLE_0:def 3;
suppose x in x1;
hence thesis;
end;
suppose A86: x in r"{x1};
A87: r"{x1} c= dom r by RELAT_1:132;
A88: x2 in C by A74,XBOOLE_0:def 5;
then reconsider x2 as Subset of cR;
x2 meets c by A87,A86,A15,A84,XBOOLE_0:3;
then x2 = c by A88,A1,EQREL_1:def 4;
hence thesis by A6,A74,XBOOLE_0:def 5;
end;
end;
hence thesis by A78,XBOOLE_0:def 10;
end;
D c= rng s proof
let x be object;
assume x in D;
then consider d being Element of Cc such that
A89: x = d \/ r"{d};
s.d = d \/ r"{d} by A68;
hence x in rng s by A89,A67,FUNCT_1:def 3;
end;
then D = rng s by A69;
then s is onto by FUNCT_2:def 3;
then A90: card Cc = card D by A72,A18,EULER_1:11;
then D is finite;
hence contradiction by A66,A90,A2,Def3;
end;
end;
begin :: Natural numbers as vertices
definition
let n be Nat;
mode NatRelStr of n -> strict RelStr means :Def7:
the carrier of it = n;
existence proof
reconsider I = {} as Relation of n,n by RELSET_1:12;
take RelStr (# n, I #);
thus thesis;
end;
end;
registration
cluster -> empty for NatRelStr of 0;
coherence by Def7;
end;
registration
let n be non zero Nat;
cluster -> non empty for NatRelStr of n;
coherence by Def7;
end;
registration
let n be Nat;
cluster -> finite for NatRelStr of n;
coherence by Def7;
cluster irreflexive for NatRelStr of n;
existence proof
reconsider I = {} as Relation of n,n by RELSET_1:12;
set R = RelStr (# n, I #);
reconsider R as NatRelStr of n by Def7;
R is irreflexive ;
hence thesis;
end;
end;
definition
let n be Nat;
func CompleteRelStr n -> NatRelStr of n means :Def8:
the InternalRel of it = [: n, n :] \ id n;
existence proof
[:n,n:] c= [:n,n:];
then reconsider f = [:n,n:] as Relation of n;
reconsider R = RelStr(# n, f\id n #) as NatRelStr of n by Def7;
take R;
thus the InternalRel of R = [: n, n :] \ id n;
end;
uniqueness
proof
let C1, C2 be NatRelStr of n;
the carrier of C1 = n & the carrier of C2 = n by Def7;
hence thesis;
end;
end;
theorem Th32: :: CRS:
for n being Nat, x,y being set
st x in n & y in n
holds [x,y] in the InternalRel of CompleteRelStr n iff x <> y
proof
let n be Nat, x,y be set; assume
A1: x in n & y in n;
hereby
assume [x,y] in the InternalRel of CompleteRelStr n;
then [x,y] in [:n,n:] \ id n by Def8;
then not [x,y] in id n by XBOOLE_0:def 5;
hence x <> y by A1,RELAT_1:def 10;
end;
assume x <> y;
then [x,y] in [:n,n:] & not [x,y] in id n by A1,RELAT_1:def 10,ZFMISC_1:87;
then [x,y] in [:n,n:] \ id n by XBOOLE_0:def 5;
hence [x,y] in the InternalRel of CompleteRelStr n by Def8;
end;
registration
let n be Nat;
cluster CompleteRelStr n -> irreflexive symmetric;
coherence proof
set R = CompleteRelStr n;
set cR = the carrier of R, iR = the InternalRel of R;
A1: cR = n by Def7;
thus R is irreflexive by A1,Th32;
thus R is symmetric proof
let x, y be object;
assume x in cR & y in cR;
then A2: x in n & y in n by Def7;
assume [x,y] in iR;
hence thesis by A2,Th32;
end;
end;
end;
registration
let n be Nat;
cluster [#]CompleteRelStr n -> clique;
coherence
proof
set R = CompleteRelStr n;
set iR = the InternalRel of R;
let x, y be object;
assume x in [#]R & y in [#]R;
then A1: x in n & y in n by Def7;
assume x <> y;
hence [x,y] in iR or [y,x] in iR by A1,Th32;
end;
end;
theorem Th33: :: CompleteCli:
for n being Nat holds clique# CompleteRelStr n = n
proof
let n be Nat;
set R = CompleteRelStr n;
A1: card card n = card n;
[#]R = n by Def7;
then
A2: ex C being finite Clique of R st card C = n by A1;
for T being finite Clique of R holds card T <= n proof
let T be finite Clique of R;
card n = n;
then
A3: card the carrier of R = n by Def7;
A4: card T <= clique# R by DILWORTH:def 4;
clique# R <= n by A3,Th11;
hence thesis by A4,XXREAL_0:2;
end;
hence clique# R = n by A2,DILWORTH:def 4;
end;
theorem :: CompleteSta:
for n being non zero Nat holds stability# CompleteRelStr n = 1
proof
let n be non zero Nat;
set R = CompleteRelStr n;
[#]R is Clique of R;
hence stability# CompleteRelStr n = 1 by DILWORTH:20;
end;
theorem Th35: :: CompleteChr:
for n being Nat holds chromatic# CompleteRelStr n = n
proof
let n be Nat;
set R = CompleteRelStr n;
clique# R = n by Th33;
then
A1: n <= chromatic# R by Th15;
A2: chromatic# R <= card the carrier of R by Th13;
card n = n;
then card the carrier of R = n by Def7;
hence chromatic# CompleteRelStr n = n by A1,A2,XXREAL_0:1;
end;
theorem :: CompleteClico
for n being non zero Nat holds cliquecover# CompleteRelStr n = 1
proof
let n be non zero Nat;
set R = CompleteRelStr n; set cR = the carrier of R;
reconsider C = {cR} as a_partition of cR by EQREL_1:39;
A1: now let x be set;
assume x in C;
then x = [#]R by TARSKI:def 1;
hence x is Clique of R;
end;
A2: now
take C;
thus C is finite;
thus C is Clique-partition of R by A1,DILWORTH:def 11;
thus card C = 1 by CARD_1:30;
end;
now
let C be finite Clique-partition of R;
0+1 <= card C by NAT_1:13;
hence 1 <= card C;
end;
hence cliquecover# CompleteRelStr n = 1 by A2,Def5;
end;
begin :: Mycielskian of a graph
definition
let n be Nat, R be NatRelStr of n;
:: Note: no assumptions about R
func Mycielskian R -> NatRelStr of 2*n+1 means :Def9:
the InternalRel of it =
(the InternalRel of R)
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in the InternalRel of R }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in the InternalRel of R }
\/ [: {2*n}, 2*n \ n :]
\/ [: 2*n \ n, {2*n} :];
existence proof
set cR = the carrier of R, iR = the InternalRel of R;
set cMR = 2*n+1;
set iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :];
A1: cR = n by Def7;
n <= n+n by NAT_1:11;
then
A2: n < 2*n+1 by NAT_1:13;
iMR c= [:cMR, cMR:] proof
let z be object;
assume A3: z in iMR;
per cases by A3,Th4;
suppose z in iR;
then consider c, d being object such that
A4: c in Segm n and
A5: d in Segm n and
A6: z = [c,d] by ZFMISC_1:def 2,A1;
reconsider c, d as Nat by A4,A5;
c < n & d < n by A4,A5,NAT_1:44;
then c < cMR & d < cMR by A2,XXREAL_0:2;
then c in Segm cMR & d in Segm cMR by NAT_1:44;
hence z in [:cMR, cMR:] by A6,ZFMISC_1:def 2;
end;
suppose z in { [x,y+n] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A7: z = [x,y+n] and
A8: [x,y] in iR;
x in Segm n by A1,A8,ZFMISC_1:87;
then x < n by NAT_1:44;
then x < cMR by A2,XXREAL_0:2;
then A9: x in Segm cMR by NAT_1:44;
y in Segm n by A1,A8,ZFMISC_1:87;
then y < n by NAT_1:44;
then y+n < n+n by XREAL_1:6;
then y+n < 2*n+1 by NAT_1:13;
then y+n in Segm cMR by NAT_1:44;
hence z in [:cMR, cMR:] by A7,A9,ZFMISC_1:def 2;
end;
suppose z in { [x+n,y] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A10: z = [x+n,y] and
A11: [x,y] in iR;
y in Segm n by A1,A11,ZFMISC_1:87;
then y < n by NAT_1:44;
then y < cMR by A2,XXREAL_0:2;
then A12: y in Segm cMR by NAT_1:44;
x in Segm n by A1,A11,ZFMISC_1:87;
then x < n by NAT_1:44;
then x+n < n+n by XREAL_1:6;
then x+n < 2*n+1 by NAT_1:13;
then x+n in Segm cMR by NAT_1:44;
hence z in [:cMR, cMR:] by A10,A12,ZFMISC_1:def 2;
end;
suppose z in [: {2*n}, 2*n \ n :];
then consider c, d being object such that
A13: c in {2*n} and
A14: d in Segm(2*n) \ Segm n and
A15: z = [c,d] by ZFMISC_1:def 2;
A16: c = 2*n by A13,TARSKI:def 1;
reconsider c as Nat by A13,TARSKI:def 1;
c < 2*n+1 by A16,NAT_1:13;
then A17: c in Segm cMR by NAT_1:44;
reconsider d as Nat by A14;
d < 2*n by A14,Th2;
then d < cMR by NAT_1:13;
then d in Segm cMR by NAT_1:44;
hence z in [:cMR, cMR:] by A17,A15,ZFMISC_1:def 2;
end;
suppose z in [: 2*n \ n, {2*n} :];
then consider c, d being object such that
A18: c in Segm(2*n) \ Segm n and
A19: d in {2*n} and
A20: z = [c,d] by ZFMISC_1:def 2;
A21: d = 2*n by A19,TARSKI:def 1;
reconsider d as Nat by A19,TARSKI:def 1;
d < 2*n+1 by A21,NAT_1:13;
then A22: d in Segm cMR by NAT_1:44;
reconsider c as Nat by A18;
c < 2*n by A18,Th2;
then c < cMR by NAT_1:13;
then c in Segm cMR by NAT_1:44;
hence z in [:cMR, cMR:] by A22,A20,ZFMISC_1:def 2;
end;
end;
then reconsider iMR as Relation of cMR;
set MR = RelStr (# cMR, iMR #);
take MR;
thus the carrier of MR = 2*n+1; :: for NatRelStr
thus the InternalRel of MR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :];
end;
uniqueness
proof
let A, B be NatRelStr of 2*n+1;
the carrier of A = 2*n+1 & the carrier of B = 2*n+1 by Def7;
hence thesis;
end;
end;
theorem Th37: :: cMR0:
for n being Nat, R being NatRelStr of n
holds the carrier of R c= the carrier of Mycielskian R
proof
let n be Nat, R be NatRelStr of n;
A1: the carrier of R = n by Def7;
n <= n+n by NAT_1:12;
then n <= 2*n+1 by NAT_1:12;
then Segm n c= Segm(2*n+1) by NAT_1:39;
hence the carrier of R c= the carrier of Mycielskian R by A1,Def7;
end;
theorem Th38: :: iMR0:
for n being Nat, R being NatRelStr of n, x, y being Nat
st [x,y] in the InternalRel of Mycielskian R
holds x < n & y < n or x < n & n <= y & y < 2*n or n <= x & x < 2*n & y < n
or x = 2*n & n <= y & y < 2*n or n <= x & x < 2*n & y = 2*n
proof
let n be Nat, R be NatRelStr of n, a, b being Nat;
set cR = the carrier of R, iR = the InternalRel of R;
defpred LHS[] means [a,b] in the InternalRel of Mycielskian R;
defpred RHS[] means
a < n & b < n or a < n & n <= b & b < 2*n or n <= a & a < 2*n & b < n
or a = 2*n & n <= b & b < 2*n or n <= a & a < 2*n & b = 2*n;
A1: the InternalRel of Mycielskian R = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
assume A2: LHS[];
per cases by A2,A1,Th4;
suppose [a,b] in iR;
then a in cR & b in cR by ZFMISC_1:87;
then a in Segm n & b in Segm n by Def7;
hence RHS[] by NAT_1:44;
end;
suppose [a,b] in { [x,y+n] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A3: [x,y+n] = [a,b] and
A4: [x,y] in iR;
y in cR by A4,ZFMISC_1:87;
then y in Segm n by Def7;
then y < n by NAT_1:44;
then A5: y+n < n+n by XREAL_1:6;
x in cR by A4,ZFMISC_1:87;
then x in Segm n by Def7;
then x < n by NAT_1:44;
hence RHS[] by A5,A3,XTUPLE_0:1;
end;
suppose [a,b] in { [x+n,y] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A6: [x+n,y] = [a,b] and
A7: [x,y] in iR;
x in cR by A7,ZFMISC_1:87;
then x in Segm n by Def7;
then x < n by NAT_1:44;
then A8: x+n < n+n by XREAL_1:6;
y in cR by A7,ZFMISC_1:87;
then y in Segm n by Def7;
then y < n by NAT_1:44;
hence RHS[] by A8,A6,XTUPLE_0:1;
end;
suppose A9: [a,b] in [: {2*n}, 2*n \ n :];
A10: b in Segm(2*n) \ Segm n by A9,ZFMISC_1:87;
a in {2*n} by A9,ZFMISC_1:87;
hence RHS[] by A10,Th2,TARSKI:def 1;
end;
suppose A11: [a,b] in [: 2*n \ n, {2*n} :];
A12: a in Segm(2*n) \ Segm n by A11,ZFMISC_1:87;
b in {2*n} by A11,ZFMISC_1:87;
hence RHS[] by A12,Th2,TARSKI:def 1;
end;
end;
theorem Th39: :: iMR1ba:
for n being Nat, R being NatRelStr of n
holds the InternalRel of R c= the InternalRel of Mycielskian R
proof
let n be Nat, R be NatRelStr of n;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of MR;
iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
hence iR c= iMR by Th3;
end;
theorem Th40: :: iMR1b:
for n being Nat, R being NatRelStr of n, x, y being set
st x in Segm n & y in Segm n &
[x,y] in the InternalRel of Mycielskian R
holds [x,y] in the InternalRel of R
proof
let n be Nat, R be NatRelStr of n, a, b be set such that
A1: a in Segm n and
A2: b in Segm n and
A3: [a,b] in the InternalRel of Mycielskian R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of MR;
A4: iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
per cases by A3,A4,Th4;
suppose [a,b] in iR;
hence [a,b] in iR;
end;
suppose [a,b] in { [x,y+n] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A5: [a,b] = [x,y+n] and [x,y] in iR;
b = y+n by A5,XTUPLE_0:1;
then y+n < n by A2,NAT_1:44;
then y < n-n by XREAL_1:20;
then y < 0;
hence [a,b] in iR;
end;
suppose [a,b] in { [x+n,y] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A6: [a,b] = [x+n,y] and [x,y] in iR;
a = x+n by A6,XTUPLE_0:1;
then x+n < n by A1,NAT_1:44;
then x < n-n by XREAL_1:20;
then x < 0;
hence [a,b] in iR;
end;
suppose [a,b] in [: {2*n}, 2*n \ n :];
then consider c, d being object such that
A7: c in {2*n} and d in 2*n \ n and
A8: [a,b] = [c,d] by ZFMISC_1:def 2;
A9: c = 2*n by A7,TARSKI:def 1;
A10: c = a by A8,XTUPLE_0:1;
n+n < n by A1,A10,A9,NAT_1:44;
then n < n-n by XREAL_1:20;
then n < 0;
hence [a,b] in iR;
end;
suppose [a,b] in [: 2*n \ n, {2*n} :];
then consider c, d being object such that c in 2*n \ n and
A11: d in {2*n} and
A12: [a,b] = [c,d] by ZFMISC_1:def 2;
A13: d = 2*n by A11,TARSKI:def 1;
A14: d = b by A12,XTUPLE_0:1;
n+n < n by A2,A14,A13,NAT_1:44;
then n < n-n by XREAL_1:20;
then n < 0;
hence [a,b] in iR;
end;
end;
theorem Th41: :: iMR1a:
for n being Nat, R being NatRelStr of n, x, y being Nat
st [x,y] in the InternalRel of R holds
[x,y+n] in the InternalRel of Mycielskian R
& [x+n,y] in the InternalRel of Mycielskian R
proof
let n be Nat, R be NatRelStr of n, a, b be Nat such that
A1: [a,b] in the InternalRel of R;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of MR;
A2: iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
reconsider ap1 = a, bp1 = b as Element of NAT by ORDINAL1:def 12;
[ap1,bp1+n] in { [x,y+n] where x, y is Element of NAT : [x,y] in iR } by A1;
hence [a,b+n] in iMR by A2,Th4;
[ap1+n,bp1] in { [x+n,y] where x, y is Element of NAT : [x,y] in iR } by A1;
hence [a+n,b] in iMR by A2,Th4;
end;
theorem Th42: :: iMR1c:
for n being Nat, R being NatRelStr of n, x, y being Nat
st x in Segm n & [x,y+n] in the InternalRel of Mycielskian R
holds [x,y] in the InternalRel of R
proof
let n be Nat, R be NatRelStr of n, a, b be Nat;
set cR = the carrier of R, iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of MR;
assume that
A1: a in Segm n and
A2: [a,b+n] in iMR;
A3: iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
per cases by A2,A3,Th4;
suppose [a,b+n] in iR;
then b+n in cR by ZFMISC_1:87;
then b+n in Segm n by Def7;
then b+n < n by NAT_1:44;
then b < n-n by XREAL_1:20;
then b < 0;
hence [a,b] in iR;
end;
suppose [a,b+n] in { [x,y+n] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A4: [a,b+n] = [x,y+n] and
A5: [x,y] in iR;
b+n = y+n by A4,XTUPLE_0:1;
hence [a,b] in iR by A5,A4,XTUPLE_0:1;
end;
suppose [a,b+n] in { [x+n,y] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A6: [a,b+n] = [x+n,y] and
A7: [x,y] in iR;
b+n = y by A6,XTUPLE_0:1;
then b+n in cR by A7,ZFMISC_1:87;
then b+n in Segm n by Def7;
then b+n < n by NAT_1:44;
then b < n-n by XREAL_1:20;
then b < 0;
hence [a,b] in iR;
end;
suppose [a,b+n] in [: {2*n}, 2*n \ n :];
then consider c, d being object such that
A8: c in {2*n} and d in 2*n \ n and
A9: [a,b+n] = [c,d] by ZFMISC_1:def 2;
A10: c = 2*n by A8,TARSKI:def 1;
A11: c = a by A9,XTUPLE_0:1;
n+n < n by A1,A11,A10,NAT_1:44;
then n < n-n by XREAL_1:20;
then n < 0;
hence [a,b] in iR;
end;
suppose [a,b+n] in [: 2*n \ n, {2*n} :];
then consider c, d being object such that
A12: c in Segm(2*n) \ Segm n and d in {2*n} and
A13: [a,b+n] = [c,d] by ZFMISC_1:def 2;
c = a by A13,XTUPLE_0:1;
then n <= a by A12,Th2;
hence [a,b] in iR by A1,NAT_1:44;
end;
end;
theorem Th43: :: iMR1d:
for n being Nat, R being NatRelStr of n, x, y being Nat
st y in Segm n & [x+n,y] in the InternalRel of Mycielskian R
holds [x,y] in the InternalRel of R
proof
let n be Nat, R be NatRelStr of n, a, b be Nat;
set cR = the carrier of R, iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of MR;
assume that
A1: b in Segm n and
A2: [a+n,b] in iMR;
A3: iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
per cases by A2,A3,Th4;
suppose [a+n,b] in iR;
then a+n in cR by ZFMISC_1:87;
then a+n in Segm n by Def7;
then a+n < n by NAT_1:44;
then a < n-n by XREAL_1:20;
then a < 0;
hence [a,b] in iR;
end;
suppose [a+n,b] in { [x,y+n] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A4: [a+n,b] = [x,y+n] and
A5: [x,y] in iR;
a+n = x by A4,XTUPLE_0:1;
then a+n in cR by A5,ZFMISC_1:87;
then a+n in Segm n by Def7;
then a+n < n by NAT_1:44;
then a < n-n by XREAL_1:20;
then a < 0;
hence [a,b] in iR;
end;
suppose [a+n,b] in { [x+n,y] where x, y is Element of NAT : [x,y] in iR };
then consider x, y being Element of NAT such that
A6: [a+n,b] = [x+n,y] and
A7: [x,y] in iR;
a+n = x+n by A6,XTUPLE_0:1;
hence [a,b] in iR by A7,A6,XTUPLE_0:1;
end;
suppose [a+n,b] in [: {2*n}, 2*n \ n :];
then consider c, d being object such that c in {2*n} and
A8: d in Segm(2*n) \ Segm n and
A9: [a+n,b] = [c,d] by ZFMISC_1:def 2;
b = d by A9,XTUPLE_0:1;
then n <= b by A8,Th2;
hence [a,b] in iR by A1,NAT_1:44;
end;
suppose [a+n,b] in [: 2*n \ n, {2*n} :];
then consider c, d being object such that c in 2*n \ n and
A10: d in {2*n} and
A11: [a+n,b] = [c,d] by ZFMISC_1:def 2;
A12: d = 2*n by A10,TARSKI:def 1;
d = b by A11,XTUPLE_0:1;
then n+n < n by A1,A12,NAT_1:44;
then n < n-n by XREAL_1:20;
then n < 0;
hence [a,b] in iR;
end;
end;
theorem Th44: :: iMR1e:
for n being Nat, R being NatRelStr of n, m being Nat
st n <= m & m < 2*n
holds [m,2*n] in the InternalRel of Mycielskian R
& [2*n,m] in the InternalRel of Mycielskian R
proof
let n be Nat, R be NatRelStr of n, m be Nat such that
A1: n <= m and
A2: m < 2*n;
set iR = the InternalRel of R;
set MR = Mycielskian R;
set iMR = the InternalRel of MR;
A3: iMR = iR
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in iR }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in iR }
\/ [: {2*n}, 2*n \ n :] \/ [: 2*n \ n, {2*n} :] by Def9;
A4: m in Segm(2*n) \ Segm n by A1,A2,Th2;
A5: 2*n in {2*n} by TARSKI:def 1;
then [m,2*n] in [: 2*n \ n, {2*n} :] by A4,ZFMISC_1:def 2;
hence [m,2*n] in iMR by A3,XBOOLE_0:def 3;
[2*n,m] in [: {2*n}, 2*n \ n :] by A4,A5,ZFMISC_1:def 2;
hence [2*n,m] in iMR by A3,Th4;
end;
theorem Th45: :: Msubrel:
for n being Nat, R being NatRelStr of n, S being Subset of Mycielskian R
st S = n holds R = subrelstr S
proof
let n be Nat, R be NatRelStr of n, S be Subset of Mycielskian R such that
A1: S = n;
set cR = the carrier of R, iR = the InternalRel of R;
set sS = subrelstr S; set csS = the carrier of sS;
set isS = the InternalRel of sS;
set MR = Mycielskian R;
set cMR = the carrier of MR, iMR = the InternalRel of MR;
A2: cR = n by Def7;
A3: csS = n by A1,YELLOW_0:def 15;
A4: iR = isS proof
thus iR c= isS proof
let z be object;
assume A5: z in iR;
then consider x, y being object such that
A6: x in cR and
A7: y in cR and
A8: z = [x,y] by ZFMISC_1:def 2;
cR c= cMR by Th37;
then reconsider xMR = x, yMR = y as Element of MR by A6,A7;
reconsider xsS = x, ysS = y as Element of sS by A6,A7,Def7,A3;
iR c= iMR by Th39;
then xMR <= yMR by A5,A8,ORDERS_2:def 5;
then xsS <= ysS by A3,A2,A7,YELLOW_0:60;
hence z in isS by A8,ORDERS_2:def 5;
end;
thus isS c= iR proof
let z be object;
assume A9: z in isS;
then consider x, y being object such that
A10: x in Segm n and
A11: y in Segm n and
A12: z = [x,y] by ZFMISC_1:def 2,A3;
cR c= cMR by Th37;
then reconsider xMR = x, yMR = y as Element of MR by A10,A11,A2;
reconsider xsS = x, ysS = y as Element of sS by A10,A11,A3;
xsS <= ysS by A9,A12,ORDERS_2:def 5;
then xMR <= yMR by YELLOW_0:59;
then z in iMR by A12,ORDERS_2:def 5;
hence z in iR by A10,A11,A12,Th40;
end;
end;
thus R = subrelstr S by Def7,A3,A4;
end;
theorem Th46: :: MClique:
for n being Nat, R being irreflexive NatRelStr of n
st 2 <= clique# R holds clique# R = clique# Mycielskian R
proof
let n be Nat, R be irreflexive NatRelStr of n such that
A1: 2 <= clique# R and
A2: clique# R <> clique# Mycielskian R;
set cR = the carrier of R; set iR = the InternalRel of R;
set MR = Mycielskian R;
set cMR = the carrier of MR; set iMR = the InternalRel of MR;
set cnMR = clique# MR;
A3: cR = n by Def7;
A4: cR c= cMR by Th37;
consider C being finite Clique of R such that
A5: card C = clique# R by DILWORTH:def 4;
n <= n+n by NAT_1:11;
then n < 2*n+1 by NAT_1:13;
then Segm n c= Segm(2*n+1) by NAT_1:39;
then reconsider S = n as Subset of MR by Def7;
A6: R = subrelstr S by Th45;
then C is Clique of MR by DILWORTH:28;
then card C <= cnMR by DILWORTH:def 4;
then
A7: clique# R < cnMR by A2,A5,XXREAL_0:1;
then 2 < cnMR by A1,XXREAL_0:2;
then
A8: 2+1 <= cnMR by NAT_1:13;
consider D being finite Clique of MR such that
A9: card D = cnMR by DILWORTH:def 4;
per cases;
suppose A10: D c= n;
D /\ S is Clique of R by A6,DILWORTH:29;
then D is Clique of R by A10,XBOOLE_1:28;
hence contradiction by A9,A7,DILWORTH:def 4;
end;
suppose not D c= n;
then consider x being object such that
A11: x in D and
A12: not x in Segm n;
x in cMR by A11; then
A13: x in Segm(2*n+1) by Def7;
reconsider x as Nat by A13;
reconsider xp1 = x as Element of MR by A11;
A14: x >= n by A12,NAT_1:44;
x < 2*n+1 by A13,NAT_1:44;
then
A15: x <= 2*n by NAT_1:13;
A16: for y being set st y in D & x <> y holds y in Segm n proof
let y be set such that
A17: y in D and
A18: x <> y and
A19: not y in Segm n;
y in cMR by A17; then
A20: y in Segm(2*n+1) by Def7;
reconsider y as Nat by A20;
reconsider yp1 = y as Element of MR by A17;
A21: y >= n by A19,NAT_1:44;
y < 2*n+1 by A20,NAT_1:44;
then
A22: y <= 2*n by NAT_1:13;
set DD = D \ {x,y};
{x,y} c= D by A17,A11,ZFMISC_1:32;
then A23: card DD = card D - card {x,y} by CARD_2:44;
1+2-2 <= card D -2 by A8,A9,XREAL_1:9;
then 1 <= card DD by A23,A18,CARD_2:57;
then consider z being object such that
A24: z in DD by CARD_1:27,XBOOLE_0:def 1;
A25: z in D by A24,XBOOLE_0:def 5;
A26: z in cMR by A24;
reconsider zp1 = z as Element of MR by A24;
A27: z in Segm(2*n+1) by A26,Def7;
reconsider z as Nat by A27;
x in {x,y} by TARSKI:def 2;
then
A28: z <> x by A24,XBOOLE_0:def 5;
y in {x,y} by TARSKI:def 2;
then
A29: z <> y by A24,XBOOLE_0:def 5;
per cases by A15,A22,XXREAL_0:1;
suppose A30: x < 2*n & y < 2*n;
xp1 <= yp1 or yp1 <= xp1 by A11,A17,A18,DILWORTH:6;
then [x,y] in iMR or [y,x] in iMR by ORDERS_2:def 5;
hence contradiction by A14,A30,A21,Th38;
end;
suppose A31: x < 2*n & y = 2*n;
xp1 <= zp1 or zp1 <= xp1 by A28,A25,A11,DILWORTH:6;
then A32: [x,z] in iMR or [z,x] in iMR by ORDERS_2:def 5;
yp1 <= zp1 or zp1 <= yp1 by A29,A25,A17,DILWORTH:6;
then [y,z] in iMR or [z,y] in iMR by ORDERS_2:def 5;
then n <= z & z < 2*n by A31,A21,Th38;
hence contradiction by A32,A31,A14,Th38;
end;
suppose A33: x = 2*n & y < 2*n;
yp1 <= zp1 or zp1 <= yp1 by A29,A25,A17,DILWORTH:6;
then A34: [y,z] in iMR or [z,y] in iMR by ORDERS_2:def 5;
xp1 <= zp1 or zp1 <= xp1 by A28,A25,A11,DILWORTH:6;
then [x,z] in iMR or [z,x] in iMR by ORDERS_2:def 5;
then n <= z & z < 2*n by A33,A14,Th38;
hence contradiction by A34,A33,A21,Th38;
end;
suppose x = 2*n & y = 2*n;
hence contradiction by A18;
end;
end;
A35: card (D\{x}) = card D - card {x} by A11,EULER_1:4
.= card D - 1 by CARD_1:30;
per cases by A15,XXREAL_0:1;
suppose A36: x < 2*n;
consider xx being Nat such that
A37: x = n+xx by A14,NAT_1:10;
n + xx < n + n by A36,A37;
then A38: xx < n by XREAL_1:6;
then A39: xx in Segm n by NAT_1:44;
reconsider xxp1 = xx as Element of MR by A39,A4,A3;
A40: now
assume xx in D;
then xp1 <= xxp1 or xxp1 <= xp1 by A11,A38,A14,DILWORTH:6;
then [x,xx] in iMR or [xx,x] in iMR by ORDERS_2:def 5;
then [xx,xx] in iR or [xx,xx] in iR by A39,A37,Th42,Th43;
hence contradiction by A39,A3,NECKLACE:def 5;
end;
set DD = (D\{x}) \/ {xx};
DD c= cR proof
let a be object;
assume a in DD;
then a in D\{x} or a in {xx} by XBOOLE_0:def 3;
then a in D & not a in {x} or a = xx
by TARSKI:def 1,XBOOLE_0:def 5;
then a in D & a <> x or a = xx by TARSKI:def 1;
hence a in cR by A38,A16,A3,NAT_1:44;
end;
then reconsider DD as Subset of R;
now
let a, b be Element of R such that
A41: a in DD and
A42: b in DD and
A43: a <> b;
a in D\{x} or a in {xx} by A41,XBOOLE_0:def 3;
then
A44
: a in D & not a in {x} or a = xx by TARSKI:def 1,XBOOLE_0:def 5;
b in D\{x} or b in {xx} by A42,XBOOLE_0:def 3;
then
A45
: b in D & not b in {x} or b = xx by TARSKI:def 1,XBOOLE_0:def 5;
A46: a in cR & b in cR by A41;
then a in Segm n & b in Segm n by A3;
then reconsider an = a, bn = b as Nat;
reconsider ap1 = a, bp1 = b as Element of MR by A46,A4;
per cases by A43,A44,A45,TARSKI:def 1;
suppose A47: a in D & a <> x & b in D & b <> x;
ap1 <= bp1 or bp1 <= ap1 by A47,A43,DILWORTH:6;
hence a <= b or b <= a by A6,A41,YELLOW_0:60;
end;
suppose A48: a in D & a <> x & b = xx;
ap1 <= xp1 or xp1 <= ap1 by A48,A11,DILWORTH:6;
then [ap1,x] in iMR or [x,ap1] in iMR by ORDERS_2:def 5;
then [an, xx] in iR or [xx,an] in iR
by A3,A37,Th42,Th43,A39;
hence a <= b or b <= a by A48,ORDERS_2:def 5;
end;
suppose A49: a = xx & b in D & b <> x;
bp1 <= xp1 or xp1 <= bp1 by A49,A11,DILWORTH:6;
then [bp1,x] in iMR or [x,bp1] in iMR by ORDERS_2:def 5;
then [bn, xx] in iR or [xx,bn] in iR
by A3,A37,Th42,Th43,A39;
hence a <= b or b <= a by A49,ORDERS_2:def 5;
end;
end;
then reconsider DD as Clique of R by DILWORTH:6;
A50: not xx in D\{x} by A40,XBOOLE_0:def 5;
card DD = card D - 1 + 1 by A50,A35,CARD_2:41 .= card D;
hence contradiction by A9,A7,DILWORTH:def 4;
end;
suppose A51: x = 2*n;
2+1-1 <= card D -1 by A9,A8,XREAL_1:9;
then Segm 2 c= Segm card (D\{x}) by A35,NAT_1:39;
then consider y, z being object such that
A52: y in D\{x} and z in D\{x} and y <> z by PENCIL_1:2;
A53: y in D by A52,ZFMISC_1:56;
A54: x <> y by A52,ZFMISC_1:56;
y in the carrier of MR by A52;
then y in Segm(2*n+1) by Def7;
then reconsider y as Nat;
reconsider yp1 = y as Element of MR by A52;
yp1 <= xp1 or xp1 <= yp1 by A54,A53,A11,DILWORTH:6;
then A55: [y,x] in iMR or [x,y] in iMR by ORDERS_2:def 5;
y in Segm n by A16,A53,A54;
then A56: y < n by NAT_1:44;
n <= n+n by NAT_1:11;
hence contradiction by A55,A51,A56,Th38;
end;
end;
end;
theorem Th47: :: Tchro0:
for R being with_finite_chromatic# RelStr, S being Subset of R
holds chromatic# R >= chromatic# subrelstr S
proof
let R be with_finite_chromatic# RelStr, S be Subset of R;
consider C be finite Coloring of R such that
A1: card C = chromatic# R by Def3;
C | S is Coloring of subrelstr S by Th10;
then
A2: card (C | S) >= chromatic# subrelstr S by Def3;
card C >= card (C | S) by Th8;
hence chromatic# R >= chromatic# subrelstr S by A1,A2,XXREAL_0:2;
end;
theorem Th48: :: :: Mchromatic: :: even when n = 0 or n = 1 and then
:: Mycielskian n = 2 is compl(P_3) (Thanks Lorna)
:: and if we continue we have disconnected graphs.
for n being Nat, R being irreflexive NatRelStr of n
holds chromatic# Mycielskian R = 1 + chromatic# R
proof
let n be Nat, R be irreflexive NatRelStr of n;
set cR = the carrier of R, iR = the InternalRel of R; set cnR = chromatic# R;
set MR = Mycielskian R; set cnMR = chromatic# MR;
set cMR = the carrier of MR, iMR = the InternalRel of MR;
A1: cR = Segm n by Def7;
A2: ex C being finite Coloring of MR st card C = 1+cnR proof
consider C being finite Coloring of R such that
A3: card C = cnR by Def3;
defpred P[object,object] means
ex D1 being set st D1 = $1 &
$2 = { m+n where m is Element of NAT : m in D1 };
A4: for e being object st e in C ex u being object st P[e,u]
proof let e be object such that
e in C;
reconsider ee = e as set by TARSKI:1;
take u = { m+n where m is Element of NAT : m in ee };
thus thesis;
end;
consider r being Function such that dom r = C and
A5: for e being object st e in C holds P[e,r.e] from CLASSES1:sch 1(A4);
set D = { d \/ r.d where d is Element of C : d in C };
A6: card D = card C proof
per cases;
suppose A7: D is empty;
now assume C is non empty;
then consider c being object such that
A8: c in C;
reconsider c as set by TARSKI:1;
c \/ r.c in D by A8;
hence contradiction by A7;
end;
hence thesis by A7;
end;
suppose A9: D is non empty;
defpred R[object,object] means
ex D1 being set st D1 = $1 & $2 = D1 \/ r.$1;
A10: for e being object st e in C ex u being object st R[e,u]
proof let e be object such that
e in C;
reconsider ee=e as set by TARSKI:1;
take u = ee \/ r.e;
thus thesis;
end;
consider s being Function such that
A11: dom s = C and
A12: for e being object st e in C holds R[e,s.e] from CLASSES1:sch 1(A10);
A13: rng s c= D proof
let y be object;
assume y in rng s;
then consider x being object such that
A14: x in dom s and
A15: y = s.x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
R[x,s.x] by A14,A11,A12;
then y = x \/ r.x by A15;
hence y in D by A14,A11;
end;
then reconsider s as Function of C, D by A11,FUNCT_2:2;
D c= rng s proof
let x be object;
assume x in D;
then consider c being Element of C such that
A16: x = c \/ r.c and
A17: c in C;
R[c,s.c] by A17,A12;
then x = s.c by A16;
hence x in rng s by A17,A11,FUNCT_1:def 3;
end;
then rng s = D by A13;
then
A18: s is onto by FUNCT_2:def 3;
s is one-to-one proof
let x1,x2 be object such that
A19: x1 in dom s and
A20: x2 in dom s and
A21: s.x1 = s.x2;
reconsider x1, x2 as set by TARSKI:1;
R[x1,s.x1] by A19,A12;
then
A22: s.x1 = x1 \/ r.x1;
R[x2,s.x2] by A20,A12;
then
A23: s.x2 = x2 \/ r.x2;
A24: x1 c= x2 proof
let x be object;
assume A25: x in x1;
A26: x in s.x1 by A22,A25,XBOOLE_0:def 3;
per cases by A26,A21,A23,XBOOLE_0:def 3;
suppose x in x2;
hence thesis;
end;
suppose
A27: x in r.x2;
P[x2,r.x2] by A5,A20;
then x in { m+n where m is Element of NAT : m in x2 }
by A27;
then consider m being Element of NAT such that
A28: x = m+n and m in x2;
m+n in Segm(0+n) by A25,A28,A19,A11,A1;
then m+n < 0+n by NAT_1:44;
hence thesis by XREAL_1:6;
end;
end;
x2 c= x1 proof
let x be object;
assume A29: x in x2;
A30: x in s.x2 by A23,A29,XBOOLE_0:def 3;
per cases by A30,A21,A22,XBOOLE_0:def 3;
suppose x in x1;
hence thesis;
end;
suppose
A31: x in r.x1;
P[x1,r.x1] by A5,A19;
then x in { m+n where m is Element of NAT : m in x1 }
by A31;
then consider m being Element of NAT such that
A32: x = m+n and m in x1;
m+n in Segm(0+n) by A29,A32,A20,A11,A1;
then m+n < 0+n by NAT_1:44;
hence thesis by XREAL_1:6;
end;
end;
hence thesis by A24,XBOOLE_0:def 10;
end;
hence thesis by A18,A9,EULER_1:11;
end;
end;
then
A33: D is finite;
set E = D \/ {{2*n}};
A34: union E c= cMR proof
let x be object;
assume x in union E;
then consider Y being set such that
A35: x in Y and
A36: Y in E by TARSKI:def 4;
per cases by A36,XBOOLE_0:def 3;
suppose Y in D;
then consider d being Element of C such that
A37: Y = d \/ r.d and
A38: d in C;
P[d,r.d] by A38,A5;
then
A39: r.d = { m+n where m is Element of NAT : m in d };
per cases by A35,A37,XBOOLE_0:def 3;
suppose A40: x in d;
then x in Segm n by A38,A1;
then reconsider a = x as Nat;
a in Segm n by A40,A38,A1;
then a < n by NAT_1:44;
then a+0 < n+n by XREAL_1:8;
then a < 2*n+1 by NAT_1:13;
then a in Segm(2*n+1) by NAT_1:44;
hence x in cMR by Def7;
end;
suppose x in r.d;
then consider m being Element of NAT such that
A41: x = m+n and
A42: m in d by A39;
m in Segm n by A42,A38,A1;
then m < n by NAT_1:44;
then m+n < n+n by XREAL_1:6;
then m+n < 2*n + 1 by NAT_1:13;
then x in Segm(2*n+1) by A41,NAT_1:44;
hence x in cMR by Def7;
end;
end;
suppose Y in {{2*n}};
then Y = {2*n} by TARSKI:def 1;
then A43: x = 2*n by A35,TARSKI:def 1;
2*n < 2*n+1 by NAT_1:13;
then 2*n in Segm(2*n+1) by NAT_1:44;
hence x in cMR by A43,Def7;
end;
end;
A44: E c= bool cMR proof
let X be object;
reconsider XX=X as set by TARSKI:1;
assume A45: X in E;
XX c= cMR proof
let x be object;
assume x in XX;
then x in union E by A45,TARSKI:def 4;
hence x in cMR by A34;
end;
hence X in bool cMR;
end;
A46: union E = cMR proof
thus union E c= cMR by A34;
thus cMR c= union E proof
let x be object;
assume x in cMR;
then A47: x in Segm(2*n+1) by Def7;
then reconsider a = x as Nat;
a < 2*n+1 by A47,NAT_1:44;
then A48: a <= 2*n by NAT_1:13;
per cases;
suppose a < n;
then a in Segm n by NAT_1:44;
then a in union C by A1,EQREL_1:def 4;
then consider c being set such that
A49: a in c and
A50: c in C by TARSKI:def 4;
A51: x in c \/ r.c by A49,XBOOLE_0:def 3;
c \/ r.c in D by A50;
then c \/ r.c in E by XBOOLE_0:def 3;
hence x in union E by A51,TARSKI:def 4;
end;
suppose A52: a >= n;
per cases by A48,XXREAL_0:1;
suppose A53: a < n+n;
consider b being Nat such that
A54: a = n + b by A52,NAT_1:10;
reconsider b as Element of NAT by ORDINAL1:def 12;
b < n by A54,A53,XREAL_1:6;
then b in Segm n by NAT_1:44;
then b in union C by EQREL_1:def 4,A1;
then consider c being set such that
A55: b in c and
A56: c in C by TARSKI:def 4;
P[c,r.c] by A56,A5;
then r.c = { m+n where m is Element of NAT : m in c };
then a in r.c by A55,A54;
then A57: x in c \/ r.c by XBOOLE_0:def 3;
c \/ r.c in D by A56;
then c \/ r.c in E by XBOOLE_0:def 3;
hence x in union E by A57,TARSKI:def 4;
end;
suppose a = 2*n;
then A58: a in {2*n} by TARSKI:def 1;
{2*n} in {{2*n}} by TARSKI:def 1;
then {2*n} in E by XBOOLE_0:def 3;
hence x in union E by A58,TARSKI:def 4;
end;
end;
end;
end;
now let A be Subset of cMR such that
A59: A in E;
thus A<>{} proof
per cases by A59,XBOOLE_0:def 3;
suppose A in D;
then consider d being Element of C such that
A60: A = d \/ r.d and
A61: d in C;
d <> {} by A61;
hence thesis by A60;
end;
suppose A in {{2*n}};
hence thesis by TARSKI:def 1;
end;
end;
let B be Subset of cMR such that
A62: B in E;
assume A63: A <> B;
assume A meets B;
then consider x being object such that
A64: x in A and
A65: x in B by XBOOLE_0:3;
per cases by A59,A62,XBOOLE_0:def 3;
suppose that A66: A in D and A67: B in D;
consider d being Element of C such that
A68: A = d \/ r.d and
A69: d in C by A66;
consider e being Element of C such that
A70: B = e \/ r.e and
A71: e in C by A67;
per cases by A68,A70,A64,A65,XBOOLE_0:def 3;
suppose x in d & x in e;
then d meets e by XBOOLE_0:3;
then d = e by A69,A71,EQREL_1:def 4;
hence contradiction by A68,A70,A63;
end;
suppose that A72: x in d and A73: x in r.e;
P[e,r.e] by A71,A5;
then x in { m+n where m is Element of NAT : m in e }
by A73;
then consider mb being Element of NAT such that
A74: x = mb+n and mb in e;
mb+n in Segm(n+0) by A74,A72,A69,A1;
then mb+n < n+0 by NAT_1:44;
hence contradiction by XREAL_1:6;
end;
suppose that A75: x in r.d and A76: x in e;
P[d,r.d] by A69,A5;
then x in { m+n where m is Element of NAT : m in d }
by A75;
then consider ma being Element of NAT such that
A77: x = ma+n and ma in d;
ma+n in Segm(n+0) by A77,A76,A71,A1;
then ma+n < n+0 by NAT_1:44;
hence contradiction by XREAL_1:6;
end;
suppose that A78: x in r.d and A79: x in r.e;
P[d,r.d] by A69,A5;
then x in { m+n where m is Element of NAT : m in d }
by A78;
then consider ma being Element of NAT such that
A80: x = ma+n and
A81: ma in d;
P[e,r.e] by A71,A5;
then x in { m+n where m is Element of NAT : m in e }
by A79;
then consider mb being Element of NAT such that
A82: x = mb+n and
A83: mb in e;
d meets e by A80,A82,A81,A83,XBOOLE_0:3;
then d = e by A69,A71,EQREL_1:def 4;
hence contradiction by A68,A70,A63;
end;
end;
suppose that A84: A in D and A85: B in {{2*n}};
B = {2*n} by A85,TARSKI:def 1;
then A86: x = 2*n by A65,TARSKI:def 1;
consider d being Element of C such that
A87: A = d \/ r.d and
A88: d in C by A84;
per cases by A87,A64,XBOOLE_0:def 3;
suppose x in d;
then n+n in Segm n by A88,A1,A86;
then n+n < n by NAT_1:44;
hence contradiction by NAT_1:11;
end;
suppose
A89: x in r.d;
P[d,r.d] by A88,A5;
then x in { m+n where m is Element of NAT : m in d }
by A89;
then consider m being Element of NAT such that
A90: x = m+n and
A91: m in d;
m in n by A91,A88,A1;
hence contradiction by A90,A86;
end;
end;
suppose that A92: A in {{2*n}} and A93: B in D;
A = {2*n} by A92,TARSKI:def 1;
then A94: x = 2*n by A64,TARSKI:def 1;
consider d being Element of C such that
A95: B = d \/ r.d and
A96: d in C by A93;
per cases by A95,A65,XBOOLE_0:def 3;
suppose x in d;
then n+n in Segm n by A96,A1,A94;
then n+n < n by NAT_1:44;
hence contradiction by NAT_1:11;
end;
suppose
A97: x in r.d;
P[d,r.d] by A96,A5;
then x in { m+n where m is Element of NAT : m in d }
by A97;
then consider m being Element of NAT such that
A98: x = m+n and
A99: m in d;
m in n by A99,A96,A1;
hence contradiction by A98,A94;
end;
end;
suppose A in {{2*n}} & B in {{2*n}};
then A = {2*n} & B = {2*n} by TARSKI:def 1;
hence contradiction by A63;
end;
end;
then reconsider E as a_partition of cMR by A44,A46,EQREL_1:def 4;
now
let x be set;
assume A100: x in E;
per cases by A100,XBOOLE_0:def 3;
suppose x in D;
then consider d being Element of C such that
A101: x = d \/ r.d and
A102: d in C;
reconsider d as Subset of R by A102;
P[d,r.d] by A102,A5;
then
A103: r.d = { m+n where m is Element of NAT : m in d };
A104: x c= cMR proof
let a be object;
assume A105: a in x;
per cases by A101,A105,XBOOLE_0:def 3;
suppose A106: a in d;
then a in Segm n by A1;
then reconsider ap1 = a as Nat;
ap1 in Segm n by A106,A1;
then
A107: ap1 < n by NAT_1:44;
n <= n+n by NAT_1:12;
then ap1 < n+n by A107,XXREAL_0:2;
then ap1 < 2*n+1 by NAT_1:13;
then a in Segm(2*n+1) by NAT_1:44;
hence a in cMR by Def7;
end;
suppose a in r.d;
then consider am being Element of NAT such that
A108: a = am+n and
A109: am in d by A103;
am in Segm n by A109,A1;
then am < n by NAT_1:44;
then am+n < n+n by XREAL_1:6;
then am+n < 2*n+1 by NAT_1:13;
then a in Segm(2*n+1) by A108,NAT_1:44;
hence a in cMR by Def7;
end;
end;
A110: now let x be Nat;
assume x in r.d;
then consider m being Element of NAT such that
A111: x = m+n and
A112: m in d by A103;
thus n <= x by A111,NAT_1:11;
m in Segm n by A112,A1;
then m < n by NAT_1:44;
then m+n < n+n by XREAL_1:6;
hence x < 2*n by A111;
end;
A113: d is stable by DILWORTH:def 12;
now
let a, b be Element of MR such that
A114: a in x and
A115: b in x and
A116: a <> b and
A117: a <= b or b <= a;
A118: [a,b] in iMR or [b,a] in iMR by A117,ORDERS_2:def 5;
per cases by A114,A115,A101,XBOOLE_0:def 3;
suppose A119: a in d & b in d;
then A120: [a,b] in iR or [b,a] in iR by A1,A118,Th40;
reconsider a, b as Element of R by A119;
a <= b or b <= a by A120,ORDERS_2:def 5;
hence contradiction by A119,A116,A113;
end;
suppose that A121: a in d and A122: b in r.d;
consider bm being Element of NAT such that
A123: b = bm+n and
A124: bm in d by A122,A103;
a in Segm n by A121,A1;
then reconsider ap1 = a as Nat;
A125: [ap1,bm] in iR or [bm,ap1] in iR by A118,Th42,Th43,A123,A121
,A1;
reconsider bmp1 = bm, a as Element of R by A124,A121;
A126: bmp1 <= a or a <= bmp1 by A125,ORDERS_2:def 5;
bmp1 <> a by A125,A121,NECKLACE:def 5;
hence contradiction by A126,A124,A121,A113;
end;
suppose that A127: a in r.d and A128: b in d;
consider am being Element of NAT such that
A129: a = am+n and
A130: am in d by A127,A103;
b in Segm n by A128,A1;
then reconsider bp1 = b as Nat;
A131: [am,bp1] in iR or [bp1,am] in iR by A118,Th42,Th43,A129,A128
,A1;
reconsider amp1 = am, b as Element of R by A130,A128;
A132: amp1 <= b or b <= amp1 by A131,ORDERS_2:def 5;
amp1 <> b by A131,A128,NECKLACE:def 5;
hence contradiction by A132,A130,A128,A113;
end;
suppose that A133: a in r.d and A134: b in r.d;
consider am being Element of NAT such that
A135: a = am+n and am in d by A133,A103;
consider bm being Element of NAT such that
A136: b = bm+n and bm in d by A134,A103;
n <= am+n & am+n < 2*n & n <= bm+n & bm+n < 2*n
by A133,A134,A135,A136,A110;
hence contradiction by A135,A136,A118,Th38;
end;
end;
hence x is StableSet of MR by A104,DILWORTH:def 2;
end;
suppose x in {{2*n}};
then A137: x = {2*n} by TARSKI:def 1;
2*n < 2*n+1 by NAT_1:13;
then 2*n in Segm(2*n+1) by NAT_1:44;
then A138: 2*n in cMR by Def7;
x is Subset of MR by A137,A138,SUBSET_1:33;
hence x is StableSet of MR by A137;
end;
end;
then reconsider E as Coloring of MR by DILWORTH:def 12;
take E;
now assume {2*n} in D;
then consider d being Element of C such that
A139: {2*n} = d \/ r.d and
A140: d in C;
A141: 2*n in d \/ r.d by A139,TARSKI:def 1;
per cases by A141,XBOOLE_0:def 3;
suppose 2*n in d;
then 2*n in cR by A140;
then 2*n in Segm n by Def7;
then n+n < n by NAT_1:44;
hence contradiction by NAT_1:11;
end;
suppose
A142: 2*n in r.d;
P[d,r.d] by A140,A5;
then 2*n in { m+n where m is Element of NAT : m in d }
by A142;
then consider m being Element of NAT such that
A143: 2*n = m+n and
A144: m in d;
m in cR by A140,A144;
then m in n by Def7;
hence contradiction by A143;
end;
end;
hence card E = 1 + cnR by A6,A33,A3,CARD_2:41;
end;
for C being finite Coloring of MR holds 1+cnR <= card C proof
:: Is Lorna's construction simpler to formalise?
:: (Showing that the color of 2*n cannot appear in R)
let E be finite Coloring of MR;
assume 1+cnR > card E;
then A145: cnR >= card E by NAT_1:13;
A146: cnMR <= card E by Def3;
then A147: cnMR <= cnR by A145,XXREAL_0:2;
n <= n+n by NAT_1:11;
then n < 2*n+1 by NAT_1:13;
then Segm n c= Segm(2*n+1) by NAT_1:39;
then reconsider S = n as Subset of MR by Def7;
A148: R = subrelstr S by Th45;
then cnR <= cnMR by Th47;
then cnR = cnMR by A147,XXREAL_0:1;
then A149: card E = cnR by A145,A146,XXREAL_0:1;
reconsider C = E |(S) as Coloring of R by A148,Th10;
A150: card C >= cnR by Def3;
A151: card C <= card E by Th8;
then A152: card C = cnR by A149,A150,XXREAL_0:1;
2*n < 2*n+1 by NAT_1:13;
then 2*n in Segm(2*n+1) by NAT_1:44;
then 2*n in cMR by Def7;
then 2*n in union E by EQREL_1:def 4;
then consider e being set such that
A153: 2*n in e and
A154: e in E by TARSKI:def 4;
reconsider e as Subset of MR by A154;
reconsider n2 = 2*n as Element of MR by A153,A154;
set se = e /\ S;
e meets S by A149,A152,A154,Th9;
then A155: se in C by A154;
then consider mp1 being Element of R such that
A156: mp1 in se and
A157: for d being Element of C st d <> se
ex w being Element of R st w in Adjacent(mp1) & w in d
by A151,A149,A150,Th31,XXREAL_0:1;
mp1 in Segm n by A156,A155;
then reconsider m = mp1 as Nat;
set mn = m+n;
A158: 0+n <= mn by XREAL_1:6;
m in Segm n by A156,A155;
then m < n by NAT_1:44;
then A159: mn < n+n by XREAL_1:6;
then mn < 2*n+1 by NAT_1:13;
then A160: mn in Segm(2*n+1) by NAT_1:44;
then mn in cMR by Def7;
then mn in union E by EQREL_1:def 4;
then consider f being set such that
A161: mn in f and
A162: f in E by TARSKI:def 4;
reconsider f as Subset of MR by A162;
reconsider mnp1 = mn as Element of MR by A160,Def7;
A163: now assume A164: e <> f;
set sf = f /\ S;
f meets S by A149,A152,A162,Th9;
then A165: sf in C by A162;
A166: sf c= f by XBOOLE_1:17;
now
assume A167: sf = se;
sf <> {} by A165;
then consider x being object such that
A168: x in sf by XBOOLE_0:def 1;
se c= e by XBOOLE_1:17;
then e meets f by A167,A168,A166,XBOOLE_0:3;
hence contradiction by A164,A162,A154,EQREL_1:def 4;
end;
then consider wp1 being Element of R such that
A169: wp1 in Adjacent(mp1) and
A170: wp1 in sf by A165,A157;
wp1 in Segm n by A170,A165;
then reconsider w = wp1 as Nat;
w in Segm n by A170,A165;
then
A171: w < n by NAT_1:44;
mp1 < wp1 or wp1 < mp1 by A169,Def6;
then mp1 <= wp1 or wp1 <= mp1 by ORDERS_2:def 6;
then [m, w] in iR or [w, m] in iR by ORDERS_2:def 5;
then A172: [m+n, w] in iMR or [w, m+n] in iMR by Th41;
reconsider wp2 = wp1 as Element of MR by A170;
f is stable by A162,DILWORTH:def 12;
then not wp2 <= mnp1 & not mnp1 <= wp2
by A171,A158,A170,A166,A161;
hence contradiction by A172,ORDERS_2:def 5;
end;
A173: [mn,2*n] in iMR by A159,A158,Th44;
e is stable by A154,DILWORTH:def 12;
then not mnp1 <= n2 & not n2 <= mnp1 by A153,A161,A163,A159;
hence contradiction by A173,ORDERS_2:def 5;
end;
hence chromatic# Mycielskian R = 1 + chromatic# R by A2,Def3;
end;
Lm1: now
let myc1, myc2 be Function such that
A1: dom myc1 = NAT and
A2: myc1.0 = CompleteRelStr 2 and
A3: for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc1.k holds myc1.(k+1) = Mycielskian R and
A4: dom myc2 = NAT and
A5: myc2.0 = CompleteRelStr 2 and
A6: for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc2.k holds myc2.(k+1) = Mycielskian R;
defpred P2[Nat] means
myc1.$1 is NatRelStr of 3*2|^$1-'1 & myc1.$1 = myc2.$1;
3*2|^0-'1 = 3*1-'1 by NEWTON:4 .= 2+1-'1 .= 2 by NAT_D:34;
then
A7: P2[0] by A2,A5;
A8: for k being Nat st P2[k] holds P2[k+1] proof
let k be Nat such that
A9: P2[k];
reconsider R = myc1.k as NatRelStr of 3*2|^k-'1 by A9;
A10: myc1.(k+1) = Mycielskian R by A3;
A11: 3*2|^k >= 1*2|^k by XREAL_1:64;
2|^k >= k+1 & k+1 >= 1 by NAT_1:11,NEWTON:85;
then 2|^k >= 1 by XXREAL_0:2;
then A12: 3*2|^k >= 1 by A11,XXREAL_0:2;
then A13: 3*2|^k-1 >= 1-1 by XREAL_1:9;
2*2|^k >= 1*2|^k by XREAL_1:64;
then 2|^(k+1) >= 2|^k by NEWTON:6;
then 3*2|^(k+1) >= 3*2|^k by XREAL_1:64;
then 3*2|^(k+1) >= 1 by A12,XXREAL_0:2;
then A14: 3*2|^(k+1)-1 >= 1-1 by XREAL_1:9;
2*(3*2|^k-'1)+1 = 2*(3*2|^k-1)+1 by A13,XREAL_0:def 2
.= 3*(2*2|^k)-2+1
.= 3*2|^(k+1)-2+1 by NEWTON:6
.= 3*2|^(k+1)-'1 by A14,XREAL_0:def 2;
hence P2[k+1] by A10,A9,A6;
end;
for n being Nat holds P2[n] from NAT_1:sch 2(A7,A8);
then for x being object st x in dom myc1 holds myc1.x = myc2.x by A1;
hence myc1 = myc2 by A1,A4;
end;
definition
let n be Nat;
func Mycielskian n -> NatRelStr of 3*2|^n-'1 means :Def10:
ex myc being Function
st it = myc.n & dom myc = NAT & myc.0 = CompleteRelStr 2 &
:: can start with empty RelStr, numbers will change
:: and the M_2 ... will not be connected
for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc.k holds myc.(k+1) = Mycielskian R;
existence proof
defpred P[Nat,object,object] means
($2 is NatRelStr of 3*2|^$1-'1 implies
ex R being NatRelStr of 3*2|^$1-'1 st $2 = R & $3 = Mycielskian R)
& (not $2 is NatRelStr of 3*2|^$1-'1 implies $3 = $2);
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof let n be Nat, x being set;
per cases;
suppose x is NatRelStr of 3*2|^n-'1;
then reconsider R = x as NatRelStr of 3*2|^n-'1;
Mycielskian R = Mycielskian R;
then consider y being object such that
A2: P[n,x,y];
y is set by TARSKI:1;
hence thesis by A2;
end;
suppose not x is NatRelStr of 3*2|^n-'1;
hence thesis;
end;
end;
consider f being Function such that
A3: dom f = NAT and
A4: f.0 = CompleteRelStr 2 and
A5: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 1(A1);
defpred P2[Nat] means f.$1 is NatRelStr of 3*2|^$1-'1;
3*2|^0-'1 = 3*1-'1 by NEWTON:4 .= 2+1-'1 .= 2 by NAT_D:34;
then
A6: P2[0] by A4;
A7: for k being Nat st P2[k] holds P2[k+1] proof
let k be Nat such that
A8: P2[k];
consider R being NatRelStr of 3*2|^k-'1 such that f.k = R and
A9: f.(k+1) = Mycielskian R by A8,A5;
A10: 3*2|^k >= 1*2|^k by XREAL_1:64;
2|^k >= k+1 & k+1 >= 1 by NAT_1:11,NEWTON:85;
then 2|^k >= 1 by XXREAL_0:2;
then A11: 3*2|^k >= 1 by A10,XXREAL_0:2;
then A12: 3*2|^k-1 >= 1-1 by XREAL_1:9;
2*2|^k >= 1*2|^k by XREAL_1:64;
then 2|^(k+1) >= 2|^k by NEWTON:6;
then 3*2|^(k+1) >= 3*2|^k by XREAL_1:64;
then 3*2|^(k+1) >= 1 by A11,XXREAL_0:2;
then A13: 3*2|^(k+1)-1 >= 1-1 by XREAL_1:9;
2*(3*2|^k-'1)+1 = 2*(3*2|^k-1)+1 by A12,XREAL_0:def 2
.= 3*(2*2|^k)-2+1
.= 3*2|^(k+1)-2+1 by NEWTON:6
.= 3*2|^(k+1)-'1 by A13,XREAL_0:def 2;
hence P2[k+1] by A9;
end;
A14: for n being Nat holds P2[n] from NAT_1:sch 2(A6,A7);
reconsider IT = f.n as NatRelStr of 3*2|^n-'1 by A14;
take IT;
take myc = f;
thus IT = myc.n;
thus dom myc = NAT by A3;
thus myc.0 = CompleteRelStr 2 by A4;
let k be Nat;
let R be NatRelStr of 3*2|^k-'1;
assume A15: R = myc.k;
then consider RR being NatRelStr of 3*2|^k-'1 such that
A16: f.k = RR and
A17: f.(k+1) = Mycielskian RR by A5;
thus myc.(k+1) = Mycielskian R by A17,A15,A16;
end;
uniqueness by Lm1;
end;
theorem Th49: :: Mycn1:
Mycielskian 0 = CompleteRelStr 2 &
for k being Nat holds Mycielskian (k+1) = Mycielskian Mycielskian k
proof
consider myc being Function such that
A1: Mycielskian 0 = myc.0 and
dom myc = NAT and
A2: myc.0 = CompleteRelStr 2 and
for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc.k holds myc.(k+1) = Mycielskian R by Def10;
thus Mycielskian 0 = CompleteRelStr 2 by A1,A2;
let k be Nat;
consider myc1 being Function such that
A3: Mycielskian k = myc1.k and
A4: dom myc1 = NAT & myc1.0 = CompleteRelStr 2 &
for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc1.k holds myc1.(k+1) = Mycielskian R by Def10;
consider myc2 being Function such that
A5: Mycielskian (k+1) = myc2.(k+1) and
A6: dom myc2 = NAT & myc2.0 = CompleteRelStr 2 and
A7: for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc2.k holds myc2.(k+1) = Mycielskian R by Def10;
myc1 = myc2 by A4,A6,A7,Lm1;
hence thesis by A3,A7,A5;
end;
registration
let n be Nat;
cluster Mycielskian n -> irreflexive;
coherence proof
defpred P[Nat] means Mycielskian $1 is irreflexive;
A1: P[0] by Th49;
A2: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
set cMRn = the carrier of Mycielskian n;
set iMRn = the InternalRel of Mycielskian n;
set cMRn1 = the carrier of Mycielskian (n+1);
set iMRn1 = the InternalRel of Mycielskian (n+1);
assume A3: P[n];
assume not P[n+1];
then consider x being set such that
A4: x in cMRn1 and
A5: [x,x] in iMRn1 by NECKLACE:def 5;
A6: Mycielskian (n+1) = Mycielskian Mycielskian n by Th49;
set N = 3*2|^n-'1;
A7: cMRn1 = 2*N+1 by A6,Def7;
A8: cMRn = N by Def7;
x in Segm(2*N+1) by A7,A4;
then reconsider x as Nat;
x < N & x < N or x < N & N <= x & x < 2*N or
N <= x & x < 2*N & x < N or x = 2*N & N <= x & x < 2*N or
N <= x & x < 2*N & x = 2*N by A6,A5,Th38;
then A9: x in Segm N by NAT_1:44;
then [x,x] in iMRn by A5,A6,Th40;
hence contradiction by A3,A8,A9,NECKLACE:def 5;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
registration
let n be Nat;
cluster Mycielskian n -> symmetric;
coherence proof
defpred P[Nat] means Mycielskian $1 is symmetric;
A1: P[0] by Th49;
A2: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
set cMRn = the carrier of Mycielskian n;
set iMRn = the InternalRel of Mycielskian n;
set cMRn1 = the carrier of Mycielskian (n+1);
set iMRn1 = the InternalRel of Mycielskian (n+1);
assume A3: P[n];
A4: Mycielskian (n+1) = Mycielskian Mycielskian n by Th49;
set N = 3*2|^n-'1;
A5: cMRn1 = 2*N+1 by A4,Def7;
A6: cMRn = N by Def7;
let x, y be object such that
A7: x in cMRn1 and
A8: y in cMRn1 and
A9: [x,y] in iMRn1;
x in Segm(2*N+1) & y in Segm(2*N+1) by A5,A7,A8;
then reconsider xp1 = x, yp1 = y as Nat;
A10: [xp1,yp1] in iMRn1 by A9;
per cases by A10,A4,Th38;
suppose xp1 < N & yp1 < N;
then xp1 in Segm N & yp1 in Segm N by NAT_1:44;
then A11: [yp1,xp1] in iMRn by A3,A6,Th5,A9,A4,Th40;
iMRn c= iMRn1 by A4,Th39;
hence [y,x] in iMRn1 by A11;
end;
suppose that A12: xp1 < N and A13: N <= yp1 and A14: yp1 < 2*N;
consider yy being Nat such that
A15: yp1 = N + yy by A13,NAT_1:10;
A16: xp1 in Segm N by A12,NAT_1:44;
yy +N < N + N by A14,A15;
then yy < N by XREAL_1:6;
then A17: yy in Segm N by NAT_1:44;
[x,yy] in iMRn by A9,A16,A15,A4,Th42;
then [yy,x] in iMRn by A17,A16,A6,A3,Th5;
hence [y,x] in iMRn1 by A4,A10,A15,Th41;
end;
suppose that A18: N <= xp1 and A19: xp1 < 2*N and A20: yp1 < N;
consider xx being Nat such that
A21: xp1 = N + xx by A18,NAT_1:10;
A22: yp1 in Segm N by A20,NAT_1:44;
xx+N < N+N by A21,A19;
then xx < N by XREAL_1:6;
then A23: xx in Segm N by NAT_1:44;
[xx,y] in iMRn by A22,A9,A4,A21,Th43;
then [y,xx] in iMRn by A23,A22,A6,A3,Th5;
hence [y,x] in iMRn1 by A4,A10,A21,Th41;
end;
suppose xp1 = 2*N & N <= yp1 & yp1 < 2*N;
hence [y,x] in iMRn1 by A4,Th44;
end;
suppose N <= xp1 & xp1 < 2*N & yp1 = 2*N;
hence [y,x] in iMRn1 by A4,Th44;
end;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem Th50: :: Mycth:
for n being Nat
holds clique# Mycielskian n = 2 & chromatic# Mycielskian n = n+2
proof
defpred P[Nat] means
clique# Mycielskian $1 = 2 & chromatic# Mycielskian $1 = $1+2;
A1: clique# Mycielskian 0 = clique# CompleteRelStr 2 by Th49
.= 2 by Th33;
chromatic# Mycielskian 0 = chromatic# CompleteRelStr 2 by Th49
.= 2 by Th35;
then
A2: P[0] by A1;
A3: for n being Nat st P[n] holds P[n+1] proof
let n be Nat such that
A4: clique# Mycielskian n = 2 and
A5: chromatic# Mycielskian n = n+2;
A6: Mycielskian (n+1) = Mycielskian Mycielskian n by Th49;
thus clique# Mycielskian (n+1) = 2 by A4,A6,Th46;
thus chromatic# Mycielskian (n+1)
= 1 + chromatic# Mycielskian n by A6,Th48
.= n+1+2 by A5;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A2, A3);
hence thesis;
end;
theorem
for n being Nat
ex R being finite RelStr st clique# R = 2 & chromatic# R > n
proof
let n be Nat;
take Mycielskian n;
n+1+1 > n+1 & n+1 > n by NAT_1:13;
then n+2 > n by XXREAL_0:2;
hence thesis by Th50;
end;
theorem
for n being Nat
ex R being finite RelStr st stability# R = 2 & cliquecover# R > n
proof
let n be Nat;
set R = Mycielskian n;
n+1+1 > n+1 & n+1 > n by NAT_1:13;
then n+2 > n by XXREAL_0:2;
then A1: clique# R = 2 & chromatic# R > n by Th50;
take S = ComplRelStr R;
thus stability# S = 2 by A1,Th23;
thus cliquecover# S > n by A1,Th29;
end;