:: The {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received July 2, 2010
:: Copyright (c) 2010 Association of Mizar Users
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, XREAL_0, XXREAL_0, ORDINAL1, NAT_1, XBOOLE_0,
ORDERS_2, STRUCT_0, ZFMISC_1, FUNCT_2, NUMBERS;
notations TARSKI, XBOOLE_0, ZFMISC_1, FINSET_1, CARD_1, SUBSET_1, STRUCT_0,
ORDINAL1, ORDERS_2, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, NAT_D, RELAT_1,
RELSET_1, RELAT_2, PARTFUN1, EQREL_1, FUNCT_1, FUNCT_2, NEWTON, YELLOW_0,
NECKLACE, DILWORTH, NUMBERS;
constructors STRUCT_0, NECKLACE, NECKLA_3, RELSET_1, SETFAM_1, XXREAL_0,
NAT_1, NAT_D, FUNCT_2, 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, PARTFUN1, ZFMISC_1, ORDINAL1, EQREL_1, NECKLA_3,
RELAT_1, FUNCT_1, FUNCT_2, FINSET_1, DILWORTH, NUMBERS, NEWTON, NECKLACE,
YELLOW_0, YELLOW14, ORDERS_2;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions STRUCT_0, XREAL_0, TARSKI, XBOOLE_0, RELAT_2, FUNCT_1, DILWORTH,
NECKLACE, SUBSET_1, EQREL_1, ORDERS_2;
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;
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.
theorem :: TimesM:
for x, y, z being real number st 0 <= x holds x*(y-'z) = x*y -' x*z
proof let x, y, z be real number;
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:234;
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 y \ z iff z <= x & x < y
proof
let x, y, z be Nat;
hereby assume
A1: x in y \ z;
not x in z by A1, XBOOLE_0:def 5;
hence z <= x by NAT_1:45;
thus x < y by A1, NAT_1:45;
end;
assume z <= x & x < y;
then x in y & not x in z by NAT_1:45;
hence x in y \ 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
proof
let R be symmetric RelStr, x, y be set;
set cR = the carrier of R, iR = the InternalRel of R;
assume that
A1: x in cR and
A2: y in cR and
A3: [x,y] in the InternalRel of R;
iR is_symmetric_in cR by NECKLACE:def 4;
hence [y,x] in iR by A1, A2, A3, RELAT_2:def 3;
end;
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 4;
A3: [x,y] in iR by A1, ORDERS_2:def 9;
then x in cR & y in cR by ZFMISC_1:106;
then [y,x] in iR by A2, A3, RELAT_2:def 3;
hence y <= x by ORDERS_2:def 9;
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[set,set] means
$2 = choose $1;
A1: for e being set st e in P ex u being set st P[e,u];
consider f being Function such that
A2: dom f = P and
A3: for e being set 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 set such that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f.x1 = f.x2;
A8: x1 <> {} by A2, A5, EQREL_1:def 6;
A9: x2 <> {} by A2, A6, EQREL_1:def 6;
f.x1 = choose x1 & f.x2 = choose x2 by A5, A6, A2, A3;
then x1 meets x2 by A7, A8, A9, XBOOLE_0:3;
hence x1 = x2 by A5, A6, A2, EQREL_1:def 6;
end;
rng f c= X proof
let y be set;
assume y in rng f;
then consider x being set such that
A10: x in dom f and
A11: y = f.x by FUNCT_1:def 5;
A12: f.x = choose x by A2, A3, A10;
x <> {} by A2, A10, EQREL_1:def 6;
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:26;
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 set;
assume a in D;
then consider x being Element of P such that
A2: a = x /\ S and
x meets S;
a c= S by A2, XBOOLE_1:17;
hence thesis;
end;
A3: union D = S proof
thus union D c= S proof
let x be set;
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 set;
assume A6: s in S;
then s in X;
then s in union P by EQREL_1:def 6;
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 set 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 6;
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 6;
end;
end;
registration
let X be set;
cluster finite a_partition of X;
existence proof
per cases;
suppose X = {};
hence thesis by EQREL_1:54;
end;
suppose X <> {};
then {X} is a_partition of X by EQREL_1:48;
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[set,set] means
$2 = $1 /\ S;
A1: for e being set st e in P ex u being set st P[e,u];
consider f being Function such that
A2: dom f = P and
A3: for e being set st e in P holds P[e,f.e] from CLASSES1:sch 1(A1);
A4: rng f is finite by A2, FINSET_1:26;
P |(S) c= rng f proof
let x be set;
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 set 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 x = f.xx by A3, A5;
hence x in rng f by A8, A2, FUNCT_1:def 5;
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 A1: X = {};
then A2: P = {} by EQREL_1:41;
S = {} by A1;
hence card (P | S) <= card P by A2, EQREL_1:41;
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 A1: X = {};
hereby
assume for p being set st p in P holds p meets S;
S = {} by A1;
hence card (P | S) = {} by CARD_1:47, EQREL_1:41
.= card P by A1, EQREL_1:41,CARD_1:47;
end;
thus thesis by A1,EQREL_1:41;
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[set,set] means
$1 in P & $2 = $1 /\ S;
A4: for x being set st x in P ex y being set st y in PSp1 & P[x,y] proof
let x be set;
assume A5: x in P;
take x /\ S;
x meets S by A5, A3;
hence thesis by A5;
end;
consider f being Function of P,PSp1 such that
A6: for x being set st x in P holds P[x,f.x] from FUNCT_2:sch 1(A4);
now
let x1,x2 be set such that
A7: x1 in P and
A8: x2 in P and
A9: f.x1 = f.x2;
A10: f.x1 = x1 /\ S by A7, A6;
A11: f.x2 = x2 /\ S by A8, A6;
x1 meets S by A7, A3;
then f.x1 in PS by A10, A7;
then f.x1 <> {} by EQREL_1:def 6;
then consider x being set such that
A12: x in f.x1 by XBOOLE_0:def 1;
x in x1 & x in x2 by A12, A9,A10,A11,XBOOLE_0:def 4;
then x1 meets x2 by XBOOLE_0:3;
hence x1 = x2 by A7, A8, EQREL_1:def 6;
end;
then A13: f is one-to-one by FUNCT_2:25;
rng f = PSp1 proof
thus rng f c= PSp1 proof
let y be set;
assume y in rng f;
then consider x being set such that
A14: x in P and
A15: f.x = y by FUNCT_2:17;
x meets S by A3, A14;
then x /\ S in PS by A14;
hence y in PSp1 by A15, A14, A6;
end;
thus PSp1 c= rng f proof
let y be set;
assume y in PSp1;
then consider p being Element of P such that
A16: y = p /\ S and p meets S;
A17: p in Pp1;
then f.p = p /\ S by A6;
hence y in rng f by A16, A17, FUNCT_2:6;
end;
end;
then f is onto by FUNCT_2:def 3;
hence card (P | S) = card P by A13, EULER_1:12;
end;
assume A18: card (P | S) = card P;
defpred P[set,set] means
$1 in PS & $2 in Pp1 & $1 = $2 /\ S;
A19: for x being set st x in PS ex y being set st y in Pp1 & P[x,y] proof
let x be set;
assume A20: x in PS;
then consider p being Element of P such that
A21: x = p /\ S and p meets S;
take p;
thus thesis by A20, A21;
end;
consider f being Function of PS,Pp1 such that
A22: for x being set st x in PS holds P[x,f.x] from FUNCT_2:sch 1(A19);
A23: f is one-to-one proof
let x1,x2 be set such that
A24: x1 in dom f and
A25: x2 in dom f and
A26: f.x1 = f.x2;
x1 = f.x1 /\ S by A24, A22;
hence x1 = x2 by A26, A25, A22;
end;
A27: rng f = P by A18, A23, FINSEQ_4:78;
let p be set;
assume p in P;
then consider ps being set such that
A28: ps in dom f and
A29: p = f.ps by A27, FUNCT_1:def 5;
A30: dom f = PS by FUNCT_2:def 1;
A31: ps = p /\ S by A29, A28, A22;
ps is non empty by A28, A30, EQREL_1:def 6;
then ex x being set st x in ps by XBOOLE_0:def 1;
hence p meets S by A31, XBOOLE_0:4;
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 set such that z in c and
A4: z in S by A3, XBOOLE_0:3;
A5: sS is non empty by YELLOW_0:def 15, A4;
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:59;
A11: C is Coloring of Rp1;
then c in C;
then reconsider cp1 = c as Subset of R;
A12: cp1 is stable by A11, DILWORTH:def 12;
assume a <= b or b <= a;
then ap1 <= bp1 or bp1 <= ap1 by YELLOW_0:60;
hence contradiction by A9, A10, A12, DILWORTH:def 2;
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# RelStr;
existence proof
take R = the empty RelStr;
reconsider S = {} as a_partition of the carrier of R by EQREL_1:54;
take S;
thus S is finite;
end;
end;
registration
cluster finite -> with_finite_chromatic# 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:54;
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};
defpred P[set] means not contradiction;
A3: S = {F(x) where x is Element of cRp1: P[x]} by EQREL_1:46;
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} & not contradiction by A3;
hence z is StableSet of R by A2, SUBSET_1:55;
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 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 set 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, Def2;
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;
C is empty by EQREL_1:41;
hence 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# RelStr;
existence proof
take R = the empty RelStr;
reconsider S = {} as a_partition of the carrier of R by EQREL_1:54;
reconsider S as Clique-partition of R;
take S;
thus S is finite;
end;
end;
registration
cluster finite -> with_finite_cliquecover# 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:54;
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};
defpred P[set] means not contradiction;
A3: S = {F(x) where x is Element of cRp1: P[x]} by EQREL_1:46;
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} & not contradiction by A5, A3;
hence z is Clique of R by A2, SUBSET_1:55;
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 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 set 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, Def4;
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;
C is empty by EQREL_1:41;
hence 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;
card C c= card the carrier of R by CARD_1:27;
hence clique# R <= card the carrier of R by A1, NAT_1:40;
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;
card C c= card the carrier of R by CARD_1:27;
hence stability# R <= card the carrier of R by A1, NAT_1:40;
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;
card C c= card the carrier of R by Th7;
hence chromatic# R <= card the carrier of R by A1, NAT_1:40;
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;
card C c= card the carrier of R by Th7;
hence cliquecover# R <= card the carrier of R by A1, NAT_1:40;
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 card C = card C & card card A = card A;
then A4: card C in card A by A3, A1, A2, NAT_1:42;
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[set,set] means $1 in A & $2 in C & $1 in $2;
A6: for x being set st x in A ex y being set st y in C & P[x,y] proof
let x be set; 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 6;
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 set st x in A holds P[x,f.x] from FUNCT_2:sch 1(A6);
consider x,y being set 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:80;
f.x in C by A11, FUNCT_2:7; then
A15: f.x is StableSet of P by DILWORTH:def 12;
x in f.x & y in f.x by A14, A11, A12, A10;
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 card C = card C & card card A = card A;
then A4: card C in card A by A3, A1, A2, NAT_1:42;
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[set,set] means
$1 in A & $2 in C & $1 in $2;
A6: for x being set st x in A ex y being set st y in C & P[x,y] proof
let x be set 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 6;
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 set st x in A holds P[x,f.x] from FUNCT_2:sch 1(A6);
consider x,y being set 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:80;
f.x in C by A11, FUNCT_2:7; then
A15: f.x is Clique of R by DILWORTH:def 11;
x in f.x & y in f.x by A14, A11, A12, A10;
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 9;
assume x <= y;
then [x,y] in iR by ORDERS_2:def 9;
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 9;
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 9;
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 9;
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 9;
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 9;
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 9;
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 NECKLACE:def 9, DILWORTH:def 2;
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 9;
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 NECKLACE:def 9, DILWORTH:def 2;
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 9;
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 9;
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 9;
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 9;
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 NECKLACE:def 9, DILWORTH:6;
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 by DILWORTH:def 5;
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 by DILWORTH:def 3;
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 9;
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 9;
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 9;
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 9;
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, Def4;
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, Def2;
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 set;
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 10;
then [a,v] in iR by ORDERS_2:def 9;
then [a,v] in [:cR,cR:];
hence x in the carrier of R by A1, ZFMISC_1:106;
end;
suppose v < a;
then v <= a by ORDERS_2:def 10;
then [v,a] in iR by ORDERS_2:def 9;
then [v,a] in [:cR,cR:];
hence x in the carrier of R by A1, ZFMISC_1:106;
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 set;
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 set;
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 6;
reconsider c as Subset of cR by A1;
A5: c <> {} by A1, EQREL_1:def 6;
set Cc = C\{c};
A6: c in {c} by TARSKI:def 1;
per cases;
suppose A7: Cc is empty;
consider v being set 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, EULER_1:5, A7, CARD_1:47;
then 0+1 = card C - 1 +1 by CARD_1:50;
then consider x being set such that
A10: C = {x} by CARD_2:60;
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[set, set] means
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 $2);
A11: for e being set st e in c ex u being set st P[e,u] proof
let v be set 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;
thus thesis by A13, A14, A1;
end;
consider r being Function such that
A15: dom r = c and
A16: for e being set st e in c holds P[e,r.e] from CLASSES1:sch 1(A11);
defpred DP[set] means not contradiction;
deffunc DF(set) = $1 \/ r"{$1};
reconsider Cc as finite non empty set;
set D = { DF(d) where d is Element of Cc : DP[d] };
consider d being set such that
A17: d in Cc by XBOOLE_0:def 1;
A18: d \/ r"{d} in D by A17;
A19: D c= bool cR proof
let x be set;
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:167;
A22: r"{d} c= cR by A21, XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then x 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 set;
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 set;
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 r.xp1 <> c by A27, A16;
then A30: not r.xp1 in {c} by TARSKI:def 1;
r.xp1 in C by A27, A29, A16; then
A31: r.xp1 in Cc by A30, 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 13;
then A32: x in r.xp1 \/ r"{r.xp1} by XBOOLE_0:def 3;
r.xp1 \/ r"{r.xp1} in D by A31;
hence x in union D by A32, 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 A33: d \/ r"{d} in D;
x in d \/ r"{d} by A27, XBOOLE_0:def 3;
hence x in union D by A33, TARSKI:def 4;
end;
end;
end;
A34: 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
A35: A = da \/ r"{da};
A36: da in C by XBOOLE_0:def 5;
then da is non empty by EQREL_1:def 6;
hence A <> {} by A35;
let B be Subset of cR;
assume B in D;
then consider db being Element of Cc such that
A37: B = db \/ r"{db};
A38: db in C by XBOOLE_0:def 5;
per cases;
suppose da = db;
hence A = B or A misses B by A35, A37;
end;
suppose A39: da <> db;
then A40: da misses db by A36, A38, EQREL_1:def 6;
A41: r"{da} misses r"{db} by A39, ZFMISC_1:17, FUNCT_1:141;
assume A <> B;
assume A meets B;
then consider x being set such that
A42: x in A and
A43: x in B by XBOOLE_0:3;
per cases by A42, A43, A35, A37, XBOOLE_0:def 3;
suppose x in da & x in db;
hence contradiction by A40, XBOOLE_0:3;
end;
suppose that A44: x in da and A45: x in r"{db};
A46: da <> c by A6, XBOOLE_0:def 5;
r"{db} c= c by A15, RELAT_1:167;
then da meets c by A44, A45, XBOOLE_0:3;
hence contradiction by A46, A36, A1, EQREL_1:def 6;
end;
suppose that A47: x in r"{da} and A48: x in db;
A49: db <> c by A6, XBOOLE_0:def 5;
r"{da} c= c by A15, RELAT_1:167;
then db meets c by A47, A48, XBOOLE_0:3;
hence contradiction by A49, A38, A1, EQREL_1:def 6;
end;
suppose x in r"{da} & x in r"{db};
hence contradiction by A41, XBOOLE_0:3;
end;
end;
end;
reconsider D as a_partition of cR by A19, A23, A34, EQREL_1:def 6;
now
let x be set;
assume A50: x in D;
then reconsider S = x as Subset of R;
consider d being Element of Cc such that
A51: x = d \/ r"{d} by A50;
A52: r"{d} c= c by A15, RELAT_1:167;
A53: d in C by XBOOLE_0:def 5;
A54: d is StableSet of R by A53, DILWORTH:def 12;
A55: c is StableSet of R by A1, DILWORTH:def 12;
S is stable proof
let a, b be Element of R such that
A56: a in S and
A57: b in S and
A58: a <> b;
per cases by A56, A57, A51, XBOOLE_0:def 3;
suppose a in d & b in d;
hence not a <= b & not b <= a by A54, A58, DILWORTH:def 2;
end;
suppose that A59: a in d and A60: b in r"{d};
r.b in {d} by A60, FUNCT_1:def 13;
then r.b = d by TARSKI:def 1;
then not a in Adjacent(b) by A59, A52, A60,A16;
then not a < b & not b < a by Def6;
hence not a <= b & not b <= a by A58, ORDERS_2:def 10;
end;
suppose that A61: a in r"{d} and A62: b in d;
r.a in {d} by A61, FUNCT_1:def 13;
then r.a = d by TARSKI:def 1;
then not b in Adjacent(a) by A62, A52, A61, A16;
then not a < b & not b < a by Def6;
hence not a <= b & not b <= a by A58, ORDERS_2:def 10;
end;
suppose a in r"{d} & b in r"{d};
hence not a <= b & not b <= a by A52, A55, A58, 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:5;
then card Cc + 1 = card C -1+1 by CARD_1:50;
then A63: card Cc < card C by NAT_1:13;
deffunc FS(set) = $1 \/ r"{$1};
consider s being Function such that
A64: dom s = Cc and
A65: for x being set st x in Cc holds s.x = FS(x) from FUNCT_1:sch 3;
A66: rng s c= D proof
let y be set;
assume y in rng s;
then consider d being set such that
A67: d in dom s and
A68: y = s.d by FUNCT_1:def 5;
y = d \/ r"{d} by A64, A65, A67, A68;
hence y in D by A67, A64;
end;
then reconsider s as Function of Cc, D by A64, FUNCT_2:4;
A69: s is one-to-one proof
let x1, x2 be set such that
A70: x1 in dom s and
A71: x2 in dom s and
A72: s.x1 = s.x2;
A73: s.x1 = x1 \/ r"{x1} by A70, A65;
A74: s.x2 = x2 \/ r"{x2} by A71, A65;
thus x1 c= x2 proof
let x be set;
assume A75: x in x1;
then A76: x in s.x1 by A73, XBOOLE_0:def 3;
per cases by A76, A72, A74, XBOOLE_0:def 3;
suppose x in x2;
hence thesis;
end;
suppose A77: x in r"{x2};
A78: r"{x2} c= dom r by RELAT_1:167;
A79: x1 in C by A70, XBOOLE_0:def 5;
then reconsider x1 as Subset of cR;
x1 meets c by A78, A77, A15, A75, XBOOLE_0:3;
then x1 = c by A79, A1, EQREL_1:def 6;
hence thesis by A6, A70, XBOOLE_0:def 5;
end;
end;
thus x2 c= x1 proof
let x be set;
assume A80: x in x2;
then A81: x in s.x2 by A74, XBOOLE_0:def 3;
per cases by A81, A72, A73, XBOOLE_0:def 3;
suppose x in x1;
hence thesis;
end;
suppose A82: x in r"{x1};
A83: r"{x1} c= dom r by RELAT_1:167;
A84: x2 in C by A71, XBOOLE_0:def 5;
then reconsider x2 as Subset of cR;
x2 meets c by A83, A82, A15, A80, XBOOLE_0:3;
then x2 = c by A84, A1, EQREL_1:def 6;
hence thesis by A6, XBOOLE_0:def 5, A71;
end;
end;
end;
D c= rng s proof
let x be set;
assume x in D;
then consider d being Element of Cc such that
A85: x = d \/ r"{d};
s.d = d \/ r"{d} by A65;
hence x in rng s by A85, A64, FUNCT_1:def 5;
end;
then D = rng s by A66, XBOOLE_0:def 10;
then s is onto by FUNCT_2:def 3;
then A86: card Cc = card D by A69, A18, EULER_1:12;
then D is finite;
hence contradiction by A63, A86, 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:25;
take RelStr (# n, I #);
thus thesis;
end;
end;
registration
cluster -> empty NatRelStr of 0;
coherence proof
let R be NatRelStr of 0;
the carrier of R = 0 by Def7;
hence thesis;
end;
end;
registration
let n be non empty Nat;
cluster -> non empty NatRelStr of n;
coherence by Def7;
end;
registration
let n be Nat;
cluster -> finite NatRelStr of n;
coherence proof
let R be NatRelStr of n;
the carrier of R = n by Def7;
hence thesis;
end;
cluster irreflexive NatRelStr of n;
existence proof
reconsider I = {} as Relation of n,n by RELSET_1:25;
set R = RelStr (# n, I #);
reconsider R as NatRelStr of n by Def7;
R is irreflexive proof
let x be set;
assume x in the carrier of R;
thus not [x,x] in the InternalRel of R;
end;
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:106;
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 proof
let x be set;
assume x in cR;
hence not [x,x] in iR by A1,Th32;
end;
thus R is symmetric proof
let x, y be set;
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 set;
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,CARD_1:71;
for T being finite Clique of R holds card T <= n proof
let T be finite Clique of R;
card n = n by A1, CARD_1:71;
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 empty Nat holds stability# CompleteRelStr n = 1
proof
let n be non empty 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 card n = card n;
then
card n = n by CARD_1:71;
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 empty Nat holds cliquecover# CompleteRelStr n = 1
proof
let n be non empty Nat;
set R = CompleteRelStr n; set cR = the carrier of R;
reconsider C = {cR} as a_partition of cR by EQREL_1:48;
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:50;
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 set;
assume A3: z in iMR;
per cases by A3, Th4;
suppose z in iR;
then consider c, d being set such that
A4: c in cR and
A5: d in cR and
A6: z = [c,d] by ZFMISC_1:def 2;
reconsider c, d as Nat by A1, A4, A5, NECKLACE:4;
c < n & d < n by A1, A4, A5, NAT_1:45;
then c < cMR & d < cMR by A2, XXREAL_0:2;
then c in cMR & d in cMR by NAT_1:45;
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 cR by A8, ZFMISC_1:106;
then x < n by A1, NAT_1:45;
then x < cMR by A2, XXREAL_0:2;
then A9: x in cMR by NAT_1:45;
y in cR by A8, ZFMISC_1:106;
then y < n by A1, NAT_1:45;
then y+n < n+n by XREAL_1:8;
then y+n < 2*n+1 by NAT_1:13;
then y+n in cMR by NAT_1:45;
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 cR by A11, ZFMISC_1:106;
then y < n by A1, NAT_1:45;
then y < cMR by A2, XXREAL_0:2;
then A12: y in cMR by NAT_1:45;
x in cR by A11, ZFMISC_1:106;
then x < n by A1, NAT_1:45;
then x+n < n+n by XREAL_1:8;
then x+n < 2*n+1 by NAT_1:13;
then x+n in cMR by NAT_1:45;
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 set such that
A13: c in {2*n} and
A14: d in 2*n \ 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 cMR by NAT_1:45;
reconsider d as Nat by A14, NECKLACE:4;
d < 2*n by A14, Th2;
then d < cMR by NAT_1:13;
then d in cMR by NAT_1:45;
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 set such that
A18: c in 2*n \ 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 cMR by NAT_1:45;
reconsider c as Nat by A18, NECKLACE:4;
c < 2*n by A18, Th2;
then c < cMR by NAT_1:13;
then c in cMR by NAT_1:45;
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 n c= 2*n+1 by NAT_1:40;
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:106;
then a in n & b in n by Def7;
hence RHS[] by NAT_1:45;
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:106;
then y in n by Def7;
then y < n by NAT_1:45;
then A5: y+n < n+n by XREAL_1:8;
x in cR by A4, ZFMISC_1:106;
then x in n by Def7;
then x < n by NAT_1:45;
hence RHS[] by A5, A3, ZFMISC_1:33;
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:106;
then x in n by Def7;
then x < n by NAT_1:45;
then A8: x+n < n+n by XREAL_1:8;
y in cR by A7, ZFMISC_1:106;
then y in n by Def7;
then y < n by NAT_1:45;
hence RHS[] by A8, A6, ZFMISC_1:33;
end;
suppose A9: [a,b] in [: {2*n}, 2*n \ n :];
A10: b in 2*n \ n by A9, ZFMISC_1:106;
a in {2*n} by A9, ZFMISC_1:106;
hence RHS[] by A10, Th2, TARSKI:def 1;
end;
suppose A11: [a,b] in [: 2*n \ n, {2*n} :];
A12: a in 2*n \ n by A11, ZFMISC_1:106;
b in {2*n} by A11, ZFMISC_1:106;
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 n & y in 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 n and
A2: b in 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, ZFMISC_1:33;
then y+n < n by A2, NAT_1:45;
then y < n-n by XREAL_1:22;
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, ZFMISC_1:33;
then x+n < n by A1, NAT_1:45;
then x < n-n by XREAL_1:22;
then x < 0;
hence [a,b] in iR;
end;
suppose [a,b] in [: {2*n}, 2*n \ n :];
then consider c, d being set 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, ZFMISC_1:33;
n+n < n by A1, A10, A9, NAT_1:45;
then n < n-n by XREAL_1:22;
then n < 0;
hence [a,b] in iR;
end;
suppose [a,b] in [: 2*n \ n, {2*n} :];
then consider c, d being set 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, ZFMISC_1:33;
n+n < n by A2, A14, A13, NAT_1:45;
then n < n-n by XREAL_1:22;
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 13;
[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 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 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:106;
then b+n in n by Def7;
then b+n < n by NAT_1:45;
then b < n-n by XREAL_1:22;
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, ZFMISC_1:33;
hence [a,b] in iR by A5, A4, ZFMISC_1:33;
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, ZFMISC_1:33;
then b+n in cR by A7, ZFMISC_1:106;
then b+n in n by Def7;
then b+n < n by NAT_1:45;
then b < n-n by XREAL_1:22;
then b < 0;
hence [a,b] in iR;
end;
suppose [a,b+n] in [: {2*n}, 2*n \ n :];
then consider c, d being set 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, ZFMISC_1:33;
n+n < n by A1, A11, A10, NAT_1:45;
then n < n-n by XREAL_1:22;
then n < 0;
hence [a,b] in iR;
end;
suppose [a,b+n] in [: 2*n \ n, {2*n} :];
then consider c, d being set such that
A12: c in 2*n \ n and d in {2*n} and
A13: [a,b+n] = [c,d] by ZFMISC_1:def 2;
c = a by A13, ZFMISC_1:33;
then n <= a by A12, Th2;
hence [a,b] in iR by A1, NAT_1:45;
end;
end;
theorem Th43: :: iMR1d:
for n being Nat, R being NatRelStr of n, x, y being Nat
st y in 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 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:106;
then a+n in n by Def7;
then a+n < n by NAT_1:45;
then a < n-n by XREAL_1:22;
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, ZFMISC_1:33;
then a+n in cR by A5, ZFMISC_1:106;
then a+n in n by Def7;
then a+n < n by NAT_1:45;
then a < n-n by XREAL_1:22;
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, ZFMISC_1:33;
hence [a,b] in iR by A7, A6, ZFMISC_1:33;
end;
suppose [a+n,b] in [: {2*n}, 2*n \ n :];
then consider c, d being set such that c in {2*n} and
A8: d in 2*n \ n and
A9: [a+n,b] = [c,d] by ZFMISC_1:def 2;
b = d by A9, ZFMISC_1:33;
then n <= b by A8, Th2;
hence [a,b] in iR by A1, NAT_1:45;
end;
suppose [a+n,b] in [: 2*n \ n, {2*n} :];
then consider c, d being set 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, ZFMISC_1:33;
then n+n < n by A1, A12, NAT_1:45;
then n < n-n by XREAL_1:22;
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 2*n \ 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 set;
assume A5: z in iR;
then consider x, y being set 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 9;
then xsS <= ysS by A3, A2, A7, YELLOW_0:61;
hence z in isS by A8, ORDERS_2:def 9;
end;
thus isS c= iR proof
let z be set;
assume A9: z in isS;
then consider x, y being set such that
A10: x in csS and
A11: y in csS and
A12: z = [x,y] by ZFMISC_1:def 2;
cR c= cMR by Th37;
then reconsider xMR = x, yMR = y as Element of MR by A10, A11, A2, A3
;
reconsider xsS = x, ysS = y as Element of sS by A10, A11;
xsS <= ysS by A9, A12, ORDERS_2:def 9;
then xMR <= yMR by YELLOW_0:60;
then z in iMR by A12, ORDERS_2:def 9;
hence z in iR by A10, A11, A3, 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 n c= 2*n+1 by NAT_1:40;
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 set such that
A11: x in D and
A12: not x in n by TARSKI:def 3;
x in cMR by A11; then
A13: x in 2*n+1 by Def7;
reconsider x as Nat by A13, NECKLACE:4;
reconsider xp1 = x as Element of MR by A11;
A14: x >= n by A12, NAT_1:45;
x < 2*n+1 by A13, NAT_1:45;
then
A15: x <= 2*n by NAT_1:13;
A16: for y being set st y in D & x <> y holds y in n proof
let y be set such that
A17: y in D and
A18: x <> y and
A19: not y in n;
y in cMR by A17; then
A20: y in 2*n+1 by Def7;
reconsider y as Nat by A20, NECKLACE:4;
reconsider yp1 = y as Element of MR by A17;
A21: y >= n by A19, NAT_1:45;
y < 2*n+1 by A20, NAT_1:45;
then
A22: y <= 2*n by NAT_1:13;
set DD = D \ {x,y};
{x,y} c= D by A17, A11, ZFMISC_1:38;
then A23: card DD = card D - card {x,y} by CARD_2:63;
1+2-2 <= card D -2 by A8, A9, XREAL_1:11;
then 1 <= card DD by A23, A18, CARD_2:76;
then consider z being set such that
A24: z in DD by XBOOLE_0:def 1, CARD_1:47;
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 2*n+1 by A26, Def7;
reconsider z as Nat by A27, NECKLACE:4;
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 9;
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 9;
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 9;
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 9;
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 9;
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:5
.= card D - 1 by CARD_1:50;
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:8;
then A39: xx in n by NAT_1:45;
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 9;
then [xx,xx] in iR or [xx,xx] in iR by A39, A37, Th42, Th43;
hence contradiction by A39, A3, NECKLACE:def 6;
end;
set DD = (D\{x}) \/ {xx};
DD c= cR proof
let a be set;
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, NAT_1:45, A16, A3;
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 XBOOLE_0:def 5, TARSKI:def 1;
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 XBOOLE_0:def 5, TARSKI:def 1;
A46: a in cR & b in cR by A41;
reconsider an = a, bn = b as Nat by A41, A3, NECKLACE:4;
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:61;
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 9;
then [an, xx] in iR or [xx,an] in iR
by A3,A38,A37,Th42,Th43;
hence a <= b or b <= a by A48, ORDERS_2:def 9;
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 9;
then [bn, xx] in iR or [xx,bn] in iR
by A3,A38, A37,Th42,Th43;
hence a <= b or b <= a by A49, ORDERS_2:def 9;
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:54 .= 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:11;
then 2 c= card (D\{x}) by A35, NAT_1:40;
then consider y, z being set 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:64;
A54: x <> y by A52, ZFMISC_1:64;
y in the carrier of MR by A52;
then y in 2*n+1 by Def7;
then reconsider y as Nat by NECKLACE:4;
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 9;
y in n by A16, A53, A54;
then A56: y < n by NAT_1:45;
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 = 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[set,set] means
$2 = { m+n where m is Element of NAT : m in $1 };
A4: for e being set st e in C ex u being set st P[e,u];
consider r being Function such that dom r = C and
A5: for e being set 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 set such that
A8: c in C by XBOOLE_0:def 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[set,set] means $2 = $1 \/ r.$1;
A10: for e being set st e in C ex u being set st R[e,u];
consider s being Function such that
A11: dom s = C and
A12: for e being set st e in C holds R[e,s.e] from CLASSES1:sch 1(A10);
A13: rng s c= D proof
let y be set;
assume y in rng s;
then consider x being set such that
A14: x in dom s and
A15: y = s.x by FUNCT_1:def 5;
y = x \/ r.x by A14, A15, A11, A12;
hence y in D by A14, A11;
end;
then reconsider s as Function of C, D by A11, FUNCT_2:4;
D c= rng s proof
let x be set;
assume x in D;
then consider c being Element of C such that
A16: x = c \/ r.c and
A17: c in C;
x = s.c by A16, A17, A12;
hence x in rng s by A17, A11, FUNCT_1:def 5;
end;
then rng s = D by A13, XBOOLE_0:def 10;
then
A18: s is onto by FUNCT_2:def 3;
s is one-to-one proof
let x1,x2 be set such that
A19: x1 in dom s and
A20: x2 in dom s and
A21: s.x1 = s.x2;
A22: s.x1 = x1 \/ r.x1 by A19, A12;
A23: s.x2 = x2 \/ r.x2 by A20, A12;
thus x1 c= x2 proof
let x be set;
assume A24: x in x1;
A25: x in s.x1 by A22, A24, XBOOLE_0:def 3;
per cases by A25, A21, A23, XBOOLE_0:def 3;
suppose x in x2;
hence thesis;
end;
suppose x in r.x2;
then x in { m+n where m is Element of NAT : m in x2 }
by A5, A20;
then consider m being Element of NAT such that
A26: x = m+n and m in x2;
m+n < 0+n by A24, A26, A19, A11, A1, NAT_1:45;
hence thesis by XREAL_1:8;
end;
end;
thus x2 c= x1 proof
let x be set;
assume A27: x in x2;
A28: x in s.x2 by A23, A27, XBOOLE_0:def 3;
per cases by A28, A21, A22, XBOOLE_0:def 3;
suppose x in x1;
hence thesis;
end;
suppose x in r.x1;
then x in { m+n where m is Element of NAT : m in x1 }
by A5, A19;
then consider m being Element of NAT such that
A29: x = m+n and m in x1;
m+n < 0+n by A27, A29, A20, A11, A1, NAT_1:45;
hence thesis by XREAL_1:8;
end;
end;
end;
hence thesis by A18, A9, EULER_1:12;
end;
end;
then
A30: D is finite;
set E = D \/ {{2*n}};
A31: union E c= cMR proof
let x be set;
assume x in union E;
then consider Y being set such that
A32: x in Y and
A33: Y in E by TARSKI:def 4;
per cases by A33, XBOOLE_0:def 3;
suppose Y in D;
then consider d being Element of C such that
A34: Y = d \/ r.d and
A35: d in C;
A36: r.d = { m+n where m is Element of NAT : m in d } by A35, A5;
per cases by A32, A34, XBOOLE_0:def 3;
suppose A37: x in d;
reconsider a = x as Nat by A37, A35, A1, NECKLACE:4;
a < n by A37, A35, A1, NAT_1:45;
then a+0 < n+n by XREAL_1:10;
then a < 2*n+1 by NAT_1:13;
then a in 2*n+1 by NAT_1:45;
hence x in cMR by Def7;
end;
suppose x in r.d;
then consider m being Element of NAT such that
A38: x = m+n and
A39: m in d by A36;
m < n by A39, A35, A1, NAT_1:45;
then m+n < n+n by XREAL_1:8;
then m+n < 2*n + 1 by NAT_1:13;
then x in 2*n+1 by A38, NAT_1:45;
hence x in cMR by Def7;
end;
end;
suppose Y in {{2*n}};
then Y = {2*n} by TARSKI:def 1;
then A40: x = 2*n by A32, TARSKI:def 1;
2*n < 2*n+1 by NAT_1:13;
then 2*n in 2*n+1 by NAT_1:45;
hence x in cMR by A40, Def7;
end;
end;
A41: E c= bool cMR proof
let X be set;
assume A42: X in E;
X c= cMR proof
let x be set;
assume x in X;
then x in union E by A42, TARSKI:def 4;
hence x in cMR by A31;
end;
hence X in bool cMR;
end;
A43: union E = cMR proof
thus union E c= cMR by A31;
thus cMR c= union E proof
let x be set;
assume x in cMR;
then A44: x in 2*n+1 by Def7;
then reconsider a = x as Nat by NECKLACE:4;
a < 2*n+1 by A44, NAT_1:45;
then A45: a <= 2*n by NAT_1:13;
per cases;
suppose a < n;
then a in n by NAT_1:45;
then a in union C by A1, EQREL_1:def 6;
then consider c being set such that
A46: a in c and
A47: c in C by TARSKI:def 4;
A48: x in c \/ r.c by A46, XBOOLE_0:def 3;
c \/ r.c in D by A47;
then c \/ r.c in E by XBOOLE_0:def 3;
hence x in union E by A48, TARSKI:def 4;
end;
suppose A49: a >= n;
per cases by A45, XXREAL_0:1;
suppose A50: a < n+n;
consider b being Nat such that
A51: a = n + b by A49, NAT_1:10;
reconsider b as Element of NAT by ORDINAL1:def 13;
b < n by A51, A50, XREAL_1:8;
then b in cR by A1, NAT_1:45;
then b in union C by EQREL_1:def 6;
then consider c being set such that
A52: b in c and
A53: c in C by TARSKI:def 4;
r.c = { m+n where m is Element of NAT : m in c } by A53, A5;
then a in r.c by A52, A51;
then A54: x in c \/ r.c by XBOOLE_0:def 3;
c \/ r.c in D by A53;
then c \/ r.c in E by XBOOLE_0:def 3;
hence x in union E by A54, TARSKI:def 4;
end;
suppose a = 2*n;
then A55: 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 A55, TARSKI:def 4;
end;
end;
end;
end;
now let A be Subset of cMR such that
A56: A in E;
thus A<>{} proof
per cases by A56, XBOOLE_0:def 3;
suppose A in D;
then consider d being Element of C such that
A57: A = d \/ r.d and
A58: d in C;
d <> {} by A58, EQREL_1:def 6;
hence thesis by A57;
end;
suppose A in {{2*n}};
hence thesis by TARSKI:def 1;
end;
end;
let B be Subset of cMR such that
A59: B in E;
assume A60: A <> B;
assume A meets B;
then consider x being set such that
A61: x in A and
A62: x in B by XBOOLE_0:3;
per cases by A56, A59, XBOOLE_0:def 3;
suppose that A63: A in D and A64: B in D;
consider d being Element of C such that
A65: A = d \/ r.d and
A66: d in C by A63;
consider e being Element of C such that
A67: B = e \/ r.e and
A68: e in C by A64;
per cases by A65, A67, A61, A62, XBOOLE_0:def 3;
suppose x in d & x in e;
then d meets e by XBOOLE_0:3;
then d = e by A66, A68, EQREL_1:def 6;
hence contradiction by A65, A67, A60;
end;
suppose that A69: x in d and A70: x in r.e;
x in { m+n where m is Element of NAT : m in e } by A70, A68, A5;
then consider mb being Element of NAT such that
A71: x = mb+n and mb in e;
mb+n < n+0 by A71, A69, A66, A1, NAT_1:45;
hence contradiction by XREAL_1:8;
end;
suppose that A72: x in r.d and A73: x in e;
x in { m+n where m is Element of NAT : m in d } by A72, A66, A5;
then consider ma being Element of NAT such that
A74: x = ma+n and ma in d;
ma+n < n+0 by A74, A73, A68, A1, NAT_1:45;
hence contradiction by XREAL_1:8;
end;
suppose that A75: x in r.d and A76: x in r.e;
x in { m+n where m is Element of NAT : m in d } by A75, A66, A5;
then consider ma being Element of NAT such that
A77: x = ma+n and
A78: ma in d;
x in { m+n where m is Element of NAT : m in e } by A76, A68, A5;
then consider mb being Element of NAT such that
A79: x = mb+n and
A80: mb in e;
d meets e by A77, A79, A78, A80, XBOOLE_0:3;
then d = e by A66, A68, EQREL_1:def 6;
hence contradiction by A65, A67, A60;
end;
end;
suppose that A81: A in D and A82: B in {{2*n}};
B = {2*n} by A82, TARSKI:def 1;
then A83: x = 2*n by A62, TARSKI:def 1;
consider d being Element of C such that
A84: A = d \/ r.d and
A85: d in C by A81;
per cases by A84, A61, XBOOLE_0:def 3;
suppose x in d;
then n+n < n by A85, A1, A83, NAT_1:45;
hence contradiction by NAT_1:11;
end;
suppose x in r.d;
then x in { m+n where m is Element of NAT : m in d } by A85, A5;
then consider m being Element of NAT such that
A86: x = m+n and
A87: m in d;
m in n by A87, A85, A1;
hence contradiction by A86, A83;
end;
end;
suppose that A88: A in {{2*n}} and A89: B in D;
A = {2*n} by A88, TARSKI:def 1;
then A90: x = 2*n by A61, TARSKI:def 1;
consider d being Element of C such that
A91: B = d \/ r.d and
A92: d in C by A89;
per cases by A91, A62, XBOOLE_0:def 3;
suppose x in d;
then n+n < n by A92, A1, A90, NAT_1:45;
hence contradiction by NAT_1:11;
end;
suppose x in r.d;
then x in { m+n where m is Element of NAT : m in d } by A92, A5;
then consider m being Element of NAT such that
A93: x = m+n and
A94: m in d;
m in n by A94, A92, A1;
hence contradiction by A93, A90;
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 A60;
end;
end;
then reconsider E as a_partition of cMR by A41, A43, EQREL_1:def 6;
now
let x be set;
assume A95: x in E;
per cases by A95, XBOOLE_0:def 3;
suppose x in D;
then consider d being Element of C such that
A96: x = d \/ r.d and
A97: d in C;
reconsider d as Subset of R by A97;
A98: r.d = { m+n where m is Element of NAT : m in d } by A97, A5;
A99: x c= cMR proof
let a be set;
assume A100: a in x;
per cases by A96, A100, XBOOLE_0:def 3;
suppose A101: a in d;
then reconsider ap1 = a as Nat by A1, NECKLACE:4;
A102: ap1 < n by A101, A1, NAT_1:45;
n <= n+n by NAT_1:12;
then ap1 < n+n by A102, XXREAL_0:2;
then ap1 < 2*n+1 by NAT_1:13;
then a in 2*n+1 by NAT_1:45;
hence a in cMR by Def7;
end;
suppose a in r.d;
then consider am being Element of NAT such that
A103: a = am+n and
A104: am in d by A98;
am < n by A104, A1, NAT_1:45;
then am+n < n+n by XREAL_1:8;
then am+n < 2*n+1 by NAT_1:13;
then a in 2*n+1 by A103, NAT_1:45;
hence a in cMR by Def7;
end;
end;
A105: now let x be Nat;
assume x in r.d;
then consider m being Element of NAT such that
A106: x = m+n and
A107: m in d by A98;
thus n <= x by A106, NAT_1:11;
m < n by NAT_1:45, A107, A1;
then m+n < n+n by XREAL_1:8;
hence x < 2*n by A106;
end;
A108: d is stable by A97, DILWORTH:def 12;
now
let a, b be Element of MR such that
A109: a in x and
A110: b in x and
A111: a <> b and
A112: a <= b or b <= a;
A113: [a,b] in iMR or [b,a] in iMR by A112, ORDERS_2:def 9;
per cases by A109, A110, A96, XBOOLE_0:def 3;
suppose A114: a in d & b in d;
then A115: [a,b] in iR or [b,a] in iR by A1, A113, Th40;
reconsider a, b as Element of R by A114;
a <= b or b <= a by A115, ORDERS_2:def 9;
hence contradiction by A114, A111, A108, DILWORTH:def 2;
end;
suppose that A116: a in d and A117: b in r.d;
consider bm being Element of NAT such that
A118: b = bm+n and
A119: bm in d by A117, A98;
reconsider ap1 = a as Nat by A116, A1, NECKLACE:4;
A120: [ap1,bm] in iR or [bm,ap1] in iR by A113,Th42,Th43,A118,A116
,A1;
reconsider bmp1 = bm, a as Element of R by A119, A116;
A121: bmp1 <= a or a <= bmp1 by A120, ORDERS_2:def 9;
bmp1 <> a by A120, A116, NECKLACE:def 6;
hence contradiction by A121, A119, A116, A108, DILWORTH:def 2;
end;
suppose that A122: a in r.d and A123: b in d;
consider am being Element of NAT such that
A124: a = am+n and
A125: am in d by A122, A98;
reconsider bp1 = b as Nat by A123, A1, NECKLACE:4;
A126: [am,bp1] in iR or [bp1,am] in iR by A113,Th42,Th43,A124,A123
,A1;
reconsider amp1 = am, b as Element of R by A125, A123;
A127: amp1 <= b or b <= amp1 by A126, ORDERS_2:def 9;
amp1 <> b by A126, A123, NECKLACE:def 6;
hence contradiction by A127, A125, A123, A108, DILWORTH:def 2;
end;
suppose that A128: a in r.d and A129: b in r.d;
consider am being Element of NAT such that
A130: a = am+n and am in d by A128, A98;
consider bm being Element of NAT such that
A131: b = bm+n and bm in d by A129, A98;
n <= am+n & am+n < 2*n & n <= bm+n & bm+n < 2*n
by A128, A129,A130,A131, A105;
hence contradiction by A130, A131, A113, Th38;
end;
end;
hence x is StableSet of MR by A99, DILWORTH:def 2;
end;
suppose x in {{2*n}};
then A132: x = {2*n} by TARSKI:def 1;
2*n < 2*n+1 by NAT_1:13;
then 2*n in 2*n+1 by NAT_1:45;
then A133: 2*n in cMR by Def7;
x is Subset of MR by A132, A133, SUBSET_1:55;
hence x is StableSet of MR by A132;
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
A134: {2*n} = d \/ r.d and
A135: d in C;
A136: 2*n in d \/ r.d by A134, TARSKI:def 1;
per cases by A136, XBOOLE_0:def 3;
suppose 2*n in d;
then 2*n in cR by A135;
then 2*n in n by Def7;
then n+n < n by NAT_1:45;
hence contradiction by NAT_1:11;
end;
suppose 2*n in r.d;
then 2*n in { m+n where m is Element of NAT : m in d } by A135, A5;
then consider m being Element of NAT such that
A137: 2*n = m+n and
A138: m in d;
m in cR by A135, A138;
then m in n by Def7;
hence contradiction by A137;
end;
end;
hence card E = 1 + cnR by A6, A30, A3, CARD_2:54;
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 A139: cnR >= card E by NAT_1:13;
A140: cnMR <= card E by Def3;
then A141: cnMR <= cnR by A139, XXREAL_0:2;
n <= n+n by NAT_1:11;
then n < 2*n+1 by NAT_1:13;
then n c= 2*n+1 by NAT_1:40;
then reconsider S = n as Subset of MR by Def7;
A142: R = subrelstr S by Th45;
then cnR <= cnMR by Th47;
then cnR = cnMR by A141, XXREAL_0:1;
then A143: card E = cnR by A139,A140, XXREAL_0:1;
reconsider C = E |(S) as Coloring of R by A142, Th10;
A144: card C >= cnR by Def3;
A145: card C <= card E by Th8;
then A146: card C = cnR by A143, A144, XXREAL_0:1;
2*n < 2*n+1 by NAT_1:13;
then 2*n in 2*n+1 by NAT_1:45;
then 2*n in cMR by Def7;
then 2*n in union E by EQREL_1:def 6;
then consider e being set such that
A147: 2*n in e and
A148: e in E by TARSKI:def 4;
reconsider e as Subset of MR by A148;
reconsider n2 = 2*n as Element of MR by A147, A148;
set se = e /\ S;
e meets S by A143, A146, A148, Th9;
then A149: se in C by A148;
then consider mp1 being Element of R such that
A150: mp1 in se and
A151: for d being Element of C st d <> se
ex w being Element of R st w in Adjacent(mp1) & w in d
by A145, A143, A144, XXREAL_0:1, Th31;
reconsider m = mp1 as Nat by A150, A149, NECKLACE:4;
set mn = m+n;
A152: 0+n <= mn by XREAL_1:8;
m < n by A150, A149, NAT_1:45;
then A153: mn < n+n by XREAL_1:8;
then mn < 2*n+1 by NAT_1:13;
then A154: mn in 2*n+1 by NAT_1:45;
then mn in cMR by Def7;
then mn in union E by EQREL_1:def 6;
then consider f being set such that
A155: mn in f and
A156: f in E by TARSKI:def 4;
reconsider f as Subset of MR by A156;
reconsider mnp1 = mn as Element of MR by A154, Def7;
A157: now assume A158: e <> f;
set sf = f /\ S;
f meets S by A143, A146, A156, Th9;
then A159: sf in C by A156;
A160: sf c= f by XBOOLE_1:17;
now
assume A161: sf = se;
sf <> {} by A159, EQREL_1:def 6;
then consider x being set such that
A162: x in sf by XBOOLE_0:def 1;
se c= e by XBOOLE_1:17;
then e meets f by A161, A162, A160, XBOOLE_0:3;
hence contradiction by A158, A156, A148, EQREL_1:def 6;
end;
then consider wp1 being Element of R such that
A163: wp1 in Adjacent(mp1) and
A164: wp1 in sf by A159, A151;
reconsider w = wp1 as Nat by A164, A159, NECKLACE:4;
A165: w < n by A164, A159, NAT_1:45;
mp1 < wp1 or wp1 < mp1 by A163, Def6;
then mp1 <= wp1 or wp1 <= mp1 by ORDERS_2:def 10;
then [m, w] in iR or [w, m] in iR by ORDERS_2:def 9;
then A166: [m+n, w] in iMR or [w, m+n] in iMR by Th41;
reconsider wp2 = wp1 as Element of MR by A164;
f is stable by A156, DILWORTH:def 12;
then not wp2 <= mnp1 & not mnp1 <= wp2
by A165, A152, A164, A160, A155, DILWORTH:def 2;
hence contradiction by A166, ORDERS_2:def 9;
end;
A167: [mn,2*n] in iMR by A153, A152, Th44;
e is stable by A148, DILWORTH:def 12;
then not mnp1 <= n2 & not n2 <= mnp1 by A147, A155, A157, A153
, DILWORTH:def 2;
hence contradiction by A167, ORDERS_2:def 9;
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:9 .= 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:66;
2|^k >= k+1 & k+1 >= 1 by NEWTON:104, NAT_1:11;
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:11;
2*2|^k >= 1*2|^k by XREAL_1:66;
then 2|^(k+1) >= 2|^k by NEWTON:11;
then 3*2|^(k+1) >= 3*2|^k by XREAL_1:66;
then 3*2|^(k+1) >= 1 by A12, XXREAL_0:2;
then A14: 3*2|^(k+1)-1 >= 1-1 by XREAL_1:11;
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:11
.= 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 set st x in dom myc1 holds myc1.x = myc2.x by A1;
hence myc1 = myc2 by A1, A4, FUNCT_1:9;
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,set,set] 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 Element of NAT for x being set ex y being set st P[n,x,y]
proof let n be Element of 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;
hence ex y being set st P[n,x,y];
end;
suppose not x is NatRelStr of 3*2|^n-'1;
hence thesis;
end;
end;
consider f being Function such that
A2: dom f = NAT and
A3: f.0 = CompleteRelStr 2 and
A4: for n being Element of 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:9 .= 2+1-'1 .= 2 by NAT_D:34;
then
A5: P2[0] by A3;
A6: for k being Element of NAT st P2[k] holds P2[k+1] proof
let k be Element of NAT such that
A7: P2[k];
consider R being NatRelStr of 3*2|^k-'1 such that f.k = R and
A8: f.(k+1) = Mycielskian R by A7, A4;
A9: 3*2|^k >= 1*2|^k by XREAL_1:66;
2|^k >= k+1 & k+1 >= 1 by NEWTON:104, NAT_1:11;
then 2|^k >= 1 by XXREAL_0:2;
then A10: 3*2|^k >= 1 by A9, XXREAL_0:2;
then A11: 3*2|^k-1 >= 1-1 by XREAL_1:11;
2*2|^k >= 1*2|^k by XREAL_1:66;
then 2|^(k+1) >= 2|^k by NEWTON:11;
then 3*2|^(k+1) >= 3*2|^k by XREAL_1:66;
then 3*2|^(k+1) >= 1 by A10, XXREAL_0:2;
then A12: 3*2|^(k+1)-1 >= 1-1 by XREAL_1:11;
2*(3*2|^k-'1)+1 = 2*(3*2|^k-1)+1 by A11, XREAL_0:def 2
.= 3*(2*2|^k)-2+1
.= 3*2|^(k+1)-2+1 by NEWTON:11
.= 3*2|^(k+1)-'1 by A12, XREAL_0:def 2;
hence P2[k+1] by A8;
end;
A13: for n being Element of NAT holds P2[n] from NAT_1:sch 1(A5,A6);
n is Element of NAT by ORDINAL1:def 13;
then reconsider IT = f.n as NatRelStr of 3*2|^n-'1 by A13;
take IT;
take myc = f;
thus IT = myc.n;
thus dom myc = NAT by A2;
thus myc.0 = CompleteRelStr 2 by A3;
let k be Nat;
A14: k is Element of NAT by ORDINAL1:def 13;
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 A14, A4;
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 6;
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;
reconsider x as Nat by A7, A4, NECKLACE:4;
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 N by NAT_1:45;
then [x,x] in iMRn by A5, A6, Th40;
hence contradiction by A3, A8, A9, NECKLACE:def 6;
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 set such that
A7: x in cMRn1 and
A8: y in cMRn1 and
A9: [x,y] in iMRn1;
reconsider xp1 = x, yp1 = y as Nat by A5, A7, A8, NECKLACE:4;
A10: [xp1,yp1] in iMRn1 by A9;
per cases by A10, A4, Th38;
suppose xp1 < N & yp1 < N;
then xp1 in N & yp1 in N by NAT_1:45;
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 N by A12, NAT_1:45;
yy +N < N + N by A14, A15;
then yy < N by XREAL_1:8;
then A17: yy in N by NAT_1:45;
[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 N by A20, NAT_1:45;
xx+N < N+N by A21, A19;
then xx < N by XREAL_1:8;
then A23: xx in N by NAT_1:45;
[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;