:: 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;