:: Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received February 8, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies MATROID0, NAT_1, FINSET_1, CARD_1, ARYTM_3, SUBSET_1, XXREAL_0,
CLASSES1, SGRAPH1, SIMPLEX0, TARSKI, GRAPH_1, GLIB_000, PBOOLE, XBOOLE_0,
ZFMISC_1, NUMBERS, FUNCT_1, RELAT_1, COMBGRAS, MYCIELSK, DILWORTH,
CIRCUIT2, AOFA_000, EQREL_1, PEPIN, CIRCUIT1, FUNCT_2, ARYTM_1, PROB_1,
BSPACE, STRUCT_0, NEWTON, STIRL2_1, UPROOTS, FINSEQ_1, CARD_3, FINSEQ_2,
PROB_2, GROUP_10, RAMSEY_1, SCMYCIEL;
notations TARSKI, XBOOLE_0, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2, MATROID0,
XCMPLX_0, NAT_1, FINSET_1, ENUMSET1, FINSEQ_1, FINSEQ_2, CARD_1,
SUBSET_1, XXREAL_0, ZFMISC_1, NUMBERS, NEWTON, UPROOTS, RVSUM_1, PROB_2,
FUNCOP_1, CLASSES1, AOFA_000, EQREL_1, BSPACE, STIRL2_1, PBOOLE,
CARD_LAR, MYCIELSK, GROUP_10, RAMSEY_1, CARD_3;
constructors MATROID0, LEXBFS, UPROOTS, CARD_LAR, RVSUM_1, BSPACE, STIRL2_1,
BINOP_2, PROB_2, DOMAIN_1, CLASSES1, MYCIELSK, RAMSEY_1, RELSET_1,
COHSP_1;
registrations FINSET_1, XXREAL_0, ORDINAL1, SETFAM_1, RELSET_1, XREAL_0,
NAT_1, SUBSET_1, EQREL_1, CARD_1, NEWTON, VALUED_0, XBOOLE_0, PARTFUN1,
FUNCT_2, SIMPLEX0, MYCIELSK, ZFMISC_1, FINSEQ_1, COHSP_1, STIRL2_1;
requirements SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
definitions TARSKI, XBOOLE_0, FUNCT_1, CLASSES1, FINSET_1;
equalities TARSKI, MYCIELSK, BSPACE, FINSEQ_2, GROUP_10, EQREL_1, CARD_3,
ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSET_1;
theorems TARSKI, XXREAL_0, XBOOLE_0, NAT_1, ZFMISC_1, ENUMSET1, CARD_1,
CARD_2, EULER_1, FUNCT_1, FUNCT_2, EQREL_1, FINSET_1, XREAL_1, MYCIELSK,
XBOOLE_1, BSPACE, CLASSES1, XREGULAR, WELLORD2, STIRL2_1, RVSUM_1,
DIST_1, FINSEQ_3, FINSEQ_1, FUNCOP_1, PROB_2, FINSEQ_2, DILWORTH,
PENCIL_1, RELAT_1, PARTFUN1, PBOOLE, NEWTON, RAMSEY_1, TOPGEN_2,
SUBSET_1, ORDERS_1, FINSEQ_4, XTUPLE_0;
schemes CLASSES1, FUNCT_1, FUNCT_2, NAT_1, FRAENKEL, SUBSET_1, RECDEF_1,
PRE_CIRC, FINSEQ_2;
begin :: Preliminaries
:: Could not find in MML
theorem Th1:
for x being object, X being set holds not [x,X] in X
proof
let x be object, X be set;
A1: X in {x, X} by TARSKI:def 2;
{x, X} in {{x, X}, {x}} by TARSKI:def 2;
hence thesis by A1,XREGULAR:7;
end;
theorem Th2:
for x, X being object holds [x,X] <> X
proof
let x, X be object;
assume
A1: [x,X] = X;
reconsider X as set by TARSKI:1;
{x,X} in X by TARSKI:def 2,A1;
hence contradiction by TARSKI:def 2;
end;
theorem Th3:
for x, X being object holds [x,X] <> x
proof
let x, X be object;
assume
A1: [x,X] = x;
reconsider x as set by TARSKI:1;
{x,X} in x by TARSKI:def 2,A1;
hence contradiction by TARSKI:def 2;
end;
theorem Th4:
for x1,y1,x2,y2 being object, X being set
st x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]}
holds x1 = x2 & y1 = y2
proof
let x1,y1,x2,y2 be object,X be set;
assume that A1: x1 in X and A2: x2 in X;
assume A3: {x1,[y1,X]} = {x2,[y2,X]};
per cases by A3,ZFMISC_1:6;
suppose x1 = x2 & [y1,X] = [y2,X];
hence x1 = x2 & y1 = y2 by XTUPLE_0:1;
end;
suppose x1 = x2 & [y1,X] = x2;
hence x1 = x2 & y1 = y2 by Th1,A2;
end;
suppose x1 = [y2,X] & [y1,X] = x2;
hence x1 = x2 & y1 = y2 by Th1,A2;
end;
suppose x1 = [y2,X] & [y1,X] = [y2,X];
hence x1 = x2 & y1 = y2 by Th1,A1;
end;
end;
theorem Th5: :: belongs to PENCIL_1
for X being set, v being object st 3 c= card X
ex v1, v2 being object st v1 in X & v2 in X & v1<>v & v2<>v & v1<>v2
proof
let X be set, v be object;
assume 3 c= card X;
then consider x,y,z being object such that
A1: x in X and
A2: y in X and
A3: z in X and
A4: x<>y and
A5: x<>z and
A6: y<>z by PENCIL_1:5;
v <> x & v <> y & v <> z or v = x or v = y or v = z;
hence ex v1, v2 being object
st v1 in X & v2 in X & v1<>v & v2<>v & v1<>v2 by A1,A2,A3,A4,A5,A6;
end;
theorem Th6:
for x being set holds singletons {x} = { {x} }
proof
let x be set;
A1: {x} c= {x};
thus singletons {x} c= { {x} } proof
let a be object;
assume a in singletons {x};
then consider f being Subset of {x} such that
A2: a = f and
A3: f is 1-element;
f = {} or f = {x} by ZFMISC_1:33;
hence thesis by A2,A3,TARSKI:def 1;
end;
let a be object;
assume a in {{x}};
then a = {x} by TARSKI:def 1;
hence thesis by A1;
end;
registration
cluster finite-yielding for FinSequence;
existence proof
take <*{}*>;
thus thesis;
end;
end;
theorem Th7:
for X being non empty finite set, P being a_partition of X
st card P < card X
ex p being set, x, y being object st p in P & x in p & y in p & x <> y
proof
let X be non empty finite set, P be a_partition of X such that
A1: card P < card X;
A2: card P in Segm card X by A1,NAT_1:44;
consider x,y being object such that
A3: x in X and
A4: y in X and
A5: x <> y and
A6: (proj P).x = (proj P).y by A2,FINSEQ_4:65;
take p = (proj P).x;
take x, y;
thus p in P by A3,FUNCT_2:5;
thus x in p & y in p by A3,A4,A6,EQREL_1:def 9;
thus x <> y by A5;
end;
registration
cluster union {{}} -> empty;
correctness;
end;
theorem Th8:
for x being set holds union { {}, {x} } = {x}
proof
let x be set;
{x} = union bool {x} by ZFMISC_1:81;
hence thesis by ZFMISC_1:24;
end;
theorem Th9: :: variant of SUBSET_1:46 or CARD_1:65
for X being set, s being Subset of X
st s is 1-element
ex x being set st x in X & s = {x}
proof
let X be set, s be Subset of X;
assume s is 1-element;
then s is trivial non empty;
then consider x being Element of s such that
A1: s = {x} by SUBSET_1:46;
take x;
x in s by A1;
hence x in X;
thus s = {x} by A1;
end;
theorem Th10:
for X being set holds
card { {X,[x,X]} where x is Element of X : x in X } = card X
proof
let X be set;
set uG = X; set A = { {uG,[x,uG]} where x is Element of uG : x in uG };
deffunc F(object) = {uG,[$1,uG]};
consider f being Function such that
A1: dom f = uG and
A2: for x being object st x in uG holds f.x = F(x) from FUNCT_1:sch 3;
now
let x1,x2 be object;
assume that A3: x1 in dom f and A4: x2 in dom f and A5: f.x1 = f.x2;
F(x1) = f.x1 & F(x2) = f.x2 by A3,A4,A1,A2;
then [x1,uG] = uG or [x1,uG] = [x2,uG] by A5,ZFMISC_1:6;
hence x1 = x2 by Th2,XTUPLE_0:1;
end;
then A6: f is one-to-one;
A7: rng f = A proof
thus rng f c= A proof
let y be object;
assume y in rng f;
then consider a being object such that
A8: a in dom f and
A9: f.a = y by FUNCT_1:def 3;
y = {uG,[a,uG]} by A8,A9,A1,A2;
hence thesis by A8,A1;
end;
thus A c= rng f proof
let a be object;
assume a in A;
then consider x being Element of uG such that
A10: a = {uG,[x,uG]} and
A11: x in uG;
f.x = a by A10,A11,A2;
hence thesis by A1,A11,FUNCT_1:def 3;
end;
end;
A, uG are_equipotent by A1,A6,A7,WELLORD2:def 4;
hence card A = card uG by CARD_1:5;
end;
definition
let G be set;
func PairsOf G -> Subset of G means :Def1:
for e being set holds e in it iff e in G & card e = 2;
existence proof
defpred P[set] means card $1 = 2;
consider X being Subset of G such that
A1: for x being set holds x in X iff x in G & P[x] from SUBSET_1:sch 1;
take X;
thus thesis by A1;
end;
uniqueness proof
let it1, it2 be Subset of G such that
A2: for e being set holds e in it1 iff e in G & card e = 2 and
A3: for e being set holds e in it2 iff e in G & card e = 2;
now
let x be object;
reconsider xx = x as set by TARSKI:1;
x in it2 iff x in G & card xx = 2 by A3;
hence x in it1 iff x in it2 by A2;
end;
hence it1 = it2 by TARSKI:2;
end;
end;
theorem Th11:
for X being set, e being set
st e in PairsOf X
ex x, y being set st x <> y & x in union X & y in union X & e = {x, y}
proof
let G be set, e be set; assume
A1: e in PairsOf G; then
card e = 2 by Def1; then
consider x, y being object such that
A2: x <> y and
A3: e = {x,y} by CARD_2:60;
x in e & y in e by A3,TARSKI:def 2;
then x in union G & y in union G by A1,TARSKI:def 4;
hence thesis by A2,A3;
end;
theorem Th12:
for X being set, x, y being object st x <> y & {x, y} in X
holds {x, y} in PairsOf X
proof
let X be set, x, y be object such that
A1: x <> y and
A2: {x, y} in X;
card {x,y} = 2 by A1,CARD_2:57;
hence {x, y} in PairsOf X by A2,Def1;
end;
theorem Th13:
for X being set, x, y being object
st {x, y} in PairsOf X holds x <> y & x in union X & y in union X
proof
let G be set, a, b be object;
assume {a, b} in PairsOf G;
then consider x, y being set such that
A1: x <> y and
A2: x in union G & y in union G and
A3: {a,b} = {x, y} by Th11;
a = x & b = y or a = y & b = x by A3,ZFMISC_1:6;
hence thesis by A2,A1;
end;
theorem Th14:
for G, H being set st G c= H holds PairsOf G c= PairsOf H
proof
let G, H be set; assume
A1: G c= H;
let e be object;
reconsider ee=e as set by TARSKI:1;
assume A2: e in PairsOf G;
A3: card ee = 2 by A2,Def1;
e in G by A2;
hence thesis by A1,A3,Def1;
end;
theorem Th15:
for X being finite set holds
card { {x,[y, union X]} where x, y is Element of union X
: {x,y} in PairsOf X } = 2 * card PairsOf X
proof
let G be finite set; set Y = union G;
set A = { {x,[y,Y]} where x, y is Element of union G : {x,y} in PairsOf G };
set EG = PairsOf G; set uG = union G;
set s = canFS(EG);
A1: len s = card EG by FINSEQ_1:93;
A2: rng s = EG by FUNCT_2:def 3;
defpred P[object,object] means
for a, b being set st $1 = {a, b} holds $2 = {{a,[b,Y]},{b,[a,Y]}};
A3: for x,y1,y2 being object st x in EG & P[x,y1] & P[x,y2] holds y1 = y2
proof let x,v1,v2 be object such that
A4: x in EG and
A5: P[x,v1] and
A6: P[x,v2];
consider x1, y1 being set such that
x1 <> y1 and x1 in union G and y1 in union G and
A7: x = {x1, y1} by A4,Th11;
v2 = {{x1,[y1,Y]},{y1,[x1,Y]}} by A7,A6;
hence v1 = v2 by A7,A5;
end;
A8: for x being object st x in EG ex y being object st P[x,y]
proof
let x be object;
assume x in EG;
then consider x1, y1 being set such that
x1 <> y1 and x1 in union G and y1 in union G and
A9: x = {x1, y1} by Th11;
take y = {{x1,[y1,Y]},{y1,[x1,Y]}};
let a, b be set;
assume x = {a, b};
then a=x1 & b=y1 or a=y1 & b = x1 by A9,ZFMISC_1:6;
hence y = {{a,[b,Y]},{b,[a,Y]}};
end;
consider f being Function such that
A10: dom f = EG and
A11: for x being object st x in EG holds P[x,f.x] from FUNCT_1:sch 2(A3,A8);
now
let y be set;
assume y in rng (f*s);
then y in rng f by FUNCT_1:14;
then consider x being object such that
A12: x in dom f and
A13: y = f.x by FUNCT_1:def 3;
consider x1, y1 being set such that
x1 <> y1 and x1 in union G and y1 in union G and
A14: x = {x1, y1} by A12,A10,Th11;
y = {{x1,[y1,Y]},{y1,[x1,Y]}} by A14,A13,A12,A10,A11;
hence y is finite;
end;
then reconsider S = f*s as finite-yielding FinSequence
by A2,A10,FINSEQ_1:16,FINSET_1:def 2;
A15: dom S = dom s by A2,A10,RELAT_1:27;
deffunc F(set) = card (S.$1);
consider L being FinSequence of NAT such that
A16: len L = len S and
A17: for j being Nat st j in dom L holds L.j = F(j) from FINSEQ_2:sch 1;
A18: dom S = dom L by A16,FINSEQ_3:29;
A19: for i be Nat st i in dom S holds S.i is finite & L.i = card (S.i) by A18,
A17;
now
let x, y be object;
assume A20: x <> y;
per cases;
suppose that A21: x in dom S and A22: y in dom S;
A23: x in dom s & s.x in dom f by A21,FUNCT_1:11;
A24: y in dom s & s.y in dom f by A22,FUNCT_1:11;
consider x1,y1 being set such that
x1 <> y1 and
A25: x1 in union G & y1 in union G and
A26: s.x = {x1, y1} by A23,A10,Th11;
consider x2,y2 being set such that
x2 <> y2 and
A27: x2 in union G & y2 in union G and
A28: s.y = {x2, y2} by A24,A10,Th11;
A29: S.x = f.(s.x) by A21,FUNCT_1:12;
A30: S.y = f.(s.y) by A22,FUNCT_1:12;
A31: S.x = {{x1,[y1,Y]},{y1,[x1,Y]}} by A26,A29,A23,A10,A11;
A32: S.y = {{x2,[y2,Y]},{y2,[x2,Y]}} by A28,A30,A24,A10,A11;
assume S.x meets S.y;
then consider a being object such that
A33: a in S.x and
A34: a in S.y by XBOOLE_0:3;
A35: a = {x1,[y1,Y]} or a = {y1,[x1,Y]} by A33,A31,TARSKI:def 2;
A36: a = {x2,[y2,Y]} or a = {y2,[x2,Y]} by A34,A32,TARSKI:def 2;
x1 = x2 & y1 = y2 or x1 = y2 & y1 = x2 or y1 = x2 & x1 = y2
by A25,A27,A35,A36,Th4;
hence contradiction by A26,A28,A20,A23,A24,FUNCT_1:def 4;
end;
suppose not (x in dom S & y in dom S);
then S.x = {} or S.y = {} by FUNCT_1:def 2;
hence S.x misses S.y;
end;
end; then
A37: S is disjoint_valued by PROB_2:def 2;
Union S = union rng S; then
A38: card (union rng S) = Sum L by A18,A19,A37,DIST_1:17;
A39: dom ((len L) |-> 2) = Seg len L by FUNCOP_1:13
.= dom L by FINSEQ_1:def 3;
now let j be Nat such that
A40: j in dom L;
A41: S.j = f.(s.j) by A40,A18,FUNCT_1:12;
consider x, y being set such that
A42: x <> y and x in union G and y in union G and
A43: s.j = {x, y} by Th11,A40,A18,A15,A2,FUNCT_1:3;
A44: f.(s.j) = {{x,[y,Y]},{y,[x,Y]}} by A43,A11,A40,A18,A15,A2,FUNCT_1:3;
A45: now assume {x,[y,Y]} = {y,[x,Y]};
then x= y or x = [x,Y] by ZFMISC_1:6;
hence contradiction by A42,Th3;
end;
A46: j in Seg len L by A40,FINSEQ_1:def 3;
thus L.j = card (S.j) by A40,A17
.= 2 by A45,A44,A41,CARD_2:57
.= ((len L) |-> 2).j by A46,FINSEQ_2:57;
end;
then
A47: L = (len L) |-> 2 by A39;
A48: len L = card EG by A16,A15,A1,FINSEQ_3:29;
union rng S = A proof
thus union rng S c= A proof
let a be object;
assume a in union rng S;
then consider YY being set such that
A49: a in YY and
A50: YY in rng S by TARSKI:def 4;
consider b being object such that
A51: b in dom S and
A52: YY = S.b by A50,FUNCT_1:def 3;
A53: S.b = f.(s.b) by A51,FUNCT_1:12;
A54: s.b in EG by A51,A15,A2,FUNCT_1:3;
consider x, y being set such that x <> y and
A55: x in union G and
A56: y in union G and
A57: s.b = {x, y} by Th11,A51,A15,A2,FUNCT_1:3;
f.(s.b) = {{x,[y,Y]},{y,[x,Y]}} by A57,A11,A51,A15,A2,FUNCT_1:3;
then a = {x,[y,Y]} or a = {y,[x,Y]} by A49,A52,A53,TARSKI:def 2;
hence a in A by A57,A54,A55,A56;
end;
thus A c= union rng S proof
let a be object;
assume a in A;
then consider x, y being Element of uG such that
A58: a = {x,[y,Y]} and
A59: {x,y} in EG;
consider c being object such that c in dom s and
A60: s.c = {x,y} by A59,A2,FUNCT_1:def 3;
rng S = rng f by A10,A2,RELAT_1:28;
then A61: f.(s.c) in rng S by A10,A60,A59,FUNCT_1:3;
f.(s.c) = {{x,[y,Y]},{y,[x,Y]}} by A60,A59,A11;
then a in f.(s.c) by A58,TARSKI:def 2;
hence a in union rng S by A61,TARSKI:def 4;
end;
end;
hence card A = 2 * card EG by A38,A47,A48,RVSUM_1:80;
end;
theorem :: ordunordpairs:
for X being finite set holds
card {[x, y] where x, y is Element of union X
: {x,y} in PairsOf X } = 2 * card PairsOf X
proof
let X be finite set;
set Y = union X;
set B = {[x, y] where x, y is Element of Y : {x,y} in PairsOf X };
set A = { {x,[y,Y]} where x, y is Element of Y : {x,y} in PairsOf X };
per cases;
suppose A1: B is empty;
now
assume A is non empty;
then consider a being object such that
A2: a in A;
consider x, y being Element of union X such that a = {x, [y, Y]} and
A3: {x,y} in PairsOf X by A2;
[x,y] in B by A3;
hence contradiction by A1;
end;
hence card B = 2 * card PairsOf X by A1,Th15;
end;
suppose A4: B is non empty;
then consider b being object such that
A5: b in B;
consider x, y being Element of Y such that b = [x, y] and
A6: {x,y} in PairsOf X by A5;
A7: x in {x,y} by TARSKI:def 2;
A8: Y <> {} by A6,A7,TARSKI:def 4;
defpred P[object, object] means
for a, b being Element of Y st a in Y & b in Y & $1 = {a,[b,Y]}
holds $2 = [a,b];
A9: for c being object st c in A ex d being object st d in B & P[c,d]
proof
let c be object;
assume c in A;
then consider x, y being Element of union X such that
A10: c = {x, [y, Y]} and
A11: {x,y} in PairsOf X;
take d = [x,y];
thus d in B by A11;
thus P[c,d] proof
let a, b be Element of Y;
assume A12: a in Y & b in Y;
assume c = {a,[b,Y]};
then a = x & b = y by A10,A12,Th4;
hence d = [a,b];
end;
end;
consider f being Function of A, B such that
A13: for c being object st c in A holds P[c,f.c] from FUNCT_2:sch 1(A9);
A14: dom f = A by A4,FUNCT_2:def 1;
A15: f is one-to-one proof
let c1,c2 be object such that
A16: c1 in dom f and
A17: c2 in dom f and
A18: f.c1 = f.c2;
consider x1, y1 being Element of Y such that
A19: c1 = {x1,[y1,Y]} and {x1,y1} in PairsOf X by A16,A14;
consider x2, y2 being Element of Y such that
A20: c2 = {x2,[y2,Y]} and {x2,y2} in PairsOf X by A17,A14;
A21: f.c1 = [x1,y1] by A13,A16,A14,A8,A19;
A22: f.c2 = [x2,y2] by A13,A17,A14,A8,A20;
x1 = x2 & y1 = y2 by A18,A21,A22,XTUPLE_0:1;
hence c1 = c2 by A19,A20;
end;
A23: rng f = B proof
thus rng f c= B proof
let b be object;
assume b in rng f;
then consider a being object such that
A24: a in dom f and
A25: b = f.a by FUNCT_1:def 3;
consider x, y being Element of Y such that
A26: a = {x,[y,Y]} and
A27: {x,y} in PairsOf X by A24,A14;
A28: b = [x,y] by A25,A24,A13,A14,A8,A26;
thus b in B by A28,A27;
end;
thus B c= rng f proof
let b be object;
assume A29: b in B;
consider x, y being Element of Y such that
A30: b = [x, y] and
A31: {x,y} in PairsOf X by A29;
set a = {x,[y,Y]};
A32: a in A by A31;
A33: f.a = b by A32,A13,A30,A8;
thus b in rng f by A32,A33,A14,FUNCT_1:3;
end;
end;
A34: f is onto by A23,FUNCT_2:def 3;
thus card B = card A by A15,A34,A4,EULER_1:11
.= 2 * card PairsOf X by Th15;
end;
end;
registration
let X be finite set;
cluster PairsOf X -> finite;
coherence;
end;
definition
let X be set;
attr X is void means :Def2:
X = {{}};
end;
registration
cluster void for set;
existence by Def2;
end;
registration
cluster void -> finite for set;
coherence;
end;
registration
let G be void set;
cluster union G -> empty;
coherence proof
G = {{}} by Def2;
hence thesis;
end;
end;
theorem Th17:
for X being set st X is void holds PairsOf X = {}
proof
let G be set such that
A1: G is void;
assume PairsOf G <> {};
then consider x being object such that
A2: x in PairsOf G by XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
A3: card x = 2 by A2,Def1;
G = {{}} by A1;
then x = {} by A2,TARSKI:def 1;
hence thesis by A3;
end;
theorem Th18:
for X being set st union X = {} holds X = {} or X = {{}}
proof
let X be set such that
A1: union X = {};
assume X <> {};
then consider x being object such that
A2: x in X by XBOOLE_0:def 1;
thus X = {{}} proof
thus X c= {{}} proof
let a be object;
assume a in X;
then a = {} by A1,ORDERS_1:6;
hence thesis by TARSKI:def 1;
end;
let a be object;
assume a in {{}};
then a = {} by TARSKI:def 1;
hence a in X by A2,A1,ORDERS_1:6;
end;
end;
definition
let X be set;
attr X is pairfree means
PairsOf X is empty;
end;
theorem Th19:
for X, x being set st card union X = 1 holds X is pairfree
proof
let G, x be set;
assume A1: card union G = 1;
assume not G is pairfree;
then PairsOf G <> {};
then consider e being object such that
A2: e in PairsOf G by XBOOLE_0:def 1;
consider x, y being set such that
A3: x <> y and
A4: x in union G and
A5: y in union G and
e = {x, y} by A2,Th11;
consider w being object such that
A6: union G = {w} by A1,CARD_2:42;
x = w by A4,A6,TARSKI:def 1;
hence contradiction by A3,A5,A6,TARSKI:def 1;
end;
Lm1:
for X being set
holds union { V where V is finite Subset of X : card V <= 2} = X
proof
let X be set;
set G = { V where V is finite Subset of X : card V <= 2};
thus union G c= X proof
let x be object;
assume x in union G;
then consider a being set such that
A1: x in a and
A2: a in G by TARSKI:def 4;
consider V being finite Subset of X such that
A3: a = V & card V <= 2 by A2;
thus x in X by A1,A3;
end;
thus X c= union G proof
let x be object;
A4: card {x} = 1 by CARD_1:30;
A5: x in {x} by TARSKI:def 1;
assume x in X;
then {x} c= X by ZFMISC_1:31;
then {x} in G by A4;
hence x in union G by A5,TARSKI:def 4;
end;
end;
registration
cluster finite-membered non empty for set;
existence proof
take {{}};
thus thesis;
end;
end;
registration
let X be finite-membered set, Y be set;
cluster X /\ Y -> finite-membered;
coherence proof
let x be set;
assume x in X /\ Y;
then x in X by XBOOLE_0:def 4;
hence thesis;
end;
cluster X \ Y -> finite-membered;
coherence;
end;
begin :: Simple graphs as simplicial complexes
definition
let n be Nat;
let X be set;
attr X is n-at_most_dimensional means :Def4:
for x being set st x in X holds card x c= n+1;
end;
registration
let n be Nat;
cluster n-at_most_dimensional -> finite-membered for set;
correctness proof
let X be set;
assume A1: X is n-at_most_dimensional;
thus X is finite-membered proof
let x be set;
assume x in X;
then card x c= n+1 by A1;
hence x is finite;
end;
end;
end;
Lm2:
for n being Nat holds {{}} is n-at_most_dimensional
proof
let n be Nat;
set E = {{}};
thus {{}} is n-at_most_dimensional proof
let x be set;
assume x in E;
then x = {} by TARSKI:def 1;
hence card x c= n+1;
end;
end;
registration
let n be Nat;
cluster n-at_most_dimensional subset-closed non empty for set;
existence proof
set E = {{}};
take E;
thus thesis by Lm2;
end;
end;
theorem Th20:
for G being subset-closed non empty set holds {} in G
proof let G be subset-closed non empty set;
consider z being object such that
A1: z in G by XBOOLE_0:def 1;
reconsider z as set by TARSKI:1;
{} c= z;
hence {} in G by A1,CLASSES1:def 1;
end;
theorem Th21:
for n being Nat, X being n-at_most_dimensional set,
x being Element of X
st x in X holds card x <= n+1
proof let n be Nat, X be n-at_most_dimensional set, x be Element of X;
assume x in X;
then
A1: card x c= n+1 by Def4;
reconsider x as finite set;
Segm card x c= Segm(n+1) by A1;
hence thesis by NAT_1:39;
end;
registration
let n be Nat;
let X, Y be n-at_most_dimensional set;
cluster X \/ Y -> n-at_most_dimensional;
coherence proof
let x be set;
assume A1: x in X \/ Y;
x in X or x in Y by A1,XBOOLE_0:def 3;
hence card x c= n+1 by Def4;
end;
end;
registration
let n be Nat;
let X be n-at_most_dimensional set, Y be set;
cluster X /\ Y -> n-at_most_dimensional;
coherence proof
let x be set;
assume x in X /\ Y;
then x in X by XBOOLE_0:def 4;
hence card x c= n+1 by Def4;
end;
cluster X \ Y -> n-at_most_dimensional;
coherence by Def4;
end;
registration
let n be Nat, X be n-at_most_dimensional set;
cluster -> n-at_most_dimensional for Subset of X;
correctness by Def4;
end;
definition
let s be set;
attr s is SimpleGraph-like means
s is 1-at_most_dimensional subset-closed non empty;
end;
registration
cluster SimpleGraph-like ->
1-at_most_dimensional subset-closed non empty for set;
correctness;
cluster 1-at_most_dimensional subset-closed non empty
-> SimpleGraph-like for set;
correctness;
end;
theorem Th22:
{{}} is SimpleGraph-like
by Lm2;
registration
cluster {{}} -> SimpleGraph-like;
correctness by Th22;
end;
registration
cluster SimpleGraph-like for set;
existence by Th22;
end;
definition
mode SimpleGraph is SimpleGraph-like set;
end;
registration
cluster void for SimpleGraph;
existence proof
reconsider G = {{}} as SimpleGraph;
take G;
thus thesis;
end;
cluster finite for SimpleGraph;
existence by Th22;
end;
notation :: meant for graphs
let G be set;
synonym Vertices G for union G;
synonym Edges G for PairsOf G;
end;
notation
let X be set;
synonym X is edgeless for X is pairfree;
end;
theorem Th23:
for G being SimpleGraph st Vertices G is finite holds G is finite
proof
let G be SimpleGraph;
assume A1: Vertices G is finite;
G c= bool Vertices G by ZFMISC_1:82;
hence G is finite by A1;
end;
theorem Th24:
for G being SimpleGraph, x being object holds x in Vertices G iff {x} in G
proof
let G be SimpleGraph, x be object;
thus x in Vertices G implies {x} in G proof
assume x in Vertices G;
then consider y being set such that
A1: x in y and
A2: y in G by TARSKI:def 4;
{x} c= y by A1,ZFMISC_1:31;
hence {x} in G by A2,CLASSES1:def 1;
end;
x in {x} by TARSKI:def 1;
hence thesis by TARSKI:def 4;
end;
theorem Th25:
for x being set holds { {}, {x} } is SimpleGraph
proof
let x be set;
set H = { {}, {x} };
A1: H is 1-at_most_dimensional
proof
let a be set such that
A2: a in H;
per cases by A2,TARSKI:def 2;
suppose a = {};
hence card a c= 1+1;
end;
suppose a = {x};
then
A3: card a = 1 by CARD_1:30;
Segm 1 c= Segm(1+1) by NAT_1:39;
hence card a c= 1+1 by A3;
end;
end;
H is subset-closed proof
let X,Y be set such that
A4: X in H and
A5: Y c= X;
per cases by A4,TARSKI:def 2;
suppose X = {};
then Y = {} by A5;
hence Y in H by TARSKI:def 2;
end;
suppose A6: X = {x};
per cases by A6,A5,ZFMISC_1:33;
suppose Y = {};
hence Y in H by TARSKI:def 2;
end;
suppose Y = {x};
hence Y in H by TARSKI:def 2;
end;
end;
end;
hence { {}, {x} } is SimpleGraph by A1;
end;
definition :: meant for graphs
let X be finite finite-membered set;
func order X -> Nat equals
card union X;
coherence;
end;
definition :: meant for graphs
let X be finite set;
func size X -> Nat equals card PairsOf X;
coherence;
end;
theorem Th26:
for G being finite SimpleGraph holds order G <= card G
proof
let G be finite SimpleGraph;
set uG = union G;
A1: card singletons uG = card uG by BSPACE:41;
singletons uG c= G proof
let x be object;
assume x in singletons uG;
then consider f being Subset of uG such that
A2: x = f and
A3: f is 1-element;
consider a being set such that
A4: a in uG and
A5: f = {a} by A3,Th9;
consider y being set such that
A6: a in y and
A7: y in G by A4,TARSKI:def 4;
{a} c= y by A6,ZFMISC_1:31;
hence x in G by A7,A5,A2,CLASSES1:def 1;
end;
hence order G <= card G by A1,NAT_1:43;
end;
definition
let G be SimpleGraph;
mode Vertex of G is Element of Vertices G;
mode Edge of G is Element of Edges G;
end;
theorem Th27:
for G being SimpleGraph holds G = { {} } \/ singletons Vertices G \/ Edges G
proof let G be SimpleGraph;
thus G c= { {} } \/ singletons Vertices G \/ Edges G proof
let x be object;
assume A1: x in G;
reconsider v = x as finite set by A1;
card v <= 1+1 by A1,Th21;
then card v = 0 or ... or card v = 2;
then per cases;
suppose card v = 0;
then v = {};
then v in {{}} by TARSKI:def 1;
then v in {{}} \/ singletons Vertices G by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose card v = 1;
then consider a being object such that
A2: v = {a} by CARD_2:42;
A3: a in v by A2,TARSKI:def 1;
A4: a in union G by A3,A1,TARSKI:def 4;
reconsider v as Subset of Vertices G by A4,A2,ZFMISC_1:31;
v in singletons Vertices G by A2;
then v in {{}} \/ singletons Vertices G by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose card v = 2;
then v in Edges G by A1,Def1;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus { {} } \/ singletons Vertices G \/ Edges G c= G proof
let x be object;
assume x in { {} } \/ singletons Vertices G \/ Edges G;
then A5: x in { {} } \/ singletons Vertices G or x in Edges G
by XBOOLE_0:def 3;
per cases by A5,XBOOLE_0:def 3;
suppose A6: x in { {} };
consider z being object such that
A7: z in G by XBOOLE_0:def 1;
reconsider z as set by TARSKI:1;
A8: {} c= z;
x = {} by A6,TARSKI:def 1;
hence x in G by A8,A7,CLASSES1:def 1;
end;
suppose x in singletons Vertices G;
then consider f being Subset of Vertices G such that
A9: x = f and
A10: f is 1-element;
consider v being set such that
A11: v in Vertices G and
A12: f = {v} by A10,Th9;
thus x in G by A9,A11,A12,Th24;
end;
suppose x in Edges G;
hence x in G;
end;
end;
end;
theorem Th28:
for G being SimpleGraph st Vertices G = {} holds G is void by Th18;
theorem Th29:
for G being SimpleGraph, x being set
st x in G & x <> {}
holds (ex y being set st x = {y} & y in Vertices G) or x in Edges G
proof
let G be SimpleGraph, x be set such that
A1: x in G and
A2: x <> {};
x in { {} } \/ singletons Vertices G \/ Edges G by A1,Th27;
then x in {{}} \/ singletons Vertices G or x in Edges G by XBOOLE_0:def 3;
then A3: x in {{}} or x in singletons Vertices G or x in Edges G
by XBOOLE_0:def 3;
per cases by A3,A2,TARSKI:def 1;
suppose x in singletons Vertices G;
then consider f being Subset of Vertices G such that
A4: x = f and
A5: f is 1-element;
consider v being set such that
A6: v in Vertices G and
A7: f = {v} by A5,Th9;
thus thesis by A7,A6,A4;
end;
suppose x in Edges G;
hence thesis;
end;
end;
theorem :: Gsingle:
for G being SimpleGraph, x being set st Vertices G = {x} holds G = { {}, {x} }
proof
let G be SimpleGraph, a be set such that
A1: Vertices G = {a};
A2: now
assume Edges G <> {};
then consider e being object such that
A3: e in Edges G by XBOOLE_0:def 1;
consider x, y being set such that
A4: x <> y and
A5: x in Vertices G and
A6: y in Vertices G and e = {x, y} by A3,Th11;
x = a by A5,A1,TARSKI:def 1;
hence contradiction by A4,A6,A1,TARSKI:def 1;
end;
A7: singletons Vertices G = { {a} } by A1,Th6;
thus G = { {} } \/ singletons Vertices G \/ Edges G by Th27
.= { {}, {a} } by A7,A2,ENUMSET1:1;
end;
theorem Th31:
for X being set ex G being SimpleGraph st G is edgeless & Vertices G = X
proof
let X be set;
set G = {{}} \/ singletons X;
A1: G is subset-closed proof
let x,y be set; assume that
A2: x in G and
A3: y c= x;
per cases by A2,XBOOLE_0:def 3;
suppose x in {{}};
then x = {} by TARSKI:def 1;
then y = {} by A3;
then y in {{}} by TARSKI:def 1;
hence y in G by XBOOLE_0:def 3;
end;
suppose x in singletons X;
then consider f being Subset of X such that
A4: x = f and
A5: f is 1-element;
consider v being set such that v in X and
A6: f = {v} by A5,Th9;
per cases by A3,A4,A6,ZFMISC_1:33;
suppose y = {};
then y in {{}} by TARSKI:def 1;
hence y in G by XBOOLE_0:def 3;
end;
suppose y = {v};
hence y in G by A2,A6,A4;
end;
end;
end;
A7: G is 1-at_most_dimensional proof
let x be set;
assume A8: x in G;
per cases by A8,XBOOLE_0:def 3;
suppose x in {{}};
then x = {} by TARSKI:def 1;
hence card x c= 1+1;
end;
suppose x in singletons X;
then consider f being Subset of X such that
A9: x = f and
A10: f is 1-element;
consider v being set such that v in X and
A11: f = {v} by A10,Th9;
A12: card x = 1 by A9,A11,CARD_1:30;
Segm 1 c= Segm(1+1) by NAT_1:39;
hence card x c= 1+1 by A12;
end;
end;
reconsider G as SimpleGraph by A1,A7;
take G;
now
assume Edges G <> {};
then consider e being object such that
A13: e in Edges G by XBOOLE_0:def 1;
reconsider e as set by TARSKI:1;
A14: e in G & card e = 2 by A13,Def1;
per cases by A13,XBOOLE_0:def 3;
suppose e in {{}};
hence contradiction by A14,CARD_1:27,TARSKI:def 1;
end;
suppose e in singletons X;
then consider f being Subset of X such that
A15: e = f and
A16: f is 1-element;
consider v being set such that v in X and
A17: f = {v} by A16,Th9;
thus contradiction by A14,A15,A17,CARD_1:30;
end;
end;
hence G is edgeless;
thus Vertices G = X proof
thus Vertices G c= X proof
let x be object;
assume x in Vertices G;
then consider y being set such that
A18: x in y and
A19: y in G by TARSKI:def 4;
per cases by A19,XBOOLE_0:def 3;
suppose y in {{}};
hence thesis by A18,TARSKI:def 1;
end;
suppose y in singletons X;
then consider f being Subset of X such that
A20: y = f and
f is 1-element;
thus x in X by A20,A18;
end;
end;
thus X c= Vertices G proof
let x be object;
assume x in X;
then reconsider f = {x} as Subset of X by ZFMISC_1:31;
f is 1-element;
then {x} in singletons X;
then {x} in G by XBOOLE_0:def 3;
hence x in Vertices G by Th24;
end;
end;
end;
definition
let G be SimpleGraph, v be Element of Vertices G;
func Adjacent v -> Subset of Vertices G means :Def8:
for x being Element of Vertices G holds x in it iff {v, x} in Edges G;
existence proof
set A = {x where x is Element of Vertices G: {v,x} in Edges G};
A c= Vertices G proof
let a be object;
assume a in A;
then consider x being Element of Vertices G such that
A1: a = x and
A2: {v,x} in Edges G;
thus a in Vertices G by A1,A2,Th13;
end;
then reconsider A as Subset of Vertices G;
take A;
let x be Element of Vertices G;
hereby assume x in A;
then consider a being Element of Vertices G such that
A3: x = a and
A4: {v,a} in Edges G;
thus {v,x} in Edges G by A3,A4;
end;
thus thesis;
end;
uniqueness proof
let A1, A2 be Subset of Vertices G such that
A5: for x being Element of Vertices G holds x in A1 iff {v, x} in Edges G and
A6: for x being Element of Vertices G holds x in A2 iff {v, x} in Edges G;
thus A1 c= A2 proof
let x be object;
assume A7: x in A1;
then {v,x} in Edges G by A5;
hence thesis by A6,A7;
end;
thus A2 c= A1 proof
let x be object;
assume A8: x in A2;
then {v,x} in Edges G by A6;
hence thesis by A5,A8;
end;
end;
end;
definition
let X be set;
mode SimpleGraph of X -> SimpleGraph means :Def9:
Vertices it = X;
existence proof
consider G being SimpleGraph such that G is edgeless and
A1: Vertices G = X by Th31;
take G;
thus thesis by A1;
end;
end;
definition
let X be set;
func CompleteSGraph X -> SimpleGraph of X equals
{ V where V is finite Subset of X : card V <= 2};
coherence proof
set G = { V where V is finite Subset of X : card V <= 2};
A1: G is subset-closed proof
let x,y be set such that
A2: x in G and
A3: y c= x;
consider V be finite Subset of X such that
A4: x = V and
A5: card V <= 2 by A2;
reconsider y1 = y as finite Subset of X by A4,A3,XBOOLE_1:1;
card y1 <= card V by A3,A4,NAT_1:43;
then card y1 <= 2 by A5,XXREAL_0:2;
hence y in G;
end;
A6: G is 1-at_most_dimensional proof
let x be set;
assume x in G;
then consider V being finite Subset of X such that
A7: x = V and
A8: card V <= 2;
Segm card V c= Segm(1+1) by A8,NAT_1:39;
hence card x c= 1+1 by A7;
end;
A9: {} c= X;
card {} <= 2; then
{} in G by A9;
then reconsider G as SimpleGraph by A1,A6;
Vertices G = X by Lm1;
hence thesis by Def9;
end;
end;
theorem Th32:
for G being SimpleGraph
st (for x, y being set st x in Vertices G & y in Vertices G
holds {x, y} in G)
holds G = CompleteSGraph Vertices G
proof
let G be SimpleGraph such that
A1: for x, y being set st x in Vertices G & y in Vertices G
holds {x, y} in G;
set C = { V where V is finite Subset of Vertices G : card V <= 2};
C = G proof
thus C c= G proof
let a be object;
assume a in C;
then consider V being finite Subset of Vertices G such that
A2: a = V and
A3: card V <= 2;
card V = 0 or ... or card V = 2 by A3;
then per cases;
suppose card V = 0;
then V = {};
hence a in G by A2,Th20;
end;
suppose card V = 1;
then consider c being object such that
A4: V = {c} by CARD_2:42;
c in V by A4,TARSKI:def 1;
then {c,c} in G by A1;
hence a in G by A4,A2,ENUMSET1:29;
end;
suppose card V = 2;
then consider c,d being object such that
c <> d and
A5: V = {c, d} by CARD_2:60;
c in V & d in V by A5,TARSKI:def 2;
hence a in G by A1,A5,A2;
end;
end;
thus G c= C proof
let a be object;
assume A6: a in G;
then reconsider aa = a as finite set;
A7: card aa <= 1+1 by A6,Th21;
aa c= union G by A6,ZFMISC_1:74;
hence a in C by A7;
end;
end;
hence G = CompleteSGraph Vertices G;
end;
registration
let X be finite set;
cluster CompleteSGraph X -> finite;
correctness proof
set G = CompleteSGraph X;
G c= bool X proof
let x be object;
assume x in G;
then consider V being finite Subset of X such that
A1: x = V and card V <= 2;
thus x in bool X by A1;
end;
hence G is finite;
end;
end;
theorem Th33:
for X being set, x being set st x in X holds {x} in CompleteSGraph X
proof
let X be set, x be set such that
A1: x in X;
A2: {x} c= X by A1,ZFMISC_1:31;
A3: card {x} = 1 by CARD_1:30;
thus {x} in CompleteSGraph X by A3,A2;
end;
theorem Th34:
for X being set, x, y being set st x in X & y in X
holds {x,y} in CompleteSGraph X
proof
let X be set, x,y be set such that
A1: x in X and
A2: y in X;
A3: {x, y} c= X by A1,A2,ZFMISC_1:32;
A4: card {x,y} <= 2 by CARD_2:50;
thus {x,y} in CompleteSGraph X by A4,A3;
end;
theorem Th35:
CompleteSGraph {} = {{}}
proof
for x, y being set st x in union {{}} & y in union {{}}
holds {x,y} in {{}};
hence CompleteSGraph {} = {{}} by Th32;
end;
theorem Th36:
for x being set holds CompleteSGraph {x} = {{},{x}}
proof
let x be set;
thus CompleteSGraph {x} c= {{},{x}} proof
let a be object;
assume a in CompleteSGraph {x};
then consider V being finite Subset of {x} such that
A1: a = V and card V <= 2;
a = {} or a = {x} by A1,ZFMISC_1:33;
hence thesis by TARSKI:def 2;
end;
A2: {x} = Vertices CompleteSGraph {x} by Lm1;
A3: x in {x} by TARSKI:def 1;
thus {{},{x}} c= CompleteSGraph {x} proof
let a be object;
assume a in {{},{x}};
then a = {} or a = {x} by TARSKI:def 2;
hence thesis by A2,A3,Th20,Th24;
end;
end;
theorem Th37:
for x, y being set holds CompleteSGraph {x,y} = {{},{x},{y},{x,y}}
proof
let x, y be set;
thus CompleteSGraph {x,y} c= {{},{x},{y},{x,y}} proof
let a be object;
assume a in CompleteSGraph {x,y};
then consider V being finite Subset of {x,y} such that
A1: a = V and card V <= 2;
a = {} or a = {x} or a = {y} or a = {x,y} by A1,ZFMISC_1:36;
hence thesis by ENUMSET1:def 2;
end;
A2: {x,y} = Vertices CompleteSGraph {x,y} by Lm1;
A3: x in {x,y} by TARSKI:def 2;
A4: y in {x,y} by TARSKI:def 2;
A5: card {x,y} <= 2 by CARD_2:50;
thus {{},{x},{y},{x,y}} c= CompleteSGraph {x,y} proof
let a be object;
assume a in {{},{x},{y},{x,y}};
then a = {} or a = {x} or a = {y} or a = {x,y} by ENUMSET1:def 2;
hence thesis by A2,A3,A4,A5,Th20,Th24;
end;
end;
theorem
for X, Y being set st X c= Y holds CompleteSGraph X c= CompleteSGraph Y
proof
let X, Y be set such that
A1: X c= Y;
let a be object;
assume a in CompleteSGraph X;
then consider V being finite Subset of X such that
A2: a = V and
A3: card V <= 2;
V is Subset of Y by A1,XBOOLE_1:1;
hence a in CompleteSGraph Y by A2,A3;
end;
theorem Th39:
for G being SimpleGraph, x being set st x in Vertices G
holds CompleteSGraph {x} c= G
proof
let G be SimpleGraph, x be set such that
A1: x in Vertices G;
A2: CompleteSGraph {x} = { {}, {x} } by Th36;
A3: {} in G by Th20;
A4: {x} in G by A1,Th24;
thus CompleteSGraph {x} c= G by A2,A3,A4,ZFMISC_1:32;
end;
registration
let G be SimpleGraph;
cluster SimpleGraph-like for Subset of G;
existence proof
G c= G; then
reconsider H = G as Subset of G;
take H;
thus thesis;
end;
end;
definition
let G be SimpleGraph;
mode Subgraph of G is SimpleGraph-like Subset of G;
end;
Lm3: for G being SimpleGraph
holds (CompleteSGraph Vertices G) \ Edges G is SimpleGraph
proof
let G be SimpleGraph;
set CSGVG = CompleteSGraph Vertices G;
set C = CSGVG \ Edges G;
A1: {} in CSGVG by Th20;
now assume {} in Edges G;
then consider x, y being set such that
x <> y & x in Vertices G & y in Vertices G and
A2: {} = {x, y} by Th11;
thus contradiction by A2;
end;
then reconsider C as non empty set by A1,XBOOLE_0:def 5;
C is subset-closed proof
let X, Y be set such that
A3: X in C and
A4: Y c= X;
assume Y nin C;
then A5: Y nin CSGVG or Y in Edges G by XBOOLE_0:def 5;
A6: X in CSGVG & not X in Edges G by A3,XBOOLE_0:def 5;
A7: Y in Edges G by A4,A5,A6,CLASSES1:def 1;
A8: card Y = 2 by A7,Def1;
reconsider X as finite set by A3;
A9: card X <= 1+1 by A3,Th21;
A10: 2 <= card X by A8,A4,NAT_1:43;
card X = 2 by A9,A10,XXREAL_0:1;
hence contradiction by A6,A5,A4,A8,CARD_2:102;
end;
hence thesis;
end;
Lm4:
for G being SimpleGraph
holds Vertices G = Vertices ((CompleteSGraph Vertices G) \ Edges G)
proof
let G being SimpleGraph;
set CG = ((CompleteSGraph Vertices G) \ Edges G);
A1: CG is SimpleGraph by Lm3;
now
let a be object;
hereby assume a in Vertices G;
then A2: {a} in CompleteSGraph Vertices G by Th33;
now assume {a} in Edges G;
then {a, a} in Edges G by ENUMSET1:29;
hence contradiction by Th13;
end;
then {a} in CG by A2,XBOOLE_0:def 5;
hence a in Vertices CG by A1,Th24;
end;
assume a in Vertices CG;
then {a} in CG by A1,Th24;
then a in Vertices CompleteSGraph Vertices G by Th24;
hence a in Vertices G by Lm1;
end;
hence Vertices G = Vertices CG by TARSKI:2;
end;
Lm5:
for G being SimpleGraph, x, y being set
st x <> y & x in Vertices G & y in Vertices G
holds {x,y} in Edges G
iff {x,y} nin Edges ((CompleteSGraph Vertices G) \ Edges G)
proof
let G be SimpleGraph, x, y be set such that
A1: x <> y and
A2: x in Vertices G and
A3: y in Vertices G;
set CG = ((CompleteSGraph Vertices G) \ Edges G);
thus {x,y} in Edges G implies {x,y} nin Edges CG by XBOOLE_0:def 5;
assume A4: {x,y} nin Edges CG;
assume A5: {x,y} nin Edges G;
{x,y} in CompleteSGraph Vertices G by A2,A3,Th34;
then {x,y} in CG by A5,XBOOLE_0:def 5;
hence contradiction by A4,A1,Th12;
end;
Lm6:
for G, CG being SimpleGraph st CG = ((CompleteSGraph Vertices G) \ Edges G)
holds ((CompleteSGraph Vertices CG) \ Edges CG) = G
proof
let G, CG be SimpleGraph such that
A1: CG = ((CompleteSGraph Vertices G) \ Edges G);
set CCG = ((CompleteSGraph Vertices CG) \ Edges CG);
A2: Vertices G = Vertices CG by A1,Lm4;
A3: Vertices CG = Vertices CCG by Lm4;
CCG is SimpleGraph by Lm3; then
A4: CCG = { {} } \/ singletons Vertices CCG \/ Edges CCG by Th27;
A5: G = { {} } \/ singletons Vertices G \/ Edges G by Th27;
now let a be object;
hereby assume A6: a in Edges CCG;
then consider x, y being set such that
A7: x <> y and
A8: x in Vertices CCG & y in Vertices CCG and
A9: a = {x, y} by Th11;
{x,y} nin Edges CG by A7,A3,A6,A9,A8,Lm5;
hence a in Edges G by A7,A3,A2,A8,A9,A1,Lm5;
end;
assume A10: a in Edges G;
then consider x, y being set such that
A11: x <> y and
A12: x in Vertices G & y in Vertices G and
A13: a = {x, y} by Th11;
{x,y} nin Edges CG by A11,A10,A13,A12,A1,Lm5;
hence a in Edges CCG by A11,A2,A12,A13,Lm5;
end;
hence thesis by A2,A3,A4,A5,TARSKI:2;
end;
definition
let G be SimpleGraph;
func Complement G -> SimpleGraph equals
(CompleteSGraph Vertices G) \ Edges G;
correctness by Lm3;
involutiveness by Lm6;
end;
theorem :: Compl1:
for G being SimpleGraph holds Vertices G = Vertices Complement G by Lm4;
theorem :: Compl1a:
for G being SimpleGraph, x, y being set
st x <> y & x in Vertices G & y in Vertices G
holds {x,y} in Edges G iff {x,y} nin Edges Complement G by Lm5;
begin :: Induced Subgraphs
definition
let G be SimpleGraph, L be set;
func G SubgraphInducedBy L -> Subset of G equals
G /\ bool L;
coherence by XBOOLE_1:17;
end;
registration
let G be SimpleGraph, L be set;
cluster G SubgraphInducedBy L -> SimpleGraph-like;
coherence proof
set S = G /\ bool L;
A1: {} in G by Th20;
{} c= L;
then reconsider S as non empty set by A1,XBOOLE_0:def 4;
S is subset-closed;
hence thesis;
end;
end;
theorem :: Sub3b:
for G being SimpleGraph holds G = G SubgraphInducedBy Vertices G
proof
let G be SimpleGraph;
thus G c= G SubgraphInducedBy Vertices G proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A1: x in G;
A2: xx c= union G by A1,ZFMISC_1:74;
thus thesis by A1,A2,XBOOLE_0:def 4;
end;
thus thesis;
end;
theorem Th43:
for G being SimpleGraph, L being set
holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ Vertices G)
proof
let G be SimpleGraph, L be set;
thus G SubgraphInducedBy L c= G SubgraphInducedBy (L /\ Vertices G) proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A1: x in G SubgraphInducedBy L;
then A2: x in bool L by XBOOLE_0:def 4;
A3: xx c= Vertices G by A1,ZFMISC_1:74;
A4: xx c= L /\ Vertices G by A2,A3,XBOOLE_1:19;
thus x in G SubgraphInducedBy (L /\ Vertices G) by A1,A4,XBOOLE_0:def 4;
end;
thus G SubgraphInducedBy (L /\ Vertices G) c= G SubgraphInducedBy L proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A5: x in G SubgraphInducedBy (L /\ Vertices G);
then x in bool (L /\ Vertices G) by XBOOLE_0:def 4; then
A6: xx c= L by XBOOLE_1:18;
thus thesis by A5,A6,XBOOLE_0:def 4;
end;
end;
registration
let G be finite SimpleGraph, L be set;
cluster G SubgraphInducedBy L -> finite;
coherence;
end;
registration
let G be SimpleGraph, L be finite set;
cluster G SubgraphInducedBy L -> finite;
coherence;
end;
theorem Th44:
for G, H being SimpleGraph
st G c= H holds G c= H SubgraphInducedBy Vertices G
proof
let G, H be SimpleGraph;
assume A1: G c= H;
set L = Vertices G;
let g be object;
reconsider gg=g as set by TARSKI:1;
assume A2: g in G;
gg c= Vertices G by A2,ZFMISC_1:74;
hence g in H SubgraphInducedBy L by A2,A1,XBOOLE_0:def 4;
end;
Lm7:
for G being SimpleGraph, L being set, x being set
st x in Vertices (G SubgraphInducedBy L) holds x in L
proof
let G be SimpleGraph, L be set;
set S = G /\ bool L;
let x be set; assume
A1: x in Vertices (G SubgraphInducedBy L);
consider Y being set such that
A2: x in Y and
A3: Y in S by A1,TARSKI:def 4;
set y = Y;
Y in bool L by A3,XBOOLE_0:def 4;
hence x in L by A2;
end;
Lm8:
for G being SimpleGraph, L being set, x being set
st x in L & x in Vertices G holds x in Vertices (G SubgraphInducedBy L)
proof
let G be SimpleGraph, L be set, x be set such that
A1: x in L and
A2: x in Vertices G;
A3: {x} in G by A2,Th24;
A4: {x} c= L by A1,ZFMISC_1:31;
A5: {x} in (G SubgraphInducedBy L) by A3,A4,XBOOLE_0:def 4;
thus x in Vertices (G SubgraphInducedBy L) by A5,Th24;
end;
theorem Th45:
for G being SimpleGraph, L being set
holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L
proof
let G be SimpleGraph, L be set;
set S= G SubgraphInducedBy L; set uS = union S; set uG = union G;
union (G /\ bool L) c= union G /\ union bool L by ZFMISC_1:79;
hence uS c= uG /\ L by ZFMISC_1:81;
thus uG /\ L c= uS proof
let a be object;
assume a in uG /\ L;
then a in uG & a in L by XBOOLE_0:def 4;
hence a in uS by Lm8;
end;
end;
Lm9:
for G being SimpleGraph, L being set
st L c= Vertices G holds Vertices (G SubgraphInducedBy L) = L
proof
let G be SimpleGraph, L be set such that
A1: L c= union G;
thus Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L by Th45
.= L by A1,XBOOLE_1:28;
end;
Lm10:
for G being SimpleGraph, L, x, y being set
st x in L & y in L & {x, y} in G holds {x,y} in G SubgraphInducedBy L
proof
let G be SimpleGraph, L, x, y being set such that
A1: x in L and
A2: y in L and
A3: {x, y} in G;
{x,y} c= L by A1,A2,ZFMISC_1:32;
hence {x,y} in G SubgraphInducedBy L by A3,XBOOLE_0:def 4;
end;
theorem Th46:
for G being SimpleGraph, x being set
st x in Vertices G holds G SubgraphInducedBy {x} = { {}, {x} }
proof
let G be SimpleGraph, x being set such that
A1: x in Vertices G;
set Gx = G SubgraphInducedBy {x};
thus Gx c= { {}, {x} } proof
let a be object;
assume a in Gx;
then a in bool {x} by XBOOLE_0:def 4;
then a = {} or a = {x} by ZFMISC_1:33;
hence thesis by TARSKI:def 2;
end;
thus { {}, {x} } c= Gx proof
let a be object;
reconsider aa=a as set by TARSKI:1;
A2: {} in G & {x} in G by Th20,A1,Th24;
assume a in { {}, {x} };
then A3: a = {} or a = {x} by TARSKI:def 2;
then aa c= {x};
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
end;
begin :: Clique, clique number, clique cover
definition
let G be SimpleGraph;
attr G is clique means :Def13:
G = CompleteSGraph Vertices G;
end;
theorem Th47:
for G being SimpleGraph
st for x, y being set st x <> y & x in Vertices G & y in Vertices G
holds {x,y} in Edges G
holds G is clique
proof
let G be SimpleGraph such that
A1: for x, y being set st x <> y & x in Vertices G & y in Vertices G
holds {x,y} in Edges G;
now
let x, y be set such that
A2: x in Vertices G and
A3: y in Vertices G;
per cases;
suppose x <> y;
then {x,y} in Edges G by A2,A3,A1;
hence {x, y} in G;
end;
suppose x = y;
then {x,y} = {x} by ENUMSET1:29;
hence {x,y} in G by A2,Th24;
end;
end;
then G = CompleteSGraph Vertices G by Th32;
hence G is clique;
end;
theorem Th48:
{{}} is clique
by Th35;
registration
cluster clique for SimpleGraph;
existence by Th48;
let G be SimpleGraph;
cluster clique for Subgraph of G;
existence proof
{} in G by Th20;
then reconsider S = {{}} as Subgraph of G by ZFMISC_1:31;
take S;
thus thesis by Th48;
end;
end;
definition
let G be SimpleGraph;
mode Clique of G is clique Subgraph of G;
end;
theorem Th49:
for X being set holds (CompleteSGraph X) is clique
by Lm1;
registration
let X be set;
cluster CompleteSGraph X -> clique;
correctness by Th49;
end;
theorem Th50:
for G being SimpleGraph, x being set st x in Vertices G
holds { {}, {x} } is Clique of G
proof
let G be SimpleGraph, x be set such that
A1: x in Vertices G;
set C = CompleteSGraph {x};
A2: C = { {}, {x} } by Th36;
thus { {}, {x} } is Clique of G by A2,A1,Th39;
end;
theorem Th51:
for G being SimpleGraph, x, y being set
st x in Vertices G & y in Vertices G & {x,y} in G
holds { {}, {x}, {y}, {x,y} } is Clique of G
proof
let G be SimpleGraph, x, y be set such that
A1: x in Vertices G and
A2: y in Vertices G and
A3: {x,y} in G;
set C = CompleteSGraph {x,y};
A4: C = { {}, {x}, {y}, {x,y} } by Th37;
C c= G proof
let a be object;
assume A5: a in C;
per cases by A5,A4,ENUMSET1:def 2;
suppose a = {};
hence thesis by Th20;
end;
suppose a = {x};
hence thesis by A1,Th24;
end;
suppose a = {y};
hence thesis by A2,Th24;
end;
suppose a = {x,y};
hence thesis by A3;
end;
end;
hence { {}, {x}, {y}, {x,y} } is Clique of G by Th37;
end;
registration
let G be SimpleGraph;
cluster finite for Clique of G;
existence proof
{} in G by Th20;
then reconsider C = {{}} as Subgraph of G by ZFMISC_1:31;
C is clique by Th48;
hence thesis;
end;
end;
theorem Th52:
for G being SimpleGraph, x being set st x in union G
ex C being finite Clique of G st Vertices C = {x}
proof
let G be SimpleGraph, x be set such that
A1: x in union G;
set C = CompleteSGraph {x};
A2: C = { {}, {x} } by Th36;
reconsider C as finite Clique of G by A1,A2,Th50;
take C;
thus Vertices C = {x} by A2,Th8;
end;
theorem Th53:
for C being clique SimpleGraph, u, v being set
st u in Vertices C & v in Vertices C holds {u, v} in C
proof
let C be clique SimpleGraph, u, v be set such that
A1: u in Vertices C and
A2: v in Vertices C;
C = CompleteSGraph Vertices C by Def13;
hence thesis by A1,A2,Th34;
end;
definition
let G be SimpleGraph;
attr G is with_finite_clique# means :Def14:
ex C being finite Clique of G
st for D being finite Clique of G holds order D <= order C;
end;
registration
cluster with_finite_clique# for SimpleGraph;
existence proof
take G = the void SimpleGraph;
{} in G by Th20; then {{}} c= G by ZFMISC_1:31;
then reconsider C = {{}} as finite Clique of G by Th48;
take C;
let D be finite Clique of G;
union D c= union G by ZFMISC_1:77;
hence order D <= order C;
end;
end;
registration
cluster finite -> with_finite_clique# for SimpleGraph;
coherence proof
let G be SimpleGraph;
assume G is finite;
then reconsider R9 = G as finite SimpleGraph;
defpred P[Nat] means ex c being finite Clique of G st order c = $1;
A1: for k being Nat st P[k] holds k <= card R9
proof
let k be Nat;
assume P[k];
then consider c being finite Clique of G such that
A2: order c = k;
A3: card c <= card R9 by NAT_1:43;
order c <= card c by Th26;
hence k <= card R9 by A2,A3,XXREAL_0:2;
end;
{} in G by Th20; then {{}} c= G by ZFMISC_1:31; then
reconsider E = {{}} as finite Clique of G by Th48;
order E = 0; then
A4: ex k being Nat st P[k];
consider k being Nat such that
A5: P[k] and
A6: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1,A4);
consider c being finite Clique of G such that
A7: order c = k by A5;
for D be finite Clique of G holds order(D) <= order(c) by A7,A6;
hence G is with_finite_clique#;
end;
end;
definition
let G be with_finite_clique# SimpleGraph;
func clique# G -> Nat means :Def15:
(ex C being finite Clique of G st order C = it)
& for T being finite Clique of G holds order T <= it;
existence proof
consider C be finite Clique of G such that
A1: for D being finite Clique of G holds order D <= order C by Def14;
take itt = order C;
thus ex A being finite Clique of G st order A = itt;
let T being finite Clique of G;
thus order T <= itt by A1;
end;
uniqueness proof
let it1, it2 be Nat such that
A2: ex C being finite Clique of G st order C = it1 and
A3: for T being finite Clique of G holds order T <= it1 and
A4: ex C being finite Clique of G st order C = it2 and
A5: for T being finite Clique of G holds order T <= it2;
consider C1 being finite Clique of G such that
A6: order C1 = it1 by A2;
consider C2 being finite Clique of G such that
A7: order C2 = it2 by A4;
it1 <= it2 & it2 <= it1 by A3,A5,A6,A7;
hence it1 = it2 by XXREAL_0:1;
end;
end;
theorem Th54:
for G being with_finite_clique# SimpleGraph
st clique# G = 0 holds Vertices G = {}
proof
let G be with_finite_clique# SimpleGraph;
assume
A1: clique# G = 0;
assume Vertices G <> {};
then consider v being object such that
A2: v in Vertices G by XBOOLE_0:def 1;
consider D being finite Clique of G such that
A3: Vertices D = {v} by A2,Th52;
order D <= 0 by A1,Def15;
hence contradiction by A3;
end;
theorem
for G being void SimpleGraph holds clique# G = 0
proof
let G be void SimpleGraph;
assume A1: clique# G <> 0;
consider C being finite Clique of G such that
A2: order C = clique# G by Def15;
Vertices C c= Vertices G by ZFMISC_1:77;
hence contradiction by A1,A2;
end;
theorem Th56:
for G being SimpleGraph, x, y being set
st {x,y} in G holds G SubgraphInducedBy {x,y} is Clique of G
proof
let G be SimpleGraph, x, y be set such that
A1: {x,y} in G;
set S = G SubgraphInducedBy {x,y};
now
let a, b be set such that
A2: a in union S and
A3: b in union S;
A4: a in {x,y} & b in {x,y} by A2,A3,Lm7;
then A5: (a = x or a = y) & (b = x or b = y) by TARSKI:def 2;
per cases;
suppose a = b;
then {a,b} = {a} by ENUMSET1:29;
hence {a,b} in S by A2,Th24;
end;
suppose a <> b;
hence {a,b} in S by A4,A5,A1,Lm10;
end;
end;
then S = CompleteSGraph Vertices S by Th32;
hence G SubgraphInducedBy {x,y} is Clique of G;
end;
theorem Th57:
for G being with_finite_clique# SimpleGraph
st Edges G <> {} holds clique# G >= 2
proof
let G be with_finite_clique# SimpleGraph such that
A1: Edges G <> {};
consider e being object such that
A2: e in Edges G by A1,XBOOLE_0:def 1;
consider x, y being set such that
A3: x <> y and
A4: x in Vertices G and
A5: y in Vertices G and
A6: e = {x, y} by A2,Th11;
reconsider S = G SubgraphInducedBy {x,y} as finite Clique of G by A6,A2,Th56
;
A7: Vertices S = (Vertices G) /\ {x,y} by Th45;
A8: {x,y} c= Vertices G by A4,A5,ZFMISC_1:32;
Vertices S = {x,y} by A7,A8,XBOOLE_1:28;
then order S = 2 by A3,CARD_2:57;
hence clique# G >= 2 by Def15;
end;
theorem Th58: :: CliqueSubno0:
for G, H being with_finite_clique# SimpleGraph
st G c= H holds clique# G <= clique# H
proof
let G, H be with_finite_clique# SimpleGraph such that
A1: G c= H;
consider D being finite Clique of G such that
A2: order D = clique# G by Def15;
D is Clique of H by A1,XBOOLE_1:1;
hence clique# G <= clique# H by A2,Def15;
end;
theorem Th59:
for X being finite set holds clique# CompleteSGraph X = card X
proof
let X be finite set;
set G = CompleteSGraph X;
A1: order G = card X by Lm1;
A2: G c= G;
for T being finite Clique of G holds order T <= order G
by NAT_1:43,ZFMISC_1:77;
hence clique# CompleteSGraph X = card X by A1,A2,Def15;
end;
definition
let G be SimpleGraph, P be a_partition of Vertices G;
attr P is Clique-wise means :Def16:
for x being set st x in P holds G SubgraphInducedBy x is Clique of G;
end;
registration
let G be SimpleGraph;
cluster Clique-wise for a_partition of Vertices G;
correctness proof
set VG = Vertices G;
per cases;
suppose VG is empty;
then reconsider S = {} as a_partition of VG by EQREL_1:45;
take S;
thus S is Clique-wise;
end;
suppose VG is non empty;
then reconsider cRp1 = VG as non empty set;
set S = SmallestPartition VG;
A1: S = the set of all {x} where x is Element of cRp1 by EQREL_1:37;
take S;
now let z being set;
assume A2: z in S;
consider x being Element of cRp1 such that
A3: z = {x} by A1,A2;
G SubgraphInducedBy z = { {}, {x} } by A3,Th46;
hence G SubgraphInducedBy z is Clique of G by Th50;
end;
hence S is Clique-wise;
end;
end;
end;
definition
let G be SimpleGraph;
mode Clique-partition of G is Clique-wise a_partition of Vertices G;
end;
registration
let G be void SimpleGraph;
cluster empty -> Clique-wise for a_partition of Vertices G;
correctness;
end;
definition
let G be SimpleGraph;
attr G is with_finite_cliquecover# means :Def17:
ex C being Clique-partition of G st C is finite;
end;
registration
cluster finite -> with_finite_cliquecover# for SimpleGraph;
correctness proof
let G be SimpleGraph;
assume A1: G is finite; set VG = Vertices G;
per cases;
suppose VG is empty;
then reconsider S = {} as a_partition of VG by EQREL_1:45;
for x being set st x in S holds G SubgraphInducedBy x is Clique of G;
then reconsider S as Clique-partition of G by Def16;
take S;
thus S is finite;
end;
suppose A2: VG is non empty;
defpred P[set] means not contradiction;
reconsider cRp1 = VG as finite non empty set by A2,A1;
set S = SmallestPartition VG;
deffunc F(set) = {$1};
A3: S = {F(x) where x is Element of cRp1: P[x]} by EQREL_1:37;
A4: {F(x) where x is Element of cRp1: P[x]} is finite from PRE_CIRC:sch 1;
now let z be set;
assume A5: z in S;
consider x being Element of VG such that
A6: z = {x} by A5,A3;
G SubgraphInducedBy z = { {}, {x} } by A6,A2,Th46;
hence G SubgraphInducedBy z is Clique of G by A2,Th50;
end;
then reconsider S as Clique-partition of G by Def16;
take S;
thus thesis by A4;
end;
end;
end;
registration
let G be with_finite_cliquecover# SimpleGraph;
cluster finite for Clique-partition of G;
correctness by Def17;
end;
registration
let G be with_finite_cliquecover# SimpleGraph, S be Subset of Vertices G;
cluster G SubgraphInducedBy S -> with_finite_cliquecover#;
correctness proof
set H = G SubgraphInducedBy S;
consider C being Clique-partition of G such that
A1: C is finite by Def17;
reconsider VH = Vertices H as Subset of Vertices G by ZFMISC_1:77;
reconsider D = C | VH as a_partition of Vertices H;
now
let p being set such that
A2: p in D;
set Hp = H SubgraphInducedBy p;
now
let x, y be set such that
A3: x in union Hp and
A4: y in union Hp;
consider c being Element of C such that
A5: p = c /\ VH and c meets VH by A2;
A6: x in p by A3,Lm7;
A7: y in p by A4,Lm7;
A8: x in VH by A5,A6,XBOOLE_0:def 4;
A9: y in VH by A5,A7,XBOOLE_0:def 4;
set Gc = G SubgraphInducedBy c;
A10: Gc is Clique of G by A8,Def16;
A11: Gc = CompleteSGraph Vertices Gc by A10,Def13;
x in c & y in c by A6,A7,A5,XBOOLE_0:def 4;
then x in Vertices Gc & y in Vertices Gc by Lm8;
then A12: {x,y} in Gc by A11,Th34;
x in S & y in S by A8,A9,Lm7;
then {x, y} c= S by ZFMISC_1:32;
then A13: {x, y} in H by A12,XBOOLE_0:def 4;
{x,y} c= p by A6,A7,ZFMISC_1:32;
hence {x,y} in Hp by A13,XBOOLE_0:def 4;
end;
then Hp = CompleteSGraph Vertices Hp by Th32;
hence Hp is Clique of H;
end;
then reconsider D as Clique-partition of H by Def16;
take D;
thus D is finite by A1;
end;
end;
definition
let G be with_finite_cliquecover# SimpleGraph;
func cliquecover# G -> Nat means :Def18:
(ex C being finite Clique-partition of G st card C = it)
& for C being finite Clique-partition of G holds it <= card C;
existence proof
defpred P[Nat] means ex C being finite Clique-partition of G st card C = $1;
consider C being Clique-partition of G such that
A1: C is finite by Def17;
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 G st card C = n by A3;
let C be finite Clique-partition of G;
thus n <= card C by A4;
end;
uniqueness proof
let it1, it2 be Nat such that
A5: (ex C being finite Clique-partition of G st card C = it1) and
A6: for C being finite Clique-partition of G holds it1 <= card C and
A7: (ex C being finite Clique-partition of G st card C = it2) and
A8: for C being finite Clique-partition of G holds it2 <= card C;
consider C1 being finite Clique-partition of G such that
A9: card C1 = it1 by A5;
consider C2 being finite Clique-partition of G 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;
begin :: Stable set, coloring
definition
let G be SimpleGraph, S be Subset of Vertices G;
attr S is stable means :Def19:
for x, y being set st x <> y & x in S & y in S holds {x,y} nin G;
end;
theorem
for G being SimpleGraph holds {}(Vertices G) is stable;
theorem Th61:
for G being SimpleGraph, S being Subset of Vertices G, v being object
st S = {v} holds S is stable
proof
let G be SimpleGraph, S be Subset of Vertices G, v be object such that
A1: S = {v};
let x, y be set such that
A2: x <> y and
A3: x in S & y in S;
x = v & y = v by A1,A3,TARSKI:def 1;
hence {x,y} nin G by A2;
end;
registration
let G be SimpleGraph;
cluster trivial -> stable for Subset of Vertices G;
coherence proof
let S be Subset of Vertices G;
assume A1: S is trivial;
per cases by A1,ZFMISC_1:131;
suppose S is empty;
then S = {}(Vertices G);
hence thesis;
end;
suppose ex c being object st S = {c};
then consider c being object such that
A2: S = {c};
thus thesis by A2,Th61;
end;
end;
end;
registration
let G be SimpleGraph;
cluster stable for Subset of Vertices G;
existence proof
take {}(Vertices G);
thus thesis;
end;
end;
definition
let G be SimpleGraph;
mode StableSet of G is stable Subset of Vertices G;
:: other possible names: AntiChain of R, IndependentSet of R
end;
theorem Th62:
for G being SimpleGraph, x, y being set
st x in Vertices G & y in Vertices G & {x,y} nin G
holds {x, y} is StableSet of G
proof
let G be SimpleGraph, x, y be set such that
A1: x in Vertices G and
A2: y in Vertices G and
A3: {x,y} nin G;
reconsider S = {x,y} as Subset of Vertices G by A1,A2,ZFMISC_1:32;
S is stable proof
let a, b be set such that
A4: a <> b and
A5: a in S and
A6: b in S;
(a = x or a = y) & (b = x or b = y) by A5,A6,TARSKI:def 2;
hence {a,b} nin G by A3,A4;
end;
hence {x, y} is StableSet of G;
end;
theorem Th63: :: Height4:
for G being with_finite_clique# SimpleGraph st clique# G = 1
holds Vertices G is StableSet of G
proof
let R be with_finite_clique# SimpleGraph;
assume A1: clique# R = 1;
set cR = Vertices R;
A2: cR c= cR;
now
let a, b be set such that
A3: a <> b & a in cR & b in cR;
A4: {a,b} c= cR by A3,ZFMISC_1:32;
assume {a, b} in R;
then reconsider H = R SubgraphInducedBy {a,b} as finite Clique of R
by Th56;
Vertices H = {a,b} by A4,Lm9;
then order H = 2 by A3,CARD_2:57;
hence contradiction by A1,Def15;
end;
hence cR is StableSet of R by A2,Def19;
end;
registration
let G be SimpleGraph;
cluster finite for StableSet of G;
existence proof
take {}(Vertices G);
thus thesis;
end;
end;
theorem Th64: :: AChain0:
for G being SimpleGraph, A being StableSet of G, B being Subset of A
holds B is StableSet of G
proof
let R be SimpleGraph, A be StableSet of R, B be Subset of A;
set VR = Vertices R;
reconsider BB = B as Subset of VR by XBOOLE_1:1;
BB is stable by Def19;
hence thesis;
end;
definition
let G be SimpleGraph, P be a_partition of Vertices G;
attr P is StableSet-wise means :Def20:
for x being set st x in P holds x is StableSet of G;
end;
theorem Th65:
for G being SimpleGraph holds SmallestPartition Vertices G is StableSet-wise
proof
let G be SimpleGraph;
set C = SmallestPartition Vertices G;
let c be set such that
A1: c in C;
consider a being object such that
a in Vertices G and
A2: c = Class(id Vertices G, a) by A1,EQREL_1:def 3;
reconsider cc = c as Subset of Vertices G by A1;
A3: cc is stable proof
let x, y be set such that
A4: x <> y and
A5: x in cc and
A6: y in cc;
A7: [a,x] in id Vertices G by A5,A2,RELAT_1:169;
A8: [a,y] in id Vertices G by A6,A2,RELAT_1:169;
A9: a = y by A8,RELAT_1:def 10;
thus {x,y} nin G by A7,A9,A4,RELAT_1:def 10;
end;
thus c is StableSet of G by A3;
end;
registration
let G be SimpleGraph;
cluster StableSet-wise for a_partition of Vertices G;
existence proof
take SmallestPartition Vertices G;
thus thesis by Th65;
end;
end;
definition
let G be SimpleGraph;
mode Coloring of G is StableSet-wise a_partition of Vertices G;
end;
definition
let G be SimpleGraph;
attr G is finitely_colorable means :Def21:
ex C being Coloring of G st C is finite;
end;
registration
cluster finitely_colorable for SimpleGraph;
existence proof
take G = the finite SimpleGraph;
SmallestPartition Vertices G is Coloring of G by Th65;
hence thesis;
end;
end;
registration
cluster finite -> finitely_colorable for SimpleGraph;
correctness proof
let G be SimpleGraph;
assume A1: G is finite;
SmallestPartition Vertices G is Coloring of G by Th65;
hence thesis by A1;
end;
end;
registration
let G be finitely_colorable SimpleGraph;
cluster finite for Coloring of G;
existence by Def21;
end;
theorem Th66:
for G being SimpleGraph, S being Clique of G, L being set
st L c= Vertices S holds G SubgraphInducedBy L is Clique of G
proof
let G be SimpleGraph, S be Clique of G, L be set such that
A1: L c= Vertices S;
set g = G SubgraphInducedBy L;
now let x, y be set such that
A2: x in union g and
A3: y in union g;
A4: x in L by A2,Lm7;
A5: y in L by A3,Lm7;
A6: {x,y} in S by A4,A5,A1,Th53;
thus {x,y} in g by A4,A5,A6,Lm10;
end;
then g = CompleteSGraph Vertices g by Th32;
hence g is Clique of G;
end;
theorem Th67:
for G being SimpleGraph, C being Coloring of G, S being Subset of Vertices G
holds C | S is Coloring of (G SubgraphInducedBy S)
proof
let G be SimpleGraph, C be Coloring of G, S be Subset of Vertices G;
set g = G SubgraphInducedBy S;
A1: Vertices g = S /\ Vertices G by Th45 .= S by XBOOLE_1:28;
reconsider CS = C | S as a_partition of Vertices g by A1;
CS is StableSet-wise proof
let x be set such that
A2: x in CS;
reconsider xx = x as Subset of Vertices g by A2;
consider z being Element of C such that
A3: xx = z /\ S and z meets S by A2;
xx is stable proof
let x, y be set such that
A4: x <> y and
A5: x in xx and
A6: y in xx;
assume A7: {x,y} in g;
A8: x in z by A3,A5,XBOOLE_0:def 4;
A9: y in z by A6,A3,XBOOLE_0:def 4;
z is StableSet of G by A3,A5,Def20;
hence contradiction by A7,A4,A8,A9,Def19;
end;
hence x is StableSet of g;
end;
hence C | S is Coloring of g;
end;
registration
let G be finitely_colorable SimpleGraph, S be set;
cluster G SubgraphInducedBy S -> finitely_colorable;
coherence proof
consider C being Coloring of G such that
A1: C is finite by Def21;
reconsider C as finite Coloring of G by A1;
reconsider SX = S /\ Vertices G as Subset of Vertices G by XBOOLE_1:17;
A2: G SubgraphInducedBy SX = G SubgraphInducedBy S by Th43;
reconsider D = C | SX as Coloring of G SubgraphInducedBy S by Th67,A2;
take D;
thus D is finite;
end;
end;
definition
let G be finitely_colorable SimpleGraph;
func chromatic# G -> Nat means :Def22:
(ex C being finite Coloring of G st card C = it)
& for C being finite Coloring of G holds it <= card C;
existence proof
defpred P[Nat] means ex C being finite Coloring of G st card C = $1;
consider C being Coloring of G such that
A1: C is finite by Def21;
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 G st card C = n by A3;
let C be finite Coloring of G;
thus n <= card C by A4;
end;
uniqueness proof
let it1, it2 be Nat such that
A5: ex C being finite Coloring of G st card C = it1 and
A6: for C being finite Coloring of G holds it1 <= card C and
A7: ex C being finite Coloring of G st card C = it2 and
A8: for C being finite Coloring of G holds it2 <= card C;
consider C1 being finite Coloring of G such that
A9: card C1 = it1 by A5;
consider C2 being finite Coloring of G 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;
theorem Th68:
for G, H being finitely_colorable SimpleGraph
st G c= H holds chromatic# G <= chromatic# H
proof
let G, H be finitely_colorable SimpleGraph;
assume A1: G c= H;
then reconsider S = Vertices G as Subset of Vertices H by ZFMISC_1:77;
set g = H SubgraphInducedBy S;
A2: G c= g by A1,Th44;
consider C being finite Coloring of H such that
A3: card C = chromatic# H by Def22;
reconsider g as finitely_colorable SimpleGraph;
reconsider Cg = C | S as finite Coloring of g by Th67;
A4: Vertices G = Vertices g by Lm9;
A5: G c= g proof
let a be object;
assume a in G;
then a in { {} } \/ singletons Vertices G \/ Edges G by Th27;
then A6: a in { {} } \/ singletons Vertices G or a in Edges G
by XBOOLE_0:def 3;
per cases by A6,XBOOLE_0:def 3;
suppose a in {{}};
then a = {} by TARSKI:def 1;
hence a in g by Th20;
end;
suppose a in singletons Vertices G;
then a in {{}} \/ singletons Vertices g by A4,XBOOLE_0:def 3;
then a in {{}} \/ singletons Vertices g \/ Edges g by XBOOLE_0:def 3;
hence a in g by Th27;
end;
suppose a in Edges G;
then a in G;
hence a in g by A2;
end;
end;
reconsider Cg1 = Cg as a_partition of Vertices G;
Cg1 is StableSet-wise proof
let x be set such that
A7: x in Cg1;
reconsider xx = x as Subset of Vertices G by A7;
reconsider xxx = x as Subset of Vertices g by A7;
xx is stable proof
let x, y be set such that
A8: x <> y and
A9: x in xx and
A10: y in xx;
A11: xxx is stable by A7,Def20;
assume {x,y} in G;
hence contradiction by A5,A8,A9,A10,A11;
end;
hence x is StableSet of G;
end; then
A12: card Cg >= chromatic# G by Def22;
card C >= card (C | S) by MYCIELSK:8;
hence chromatic# G <= chromatic# H by A12,A3,XXREAL_0:2;
end;
theorem Th69:
for X being finite set holds chromatic# CompleteSGraph X = card X
proof
let X be finite set;
set n = card X; set G = CompleteSGraph X; set D = SmallestPartition X;
A1: card D = card X by TOPGEN_2:12;
A2: Vertices G = X by Lm1;
reconsider D as a_partition of Vertices G by Lm1;
A3: D is StableSet-wise proof
let x be set;
assume A4: x in D;
then reconsider xx = x as Subset of Vertices G;
xx is stable proof
let x, y be set such that
A5: x <> y and
A6: x in xx and
A7: y in xx;
X is non empty by A4;
then D = the set of all {a} where a is Element of X
by EQREL_1:37;
then consider a being Element of X such that
A8: xx = {a} by A4;
a = x & y = a by A8,A6,A7,TARSKI:def 1;
hence {x,y} nin G by A5;
end;
hence x is StableSet of G;
end;
for C being finite Coloring of G holds card X <= card C proof
let C be finite Coloring of G;
assume A9: card X > card C;
then X is non empty;
then consider p being set, x, y being object such that
A10: p in C and
A11: x in p and
A12: y in p and
A13: x <> y by A9,A2,Th7;
A14: p is StableSet of G by A10,Def20;
reconsider p as Subset of Vertices G by A10;
A15: {x,y} nin G by A14,A11,A12,A13,Def19;
p c= X by A2;
hence contradiction by A11,A12,A15,Th34;
end;
hence chromatic# CompleteSGraph X = n by A1,A3,Def22;
end;
theorem Th70:
for G being finitely_colorable SimpleGraph,
C being finite Coloring of G, c being set
st c in C & card C = chromatic# G
ex v being Element of Vertices G st v in c &
for d being Element of C st d <> c
ex w being Element of Vertices G st w in Adjacent(v) & w in d
proof
let G be finitely_colorable SimpleGraph,
C be finite Coloring of G, c be set such that
A1: c in C and
A2: card C = chromatic# G;
assume
A3: not thesis;
set uG = Vertices G;
A4: union C = uG by EQREL_1:def 4;
reconsider c as Subset of uG by A1;
set Cc = C\{c};
A5: c in {c} by TARSKI:def 1;
per cases;
suppose A6: Cc is empty;
consider v being object such that
A7: v in c by A1,XBOOLE_0:def 1;
reconsider v as Element of uG by A7;
consider d being Element of C such that
A8: d <> c and for w being Element of uG
holds not (w in Adjacent(v) & w in d) by A7,A3;
0 = card C - card{c} by A1,A6,CARD_1:27,EULER_1:4;
then 0+1 = card C - 1 +1 by CARD_1:30;
then consider x being object such that
A9: C = {x} by CARD_2:42;
c = x & d = x by A1,A9,TARSKI:def 1;
hence thesis by A8;
end;
suppose Cc is non empty;
then reconsider Cc as non empty set;
defpred P[object, object] means
ex A being set st A = $2 &
for vv being Element of uG st $1 = vv
holds $2 <> c & $2 in C &
for w being Element of uG holds not (w in Adjacent(vv) & w in A);
A10: for e being object st e in c ex u being object st P[e,u]
proof
let v be object such that
A11: v in c;
reconsider vv = v as Element of uG by A11;
consider d being Element of C such that
A12: d <> c and
A13: for w being Element of uG
holds not (w in Adjacent(vv) & w in d) by A11,A3;
take d,d;
thus thesis by A12,A13,A1;
end;
consider r being Function such that
A14: dom r = c and
A15: for e being object st e in c holds P[e,r.e] from CLASSES1:sch 1(A10);
deffunc DF(set) = $1 \/ r"{$1};
reconsider Cc as finite non empty set;
defpred P[set] means not contradiction;
set D = { DF(d) where d is Element of Cc : P[d] };
consider d being object such that
A16: d in Cc by XBOOLE_0:def 1;
reconsider d as set by TARSKI:1;
A17: d \/ r"{d} in D by A16;
A18: D c= bool uG proof
let x be object;
assume x in D;
then consider d being Element of Cc such that
A19: x = d \/ r"{d};
A20: r"{d} c= c by A14,RELAT_1:132;
A21: r"{d} c= uG by A20,XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then d \/ r"{d} c= uG by A21,XBOOLE_1:8;
hence x in bool uG by A19;
end;
A22: union D = uG proof
thus union D c= uG proof
let x be object;
assume x in union D;
then consider Y being set such that
A23: x in Y and
A24: Y in D by TARSKI:def 4;
thus x in uG by A23,A24,A18;
end;
thus uG c= union D proof
let x be object;
assume A25: x in uG;
then consider d being set such that
A26: x in d and
A27: d in C by A4,TARSKI:def 4;
reconsider xp1 = x as Element of uG by A25;
per cases;
suppose A28: d = c;
P[xp1,r.xp1] by A26,A15,A28;
then r.xp1 <> c;
then A29: not r.xp1 in {c} by TARSKI:def 1;
P[xp1,r.xp1] by A26,A28,A15;
then r.xp1 in C; then
A30: r.xp1 in Cc by A29,XBOOLE_0:def 5;
r.xp1 in {r.xp1} by TARSKI:def 1;
then x in r"{r.xp1} by A26,A28,A14,FUNCT_1:def 7;
then A31: x in r.xp1 \/ r"{r.xp1} by XBOOLE_0:def 3;
r.xp1 \/ r"{r.xp1} in D by A30;
hence x in union D by A31,TARSKI:def 4;
end;
suppose d <> c;
then not d in {c} by TARSKI:def 1;
then d in Cc by A27,XBOOLE_0:def 5;
then A32: d \/ r"{d} in D;
x in d \/ r"{d} by A26,XBOOLE_0:def 3;
hence x in union D by A32,TARSKI:def 4;
end;
end;
end;
A33: for A being Subset of uG st A in D holds A <> {} &
for B being Subset of uG st B in D holds A = B or A misses B proof
let A be Subset of uG;
assume A in D;
then consider da being Element of Cc such that
A34: A = da \/ r"{da};
A35: da in C by XBOOLE_0:def 5;
hence A <> {} by A34;
let B be Subset of uG;
assume B in D;
then consider db being Element of Cc such that
A36: B = db \/ r"{db};
A37: db in C by XBOOLE_0:def 5;
per cases;
suppose da = db;
hence A = B or A misses B by A34,A36;
end;
suppose A38: da <> db;
then A39: da misses db by A35,A37,EQREL_1:def 4;
A40: r"{da} misses r"{db} by A38,FUNCT_1:71,ZFMISC_1:11;
assume A <> B;
assume A meets B;
then consider x being object such that
A41: x in A and
A42: x in B by XBOOLE_0:3;
per cases by A41,A42,A34,A36,XBOOLE_0:def 3;
suppose x in da & x in db;
hence contradiction by A39,XBOOLE_0:3;
end;
suppose that A43: x in da and A44: x in r"{db};
A45: da <> c by A5,XBOOLE_0:def 5;
r"{db} c= c by A14,RELAT_1:132;
then da meets c by A43,A44,XBOOLE_0:3;
hence contradiction by A45,A35,A1,EQREL_1:def 4;
end;
suppose that A46: x in r"{da} and A47: x in db;
A48: db <> c by A5,XBOOLE_0:def 5;
r"{da} c= c by A14,RELAT_1:132;
then db meets c by A46,A47,XBOOLE_0:3;
hence contradiction by A48,A37,A1,EQREL_1:def 4;
end;
suppose x in r"{da} & x in r"{db};
hence contradiction by A40,XBOOLE_0:3;
end;
end;
end;
reconsider D as a_partition of uG by A18,A22,A33,EQREL_1:def 4;
now
let x be set;
assume A49: x in D;
then reconsider S = x as Subset of uG;
consider d being Element of Cc such that
A50: x = d \/ r"{d} by A49;
A51: r"{d} c= c by A14,RELAT_1:132;
A52: d in C by XBOOLE_0:def 5;
A53: d is StableSet of G by A52,Def20;
A54: c is StableSet of G by A1,Def20;
S is stable proof
let a, b be set such that
A55: a <> b and
A56: a in S and
A57: b in S;
reconsider aa = a, bb = b as Vertex of G by A56,A57;
per cases by A56,A57,A50,XBOOLE_0:def 3;
suppose a in d & b in d;
hence not {a,b} in G by A53,A55,Def19;
end;
suppose that A58: a in d and A59: b in r"{d};
r.b in {d} by A59,FUNCT_1:def 7;
then
A60: r.b = d by TARSKI:def 1;
P[b,r.b] by A51,A59,A15;
then not a in Adjacent(bb) by A58,A60;
then not {aa,bb} in Edges G by Def8;
hence not {a,b} in G by A55,Th12;
end;
suppose that A61: a in r"{d} and A62: b in d;
r.a in {d} by A61,FUNCT_1:def 7;
then
A63: r.a = d by TARSKI:def 1;
P[a,r.a] by A51,A61,A15;
then not b in Adjacent(aa) by A62,A63;
then not {bb,aa} in Edges G by Def8;
hence not {a, b} in G by A55,Th12;
end;
suppose a in r"{d} & b in r"{d};
hence not {a,b} in G by A51,A54,A55,Def19;
end;
end;
hence x is StableSet of G;
end;
then reconsider D as Coloring of G by Def20;
card Cc = card C - card{c} by A1,EULER_1:4;
then card Cc + 1 = card C -1+1 by CARD_1:30;
then A64: card Cc < card C by NAT_1:13;
deffunc FS(set) = $1 \/ r"{$1};
consider s being Function such that
A65: dom s = Cc and
A66: for x being set st x in Cc holds s.x = FS(x) from FUNCT_1:sch 5;
A67: rng s c= D proof
let y be object;
assume y in rng s;
then consider d being object such that
A68: d in dom s and
A69: y = s.d by FUNCT_1:def 3;
reconsider d as set by TARSKI:1;
y = d \/ r"{d} by A65,A66,A68,A69;
hence y in D by A68,A65;
end;
then reconsider s as Function of Cc, D by A65,FUNCT_2:2;
A70: s is one-to-one proof
let x1, x2 be object such that
A71: x1 in dom s and
A72: x2 in dom s and
A73: s.x1 = s.x2;
reconsider x1,x2 as set by TARSKI:1;
A74: s.x1 = x1 \/ r"{x1} by A71,A66,A65;
A75: s.x2 = x2 \/ r"{x2} by A72,A66,A65;
A76: x1 c= x2 proof
let x be object;
assume A77: x in x1;
then A78: x in s.x1 by A74,XBOOLE_0:def 3;
per cases by A78,A73,A75,XBOOLE_0:def 3;
suppose x in x2;
hence thesis;
end;
suppose A79: x in r"{x2};
A80: r"{x2} c= dom r by RELAT_1:132;
A81: x1 in C by A65,A71,XBOOLE_0:def 5;
reconsider x1 as Subset of uG by A65,A71;
x1 meets c by A80,A79,A14,A77,XBOOLE_0:3;
then x1 = c by A81,A1,EQREL_1:def 4;
hence thesis by A5,A65,A71,XBOOLE_0:def 5;
end;
end;
x2 c= x1 proof
let x be object;
assume A82: x in x2;
then A83: x in s.x2 by A75,XBOOLE_0:def 3;
per cases by A83,A73,A74,XBOOLE_0:def 3;
suppose x in x1;
hence thesis;
end;
suppose A84: x in r"{x1};
A85: r"{x1} c= dom r by RELAT_1:132;
A86: x2 in C by A65,A72,XBOOLE_0:def 5;
reconsider x2 as Subset of uG by A65,A72;
x2 meets c by A85,A84,A14,A82,XBOOLE_0:3;
then x2 = c by A86,A1,EQREL_1:def 4;
hence thesis by A5,A65,A72,XBOOLE_0:def 5;
end;
end;
hence thesis by A76,XBOOLE_0:def 10;
end;
D c= rng s proof
let x be object;
assume x in D;
then consider d being Element of Cc such that
A87: x = d \/ r"{d};
s.d = d \/ r"{d} by A66;
hence x in rng s by A87,A65,FUNCT_1:def 3;
end;
then D = rng s by A67;
then s is onto by FUNCT_2:def 3;
then A88: card Cc = card D by A70,A17,EULER_1:11;
then D is finite;
hence contradiction by A64,A88,A2,Def22;
end;
end;
definition
let G be SimpleGraph;
attr G is with_finite_stability# means :Def23:
ex A being finite StableSet of G
st for B being finite StableSet of G holds card B <= card A;
end;
registration
cluster finite -> with_finite_stability# for SimpleGraph;
correctness proof
let R be SimpleGraph;
assume R is finite;
then reconsider R9 = R as finite SimpleGraph;
reconsider VR = Vertices R9 as finite set;
defpred P[Nat] means
ex A being finite StableSet of R9 st card A = $1;
A1: for k being Nat st P[k] holds k <= card VR by NAT_1:43;
{}VR is StableSet of R & card {} = 0;
then A2: ex k being Nat st P[k];
consider k being Nat such that
A3: P[k] and
A4: for n being Nat st P[n] holds n <= k from NAT_1:sch 6(A1, A2);
consider S being finite StableSet of R such that
A5: card S = k by A3;
take S;
let T be finite StableSet of R;
thus card T <= card S by A5,A4;
end;
end;
registration
let G be with_finite_stability# SimpleGraph;
cluster -> finite for StableSet of G;
correctness proof
consider A being finite StableSet of G such that
A1: for B being finite StableSet of G holds card(A) >= card(B) by Def23;
given B being StableSet of G such that
A2: B is infinite;
consider C being finite Subset of B such that
A3: card C > card A by A2,DILWORTH:5;
C is StableSet of G by Th64;
hence contradiction by A1,A3;
end;
end;
registration
cluster with_finite_stability# non void for SimpleGraph;
existence proof
reconsider G = { {}, {{}} } as SimpleGraph by Th25;
set A = union G;
A = {{}} by Th8;
then G is non void;
hence thesis;
end;
end;
definition
let G be with_finite_stability# SimpleGraph;
func stability# G -> Nat means :Def24:
(ex A being finite StableSet of G st card(A) = it)
& for T being finite StableSet of G holds card T <= it;
existence proof
consider A being finite StableSet of G such that
A1: for B being finite StableSet of G holds card(A) >= card(B) by Def23;
take itt = card A;
thus ex A being finite StableSet of G st card A = itt;
let T being finite StableSet of G;
thus card(T) <= itt by A1;
end;
uniqueness proof
let it1, it2 be Nat such that
A2: ex S1 being finite StableSet of G st card S1 = it1 and
A3: for T being finite StableSet of G holds card(T) <= it1 and
A4: ex S2 being finite StableSet of G st card S2 = it2 and
A5: for T being finite StableSet of G holds card(T) <= it2;
consider S1 being finite StableSet of G such that
A6: card S1 = it1 by A2;
consider S2 being finite StableSet of G such that
A7: card S2 = it2 by A4;
it1 <= it2 & it2 <= it1 by A3,A5,A6,A7;
hence it1 = it2 by XXREAL_0:1;
end;
end;
registration
let G be with_finite_stability# non void SimpleGraph;
cluster stability# G -> positive;
correctness proof
Vertices G <> {} by Th28;
then consider v being object such that
A1: v in Vertices G by XBOOLE_0:def 1;
reconsider S = {v} as finite Subset of Vertices G by A1,ZFMISC_1:31;
card S <= stability# G by Def24;
hence thesis;
end;
end;
theorem Th71: :: Width4:
for G being with_finite_stability# SimpleGraph
st stability# G = 1 holds G is clique
proof
let R be with_finite_stability# SimpleGraph;
assume A1: stability# R = 1;
set cR = Vertices R;
now
let a, b be set such that
A2: a <> b and
A3: a in cR & b in cR;
assume {a, b} nin Edges R;
then {a,b} nin R by A2,Th12;
then A4: {a,b} is StableSet of R by A3,Th62;
card {a,b} = 2 by A2,CARD_2:57;
hence contradiction by A1,A4,Def24;
end;
hence R is clique by Th47;
end;
registration :: see analoguous in DILWORTH
:: I have done it through Ramsey. How else to prove it?
:: For posets one gets it directly from Dilworth.
cluster with_finite_clique# with_finite_stability# -> finite for SimpleGraph;
correctness proof
let R be SimpleGraph;
assume A1: R is with_finite_clique#;
assume A2: R is with_finite_stability#;
assume A3: R is infinite;
set VR = Vertices R;
A4: Vertices R is infinite by A3,Th23;
A5: R c= R;
reconsider R as with_finite_clique# with_finite_stability# SimpleGraph
by A1,A2;
consider C being finite Clique of R such that
A6: order C = clique# R by Def15;
reconsider VC = Vertices C as finite Subset of VR by ZFMISC_1:77;
consider An being finite StableSet of R such that
A7: card(An) = stability# R by Def24;
reconsider VAn = An as finite Subset of VR;
set h = clique# R, w = stability# R;
A8: 0+1 <= h by A4,Th54,NAT_1:14;
R is non void by A3; then
A9: 0+1 <= w by NAT_1:13;
per cases by A8,A9,XXREAL_0:1;
suppose h = 1;
then A10: VR is StableSet of R by Th63;
consider Y being finite Subset of VR such that
A11: card Y > w by A4,DILWORTH:5;
Y is StableSet of R by A10,Th64;
hence thesis by A11,Def24;
end;
suppose w = 1;
then A12: R is Clique of R by A5,Th71;
consider Y being finite Subset of VR such that
A13: card Y > h by A4,DILWORTH:5;
A14: (R SubgraphInducedBy Y) is Clique of R by A12,Th66;
order (R SubgraphInducedBy Y) = card Y by Lm9;
hence thesis by A13,A14,Def15;
end;
suppose A15: h > 1 & w > 1;
set m = max(clique# R, stability# R) +1;
reconsider m as Nat;
consider r being Nat such that
A16: for X being finite set, P being a_partition of the_subsets_of_card(2,X)
st card X >= r & card P = 2 holds
ex S being Subset of X st card S >= m & S is_homogeneous_for P
by RAMSEY_1:17;
consider Y being finite Subset of VR such that
A17: card Y > r by A4,DILWORTH:5;
set X = Y \/ VAn \/ VC;
reconsider X as finite Subset of VR;
Y c= Y \/ An & Y \/ An c= Y \/ An \/ VC by XBOOLE_1:7;
then
A18: card Y <= card X by NAT_1:43,XBOOLE_1:1;
set A = { {x,y} where x,y is Element of VR :
x<>y & x in X & y in X & {x, y} in Edges R };
set B = { {x,y} where x,y is Element of VR :
x<>y & x in X & y in X & {x, y} nin Edges R };
set E = the_subsets_of_card(2,X); set P = { A, B };
A19: A c= E proof
let x be object;
reconsider x1 = x as set by TARSKI:1;
assume x in A;
then consider xx, yy being Element of VR such that
A20: {xx,yy} = x and
A21: xx<>yy and
A22: xx in X and
A23: yy in X and {xx,yy} in Edges R;
x is Subset of X & card x1 = 2
by A20,A21,A22,A23,CARD_2:57,ZFMISC_1:32;
hence thesis;
end;
A24: B c= E proof
let x be object;
reconsider x1 = x as set by TARSKI:1;
assume x in B;
then consider xx, yy being Element of VR such that
A25: {xx,yy} = x and
A26: xx<>yy and
A27: xx in X and
A28: yy in X and {xx,yy} nin Edges R;
x is Subset of X & card x1 = 2
by A25,A26,A27,A28,CARD_2:57,ZFMISC_1:32;
hence thesis;
end;
A29: A in P & B in P by TARSKI:def 2;
A30: now
assume A31: A = B;
consider a, b being set such that
A32: a in An and
A33: b in An and
A34: a <> b by A15,A7,NAT_1:59;
reconsider a, b as Element of VR by A32,A33;
A35: {a, b} nin Edges R by A32,A33,A34,Def19;
a in Y \/ An & b in Y \/ An by A32,A33,XBOOLE_0:def 3;
then a in X & b in X by XBOOLE_0:def 3;
then {a,b} in B by A35,A34;
then consider aa, bb being Element of VR such that
A36: {a,b} = {aa, bb} and
aa <> bb & aa in X & bb in X and
A37: {aa, bb} in Edges R by A31;
thus contradiction by A37,A32,A33,A34,Def19,A36;
end;
A38: P c= bool E proof
let x be object;
reconsider x1 = x as set by TARSKI:1;
assume x in P;
then x1 c= E by A19,A24,TARSKI:def 2;
hence thesis;
end;
A39: union P = E proof
thus union P c= E proof
let x be object;
assume x in union P;
then consider Y being set such that
A40: x in Y and
A41: Y in P by TARSKI:def 4;
Y = A or Y = B by A41,TARSKI:def 2;
hence thesis by A40,A19,A24;
end;
thus E c= union P proof
let x be object;
assume x in E;
then consider xx being Subset of X such that
A42: x = xx and
A43: card xx = 2;
consider a, b being object such that
A44: a <> b and
A45: xx = {a,b} by A43,CARD_2:60;
a in xx & b in xx by A45,TARSKI:def 2;
then a in X & b in X;
then reconsider a, b as Element of VR;
A46: a in xx & b in xx by A45,TARSKI:def 2;
{a,b} in Edges R or {a,b} nin Edges R;
then {a,b} in A or {a,b} in B by A46,A44;
hence x in union P by A42,A45,A29,TARSKI:def 4;
end;
end;
for a being Subset of E st a in P holds a<>{} &
for b being Subset of E st b in P holds a = b or a misses b proof
let a be Subset of E such that
A47: a in P;
thus a<>{} proof
per cases by A47,TARSKI:def 2;
suppose A48: a = A;
consider aa, bb being set such that
A49: aa in VC and
A50: bb in VC and
A51: aa <> bb by A15,A6,NAT_1:59;
reconsider aa, bb as Element of VR by A49,A50;
{aa, bb} in C by A49,A50,Th53;
then A52: {aa, bb} in Edges R by A51,Th12;
aa in Y \/ An \/ VC & bb in Y \/ An \/ VC by A49,A50,XBOOLE_0:def 3;
then {aa,bb} in A by A51,A52;
hence thesis by A48;
end;
suppose A53: a = B;
consider aa, bb being set such that
A54: aa in An and
A55: bb in An and
A56: aa <> bb by A15,A7,NAT_1:59;
reconsider aa, bb as Element of VR by A54,A55;
A57: {aa,bb} nin Edges R by A54,A55,A56,Def19;
aa in Y \/ An & bb in Y \/ An by A54,A55,XBOOLE_0:def 3;
then aa in X & bb in X by XBOOLE_0:def 3;
then {aa,bb} in B by A56,A57;
hence thesis by A53;
end;
end;
let b be Subset of E such that
A58: b in P;
assume A59: a <> b;
assume A60: a meets b;
(a = A or a = B) & (b = A or b = B) by A47,A58,TARSKI:def 2;
then A /\ B <> {} by A59,A60;
then consider x being object such that
A61: x in A /\ B by XBOOLE_0:def 1;
x in A by A61,XBOOLE_0:def 4;
then consider xx, yy being Element of VR such that
A62: {xx,yy} = x and xx<>yy & xx in X & yy in X and
A63: {xx, yy} in Edges R;
x in B by A61,XBOOLE_0:def 4;
then consider x2, y2 being Element of VR such that
A64: {x2,y2} = x and x2<>y2 & x2 in X & y2 in X and
A65: {x2, y2} nin Edges R;
thus contradiction by A63,A65,A62,A64;
end;
then reconsider P as a_partition of E by A39,A38,EQREL_1:def 4;
card P = 2 by A30,CARD_2:57;
then consider S being Subset of X such that
A66: card S >= m and
A67: S is_homogeneous_for P by A18,A16,A17,XXREAL_0:2;
reconsider S as finite Subset of VR by XBOOLE_1:1;
max(clique# R, stability# R) >= clique# R by XXREAL_0:25;
then m > clique# R by NAT_1:13;
then
A68: card S > clique# R by A66,XXREAL_0:2;
max(clique# R, stability# R) >= stability# R by XXREAL_0:25;
then m > stability# R by NAT_1:13;
then
A69: card S > stability# R by A66,XXREAL_0:2;
consider p being Element of P such that
A70: the_subsets_of_card(2,S) c= p by A67,RAMSEY_1:def 1;
per cases by TARSKI:def 2;
suppose A71: p = A;
set H = R SubgraphInducedBy S;
A72: Vertices H = S by Lm9;
now
let x, y be set such that
A73: x <> y and
A74: x in union H and
A75: y in union H;
{x,y} is Subset of S & card {x,y} = 2
by A72,A74,A75,A73,CARD_2:57,ZFMISC_1:32;
then {x,y} in the_subsets_of_card(2,S);
then {x,y} in A by A71,A70;
then consider xx, yy being Element of VR such that
A76: {xx,yy} = {x,y} and xx<>yy & xx in X & yy in X and
A77: {xx, yy} in Edges R;
{x, y} in H by A77,A74,A75,A72,Lm10,A76;
hence {x, y} in Edges H by A73,Th12;
end;
then H is finite Clique of R by Th47;
then order H <= clique# R by Def15;
hence contradiction by A68,Lm9;
end;
suppose A78: p = B;
now
let x, y be set such that
A79: x <> y and
A80: x in S and
A81: y in S;
{x,y} is Subset of S & card {x,y} = 2
by A80,A81,A79,CARD_2:57,ZFMISC_1:32;
then {x,y} in the_subsets_of_card(2,S);
then {x,y} in B by A78,A70;
then consider xx, yy being Element of VR such that
A82: {xx,yy} = {x,y} and xx<>yy & xx in X & yy in X and
A83: {xx, yy} nin Edges R;
thus {x,y} nin R by A79,A83,Th12,A82;
end;
then S is stable;
hence contradiction by A69,Def24;
end;
end;
end;
end;
theorem Th72:
for G being SimpleGraph, C being Clique of G
holds Vertices C is StableSet of Complement G
proof
let G be SimpleGraph, C be Clique of G; set CG = Complement G;
A1: Vertices G = Vertices CG by Lm4;
reconsider uC = union C as Subset of Vertices CG by A1,ZFMISC_1:77;
now
let x, y be set such that
A2: x <> y and
A3: x in uC and
A4: y in uC;
{x,y} in C by A3,A4,Th53;
then {x,y} in Edges G by A2,Th12;
hence {x,y} nin CG by XBOOLE_0:def 5;
end;
hence union C is StableSet of Complement G by Def19;
end;
theorem Th73:
for G being SimpleGraph, C being Clique of Complement G
holds Vertices C is StableSet of G
proof
let G be SimpleGraph, C be Clique of Complement G;
Vertices C is StableSet of Complement Complement G by Th72;
hence Vertices C is StableSet of G;
end;
theorem Th74:
for G being SimpleGraph, C being StableSet of G
holds (Complement G) SubgraphInducedBy C is Clique of Complement G
proof
let G be SimpleGraph, C be StableSet of G; set CG = Complement G;
set CGSC = CG SubgraphInducedBy C; set uCGSC = union CGSC;
now let a, b be set such that
A1: a <> b and
A2: a in uCGSC and
A3: b in uCGSC;
A4: a in C & b in C by A2,A3,Lm7;
A5: {a,b} nin Edges G by A4,A1,Def19;
A6: {a,b} in CompleteSGraph Vertices G by A4,Th34;
{a,b} in CG by A5,A6,XBOOLE_0:def 5;
then {a, b} in CGSC by A4,Lm10;
hence {a, b} in Edges CGSC by A1,Th12;
end;
hence CGSC is Clique of Complement G by Th47;
end;
theorem Th75:
for G being SimpleGraph, C being StableSet of Complement G
holds G SubgraphInducedBy C is Clique of G
proof
let G be SimpleGraph, C be StableSet of Complement G;
(Complement Complement G) SubgraphInducedBy C
is Clique of Complement Complement G by Th74;
hence G SubgraphInducedBy C is Clique of G;
end;
registration
let G be with_finite_clique# SimpleGraph;
cluster Complement G -> with_finite_stability#;
correctness proof
set CG = Complement G;
consider A being finite Clique of G such that
A1: for B being finite Clique of G holds order B <= order A by Def14;
A2: Vertices G = Vertices CG by Lm4;
set C = union A;
reconsider C as finite StableSet of CG by Th72;
take C;
let D be finite StableSet of CG;
A3: G SubgraphInducedBy D is finite Clique of G by Th75;
order (G SubgraphInducedBy D) <= order A by A3,A1;
hence card D <= card C by A2,Lm9;
end;
end;
registration
let G be with_finite_stability# SimpleGraph;
cluster Complement G -> with_finite_clique#;
correctness proof
set CG = Complement G;
consider A being finite StableSet of G such that
A1: for B being finite StableSet of G holds card B <= card A by Def23;
A2: Vertices G = Vertices CG by Lm4;
set C = CG SubgraphInducedBy A;
reconsider C as finite Clique of CG by Th74;
take C;
let D be finite Clique of CG;
A3: union D is StableSet of G by Th73;
A = union C by A2,Lm9;
hence order D <= order C by A1,A3;
end;
end;
theorem Th76:
for G being with_finite_clique# SimpleGraph
holds clique# G = stability# Complement G
proof
let G be with_finite_clique# SimpleGraph;
set CG = Complement G; set sCG = stability# Complement G, cG = clique# G;
consider C being finite Clique of G such that
A1: order C = cG by Def15;
A2: Vertices G = Vertices CG by Lm4;
reconsider A = union C as StableSet of CG by Th72;
A3: card A = cG by A1;
now let T be finite StableSet of CG;
G SubgraphInducedBy T is Clique of G by Th75;
then order (G SubgraphInducedBy T) <= cG by Def15;
hence card T <= cG by A2,Lm9;
end;
hence cG = sCG by A3,Def24;
end;
theorem :: staRcliCR:
for G being with_finite_stability# SimpleGraph
holds stability# G = clique# Complement G
proof
let G be with_finite_stability# SimpleGraph;
Complement Complement G = G;
hence thesis by Th76;
end;
theorem Th78:
for G being SimpleGraph, C being Clique-partition of Complement G
holds C is Coloring of G
proof
let G be SimpleGraph, C be Clique-partition of Complement G;
set CG = Complement G;
now
let x be set;
assume A1: x in C;
then A2: (Complement G) SubgraphInducedBy x is Clique of CG by Def16;
union ((Complement G) SubgraphInducedBy x) = x by A1,Lm9;
hence x is StableSet of G by A2,Th73;
end;
hence C is Coloring of G by Lm4,Def20;
end;
theorem Th79:
for G being SimpleGraph, C being Clique-partition of G
holds C is Coloring of Complement G
proof
let G be SimpleGraph, C being Clique-partition of G;
Complement Complement G = G;
hence thesis by Th78;
end;
theorem Th80:
for G being SimpleGraph, C being Coloring of G
holds C is Clique-partition of Complement G
proof
let G be SimpleGraph, C be Coloring of G;
set CG = Complement G;
now
let x be set;
assume x in C;
then x is StableSet of G by Def20;
hence CG SubgraphInducedBy x is Clique of CG by Th74;
end;
hence C is Clique-partition of CG by Lm4,Def16;
end;
theorem :: ChrComplClico:
for G being SimpleGraph, C being Coloring of Complement G
holds C is Clique-partition of G
proof
let G be SimpleGraph, C being Coloring of Complement G;
Complement Complement G = G;
hence thesis by Th80;
end;
registration
let G be finitely_colorable SimpleGraph;
cluster Complement G -> with_finite_cliquecover#;
correctness proof
consider C being Coloring of G such that
A1: C is finite by Def21;
C is Clique-partition of Complement G by Th80;
hence thesis by A1;
end;
end;
registration
let G be with_finite_cliquecover# SimpleGraph;
cluster Complement G -> finitely_colorable;
correctness proof
consider C being Clique-partition of G such that
A1: C is finite by Def17;
C is Coloring of Complement G by Th79;
hence thesis by A1;
end;
end;
theorem Th82:
for G being finitely_colorable SimpleGraph
holds chromatic# G = cliquecover# Complement G
proof
let G be finitely_colorable SimpleGraph;
set CG = Complement G; set k = cliquecover# CG;
consider C being finite Clique-partition of CG such that
A1: card C = k by Def18;
A2: C is Coloring of G by Th78;
now
let C be finite Coloring of G;
assume A3: k > card C;
C is Clique-partition of CG by Th80;
hence contradiction by A3,Def18;
end;
hence chromatic# G = cliquecover# Complement G by A2,A1,Def22;
end;
theorem :: covRchrCR:
for G being with_finite_cliquecover# SimpleGraph
holds cliquecover# G = chromatic# Complement G
proof
let G be with_finite_cliquecover# SimpleGraph;
Complement Complement G = G;
hence thesis by Th82;
end;
begin :: Mycielskian of a graph
definition
let G be SimpleGraph;
func Mycielskian G -> SimpleGraph equals
{ {} } \/
(the set of all {x}
where x is Element of (union G) \/ [:union G,{union G}:] \/ {union G})
\/
(Edges G) \/
{ {x,[y,union G]} where x, y is Element of union G : {x,y} in Edges G } \/
{ {union G,[x,union G]} where x is Element of union G : x in Vertices G };
correctness proof
set uG = union G;
set C = the set of all {x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG};
set A = { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set B = { {uG,[x,uG]} where x is Element of uG : x in Vertices G };
set M = { {} } \/ C \/ (Edges G) \/ A \/ B;
reconsider N = M as non empty set;
A1: M is subset-closed proof
let a,b be set such that
A2: a in M and
A3: b c= a;
A4: {} in {{}} by TARSKI:def 1; then
A5: {} in M by MYCIELSK:4;
per cases by A2,MYCIELSK:4;
suppose a in { {} };
then a = {} by TARSKI:def 1;
hence b in M by A3,A5;
end;
suppose a in C;
then consider x being Element of (uG) \/ [:uG,{uG}:] \/ {uG} such that
A6: a = {x};
thus b in M by A5,A6,A2,A3,ZFMISC_1:33;
end;
suppose a in Edges G;
then consider x, y being set such that x <> y and
A7: x in Vertices G and
A8: y in Vertices G and
A9: a = {x, y} by Th11;
A10: b = {} or b = {x} or b = {y} or b = {x,y} by A9,A3,ZFMISC_1:36;
x in (uG) \/ [:uG,{uG}:] & y in (uG) \/ [:uG,{uG}:]
by A7,A8,XBOOLE_0:def 3;
then x in (uG) \/ [:uG,{uG}:] \/ {uG} & y in (uG) \/ [:uG,{uG}:] \/ {uG}
by XBOOLE_0:def 3;
then {x} in C & {y} in C;
hence b in M by A10,A4,A9,A2,MYCIELSK:4;
end;
suppose a in A;
then consider x, y being Element of uG such that
A11: a = {x,[y,uG]} and
A12: {x,y} in Edges G;
A13: x in uG by A12,Th13;
A14: b = {} or b = {x} or b = {[y,uG]} or b = {x,[y,uG]}
by A11,A3,ZFMISC_1:36;
x in (uG) \/ [:uG,{uG}:] by A13,XBOOLE_0:def 3;
then x in (uG) \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then A15: {x} in C;
y in uG & uG in {uG} by A12,Th13,TARSKI:def 1;
then [y,uG] in [:uG,{uG}:] by ZFMISC_1:def 2;
then [y,uG] in uG \/ [:uG,{uG}:] by XBOOLE_0:def 3;
then [y,uG] in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then {[y,uG]} in C;
hence b in M by A11,A2,A14,A4,A15,MYCIELSK:4;
end;
suppose a in B;
then consider x being Element of uG such that
A16: a = {uG,[x,uG]} and
A17: x in Vertices G;
A18: b = {} or b = {uG} or b = {[x,uG]} or b = {uG,[x,uG]}
by A16,A3,ZFMISC_1:36;
uG in {uG} by TARSKI:def 1;
then uG in (uG) \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then A19: {uG} in C;
x in uG & uG in {uG} by A17,TARSKI:def 1;
then [x,uG] in [:uG,{uG}:] by ZFMISC_1:def 2;
then [x,uG] in uG \/ [:uG,{uG}:] by XBOOLE_0:def 3;
then [x,uG] in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then {[x,uG]} in C;
hence b in M by A16,A2,A18,A4,A19,MYCIELSK:4;
end;
end;
A20: N is 1-at_most_dimensional proof
let a be set;
assume A21: a in N;
per cases by A21,MYCIELSK:4;
suppose a in { {} };
then a = {} by TARSKI:def 1;
hence card a c= 1+1;
end;
suppose a in C;
then consider x being Element of (uG) \/ [:uG,{uG}:] \/ {uG} such that
A22: a = {x};
A23: card a = 1 by A22,CARD_1:30;
Segm 1 c= Segm(1+1) by NAT_1:39;
hence card a c= 1+1 by A23;
end;
suppose a in Edges G;
hence card a c= 1+1 by Def4;
end;
suppose a in A;
then consider x, y being Element of uG such that
A24: a = {x,[y,uG]} and {x,y} in Edges G;
card {x,[y,uG]} <= 2 by CARD_2:50;
then Segm card {x,[y,uG]} c= Segm(1+1) by NAT_1:39;
hence card a c= 1+1 by A24;
end;
suppose a in B;
then consider x being Element of uG such that
A25: a = {uG,[x,uG]} and x in Vertices G;
card {uG,[x,uG]} <= 2 by CARD_2:50;
then Segm card {uG,[x,uG]} c= Segm 2 by NAT_1:39;
hence card a c= 1+1 by A25;
end;
end;
thus M is SimpleGraph by A1,A20;
end;
end;
theorem Th84: :: Mycielskian0:
for G being SimpleGraph holds G c= Mycielskian G
proof
let G be SimpleGraph;
set MG = Mycielskian G; set uG = union G;
let x be object;
assume x in G;
then x in { {} } \/ singletons uG \/ Edges G by Th27;
then A1: x in { {} } \/ singletons uG or x in Edges G by XBOOLE_0:def 3;
per cases by A1,XBOOLE_0:def 3;
suppose x in { {} };
then x = {} by TARSKI:def 1;
hence x in MG by Th20;
end;
suppose x in singletons uG;
then consider f being Subset of uG such that
A2: x = f and
A3: f is 1-element;
consider a being set such that
A4: a in uG and
A5: f = {a} by A3,Th9;
a in uG \/ [:uG,{uG}:] by A4,XBOOLE_0:def 3;
then a in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then x in the set of all
{xx} where xx is Element of uG \/ [:uG,{uG}:] \/ {uG}
by A2,A5;
hence x in MG by MYCIELSK:4;
end;
suppose A6: x in Edges G;
Edges G c= MG by MYCIELSK:3;
hence x in MG by A6;
end;
end;
theorem Th85:
for G being SimpleGraph, v being set
holds v in Vertices Mycielskian G
iff v in union G or (ex x being set st x in union G & v = [x,union G])
or v = union G
proof
let G be SimpleGraph, v be set;
set uG = union G; set MG = Mycielskian G; set uMG = union MG;
hereby
assume v in Vertices MG;
then consider g being set such that
A1: v in g and
A2: g in MG by TARSKI:def 4;
defpred Thesis[] means
v in union G or (ex x being set st x in union G & v = [x,union G])
or v = union G;
per cases by A2,MYCIELSK:4;
suppose g in { {} };
hence Thesis[] by A1,TARSKI:def 1;
end;
suppose g in the set of all
{x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG};
then consider h being Element of uG \/ [:uG,{uG}:] \/ {uG} such that
A3: g = {h};
A4: h in uG \/ [:uG,{uG}:] or h in {uG} by XBOOLE_0:def 3;
A5: v = h by A3,A1,TARSKI:def 1;
per cases by A4,XBOOLE_0:def 3;
suppose h in uG;
hence Thesis[] by A3,A1,TARSKI:def 1;
end;
suppose h in [:uG,{uG}:];
then consider h1, h2 being object such that
A6: h1 in uG and
A7: h2 in {uG} and
A8: h = [h1,h2] by ZFMISC_1:def 2;
h2 = uG by A7,TARSKI:def 1;
hence Thesis[] by A5,A8,A6;
end;
suppose h in {uG};
hence Thesis[] by A5,TARSKI:def 1;
end;
end;
suppose g in Edges G;
then consider g1, g2 being set such that g1 <> g2 and
A9: g1 in Vertices G and
A10: g2 in Vertices G and
A11: g = {g1, g2} by Th11;
thus Thesis[] by A9,A10,A1,A11,TARSKI:def 2;
end;
suppose g in { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
then consider g1, g2 being Element of uG such that
A12: g = {g1,[g2,uG]} and
A13: {g1,g2} in Edges G;
A14: g1 in uG & g2 in uG by A13,Th13;
v = g1 or v = [g2,uG] by A12,A1,TARSKI:def 2;
hence Thesis[] by A14;
end;
suppose g in { {uG,[x,uG]} where x is Element of uG : x in Vertices G };
then consider x being Element of uG such that
A15: g = {uG,[x,uG]} and
A16: x in uG;
v = uG or v = [x,uG] by A1,A15,TARSKI:def 2;
hence Thesis[] by A16;
end;
end;
assume A17: v in union G or (ex x being set st x in union G & v = [x,union G])
or v = union G;
A18: for a being set st a in uG \/ [:uG,{uG}:] \/ {uG} holds a in uMG
proof
let a be set;
assume a in uG \/ [:uG,{uG}:] \/ {uG};
then A19: {a} in the set of all
{x} where x is Element of uG \/ [:uG,{uG}:] \/ {uG};
A20: the set of all {x} where x is Element of uG \/ [:uG,{uG}:] \/ {uG}
c= MG by MYCIELSK:3;
a in {a} by TARSKI:def 1;
hence a in uMG by A20,A19,TARSKI:def 4;
end;
per cases by A17;
suppose v in union G;
then v in uG \/ [:uG,{uG}:] by XBOOLE_0:def 3;
then v in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
hence thesis by A18;
end;
suppose (ex x being set st x in union G & v = [x,union G]);
then consider x being set such that
A21: x in union G and
A22: v = [x,union G];
union G in {union G} by TARSKI:def 1;
then v in [:uG,{uG}:] by A21,A22,ZFMISC_1:def 2;
then v in uG \/ [:uG,{uG}:] by XBOOLE_0:def 3;
then v in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
hence thesis by A18;
end;
suppose v = union G; then
v in {uG} by TARSKI:def 1;
then v in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
hence thesis by A18;
end;
end;
theorem Th86:
for G being SimpleGraph
holds Vertices Mycielskian G = union G \/ [:union G,{union G}:] \/ {union G}
proof
let G be SimpleGraph;
set uG = union G; set MG = Mycielskian G; set uMG = union MG;
A1: uG in {uG} by TARSKI:def 1;
thus uMG c= uG \/ [:uG,{uG}:] \/ {uG} proof
let v be object;
assume A2: v in uMG;
per cases by A2,Th85;
suppose v in uG;
then v in uG \/ ([:uG,{uG}:] \/ {uG}) by XBOOLE_0:def 3;
hence v in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_1:4;
end;
suppose ex x being set st x in uG & v = [x,uG];
then consider x being set such that
A3: x in uG and
A4: v = [x,uG];
v in [:uG,{uG}:] by A1,A3,A4,ZFMISC_1:def 2;
then v in uG \/ [:uG,{uG}:] by XBOOLE_0:def 3;
hence v in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
end;
suppose v = union G; then
v in {uG} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus uG \/ [:uG,{uG}:] \/ {uG} c= uMG proof
let v be object;
assume v in uG \/ [:uG,{uG}:] \/ {uG};
then A5: v in uG \/ [:uG,{uG}:] or v in {uG} by XBOOLE_0:def 3;
per cases by A5,XBOOLE_0:def 3;
suppose v in uG;
hence thesis by Th85;
end;
suppose v in [:uG,{uG}:];
then consider x, y being object such that
A6: x in uG and
A7: y in {uG} and
A8: v = [x,y] by ZFMISC_1:def 2;
y = uG by A7,TARSKI:def 1;
hence thesis by A6,A8,Th85;
end;
suppose v in {uG};
then v = uG by TARSKI:def 1;
hence thesis by Th85;
end;
end;
end;
theorem Th87:
for G being SimpleGraph holds union G in union Mycielskian G
proof
let G be SimpleGraph;
union G in {union G} by TARSKI:def 1;
then union G in (union G) \/ [:union G,{union G}:] \/ {union G}
by XBOOLE_0:def 3;
hence union G in union Mycielskian G by Th86;
end;
theorem Th88:
for G being void SimpleGraph holds Mycielskian G = {{},{union G}}
proof
let G be void SimpleGraph;
set uG = union G;
A1: { {uG,[x,uG]} where x is Element of uG : x in Vertices G } = {} proof
assume not thesis;
then consider e being object such that
A2: e in { {uG,[x,uG]} where x is Element of uG : x in Vertices G }
by XBOOLE_0:def 1;
consider x being Element of uG such that e = {uG,[x,uG]} and
A3: x in Vertices G by A2;
thus thesis by A3;
end;
A4: { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G } = {} proof
assume not thesis;
then consider e being object such that
A5: e in { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G }
by XBOOLE_0:def 1;
consider x, y being Element of uG such that e = {x,[y,uG]} and
A6: {x,y} in Edges G by A5;
thus thesis by A6,Th13;
end;
A7: Edges G = {} proof
assume not thesis;
then consider e being object such that
A8: e in Edges G by XBOOLE_0:def 1;
consider x, y being set such that x <> y and
A9: x in Vertices G and y in Vertices G & e = {x, y} by A8,Th11;
thus contradiction by A9;
end;
A10: the set of all {x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG}
= {{uG}} proof
thus the set of all {x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG}
c= {{uG}} proof
let a be object;
assume a in the set of all
{x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG};
then consider x being Element of (uG) \/ [:uG,{uG}:] \/ {uG} such that
A11: a = {x};
x = uG by TARSKI:def 1;
hence a in {{uG}} by A11,TARSKI:def 1;
end;
thus {{uG}} c= the set of all
{x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG}
proof
let a be object;
assume a in {{uG}};
then A12: a = {uG} by TARSKI:def 1;
uG in (uG) \/ [:uG,{uG}:] \/ {uG} by TARSKI:def 1;
hence thesis by A12;
end;
end;
thus Mycielskian G = {{},{uG}} by A1,A4,A7,A10,ENUMSET1:1;
end;
registration
let G be finite SimpleGraph;
cluster Mycielskian G -> finite;
correctness proof
set uG = union G; set MG = Mycielskian G;
set C = the set of all {x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG};
set A = { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set B = { {uG,[x,uG]} where x is Element of uG : x in Vertices G };
per cases;
suppose G is void;
then MG = {{},{union G}} by Th88;
hence thesis;
end;
suppose G is non void;
then reconsider uGf = uG as non empty set by Th28;
A1: uGf is finite;
deffunc FB(set) = {uG,[$1,uG]};
A2: { FB(x) where x is Element of uGf : x in uGf } is finite
from FRAENKEL:sch 21(A1);
A3: uG is finite;
deffunc FA(set,set) = {$1,[$2,uG]};
set AA = { FA(x,y) where x is Element of uGf, y is Element of uGf
: x in uG & y in uG };
A4: AA is finite from FRAENKEL:sch 22(A3, A3);
A5: A c= AA proof
let a be object;
assume a in A;
then consider x, y being Element of uG such that
A6: a = {x,[y,uG]} and {x,y} in Edges G;
thus a in AA by A6;
end;
deffunc FC(set) = {$1};
defpred P[set] means not contradiction;
{ FC(x) where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG} : P[x] } is finite
from PRE_CIRC:sch 1;
hence MG is finite by A2,A4,A5;
end;
end;
end;
theorem Th89:
for G being finite SimpleGraph holds order Mycielskian G = 2*(order G) + 1
proof
let G be finite SimpleGraph;
set uG = union G; set MG = Mycielskian G;
A1: card [:uG,{uG}:] = order G by CARD_1:69;
A2: uG misses [:uG,{uG}:] proof
assume uG meets [:uG,{uG}:];
then consider a being object such that
A3: a in uG and
A4: a in [:uG,{uG}:] by XBOOLE_0:3;
consider x,y being object such that x in uG and
A5: y in {uG} and
A6: a = [x,y] by A4,ZFMISC_1:def 2;
y = uG by A5,TARSKI:def 1;
hence contradiction by A6,A3,Th1;
end;
A7: now assume uG in (uG) \/ [:uG,{uG}:];
then uG in uG or uG in [:uG,{uG}:] by XBOOLE_0:def 3;
then consider x,y being object such that x in uG and
A8: y in {uG} and
A9: uG = [x,y] by ZFMISC_1:def 2;
y = uG by A8,TARSKI:def 1;
hence contradiction by A9,Th2;
end;
thus order MG = card ((uG) \/ [:uG,{uG}:] \/ {uG}) by Th86
.= card ((uG) \/ [:uG,{uG}:]) + 1 by A7,CARD_2:41
.= (card uG) + (card [:uG,{uG}:]) + 1 by A2,CARD_2:40
.= 2*(order G) + 1 by A1;
end;
theorem Th90:
for G being SimpleGraph, e being set
holds e in Edges Mycielskian G iff
e in Edges G or
(ex x, y being Element of union G st e = {x,[y,union G]} & {x,y} in Edges G)
or (ex y being Element of union G st e = {union G,[y,union G]} & y in union G)
proof
let G be SimpleGraph, e be set;
set uG = union G; set MG = Mycielskian G;
set C = the set of all {x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG};
set A = { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set B = { {uG,[x,uG]} where x is Element of uG : x in Vertices G };
hereby assume A1: e in Edges Mycielskian G;
then consider x, y being set such that
A2: x <> y and x in Vertices MG and y in Vertices MG and
A3: e = {x, y} by Th11;
per cases by A1,MYCIELSK:4;
suppose e in { {} };
hence e in Edges G
or (ex x, y being Element of uG st e = {x,[y,uG]} & {x,y} in Edges G)
or (ex y being Element of uG st e = {uG,[y,uG]} & y in uG)
by A3,TARSKI:def 1;
end;
suppose e in C;
then consider a being Element of (uG) \/ [:uG,{uG}:] \/ {uG} such that
A4: e = {a};
thus e in Edges G
or (ex x, y being Element of uG st e = {x,[y,uG]} & {x,y} in Edges G)
or (ex y being Element of uG st e = {uG,[y,uG]} & y in uG)
by A4,A3,A2,ZFMISC_1:5;
end;
suppose e in Edges G or e in A or e in B;
hence e in Edges G
or (ex x, y being Element of uG st e = {x,[y,uG]} & {x,y} in Edges G)
or (ex y being Element of uG st e = {uG,[y,uG]} & y in uG);
end;
end;
assume A5: e in Edges G
or (ex x, y being Element of uG st e = {x,[y,uG]} & {x,y} in Edges G)
or (ex y being Element of uG st e = {uG,[y,uG]} & y in uG);
per cases by A5;
suppose A6: e in Edges G;
A7: card e = 2 by A6,Def1;
e in MG by A6,MYCIELSK:4;
hence e in Edges Mycielskian G by A7,Def1;
end;
suppose ex x, y being Element of uG st e = {x,[y,uG]} & {x,y} in Edges G;
then consider x, y being Element of uG such that
A8: e = {x,[y,uG]} and
A9: {x,y} in Edges G;
A10: e in A by A8,A9;
A11: e in MG by A10,MYCIELSK:4;
y in uG by A9,Th13;
then x <> [y,uG] by Th1;
then card e = 2 by A8,CARD_2:57;
hence e in Edges Mycielskian G by A11,Def1;
end;
suppose ex y being Element of uG st e = {uG,[y,uG]} & y in uG;
then consider y being Element of uG such that
A12: e = {uG,[y,uG]} and
A13: y in uG;
A14: e in B by A12,A13;
A15: e in MG by A14,MYCIELSK:4;
card e = 2 by Th2,A12,CARD_2:57;
hence e in Edges Mycielskian G by A15,Def1;
end;
end;
theorem Th91:
for G being SimpleGraph
holds Edges Mycielskian G = (Edges G)
\/ { {x,[y,union G]} where x, y is Element of union G : {x,y} in Edges G }
\/ { {union G,[y,union G]} where y is Element of union G : y in union G }
proof
let G be SimpleGraph;
set uG = union G;
set A = { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set B = { {uG,[y,uG]} where y is Element of uG : y in uG };
thus Edges Mycielskian G c= (Edges G) \/ A \/ B
proof let e be object; assume
A1: e in Edges Mycielskian G;
per cases by A1,Th90;
suppose e in Edges G;
then e in (Edges G) \/ A by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex x, y being Element of union G
st e = {x,[y,union G]} & {x,y} in Edges G;
then e in A;
then e in (Edges G) \/ A by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
suppose ex y being Element of union G st e = {uG,[y,uG]} & y in uG;
then e in B;
hence thesis by XBOOLE_0:def 3;
end;
end;
thus (Edges G) \/ A \/ B c= Edges Mycielskian G proof
let e be object;
assume e in (Edges G) \/ A \/ B;
then A2: e in (Edges G) \/ A or e in B by XBOOLE_0:def 3;
per cases by A2,XBOOLE_0:def 3;
suppose e in Edges G;
hence thesis by Th90;
end;
suppose e in A;
then consider x, y being Element of uG such that
A3: e = {x,[y,uG]} & {x,y} in Edges G;
thus thesis by A3,Th90;
end;
suppose e in B;
then consider y being Element of uG such that
A4: e = {union G,[y,union G]} & y in uG;
thus thesis by A4,Th90;
end;
end;
end;
theorem Th92:
for G being finite SimpleGraph holds size Mycielskian G = 3*(size G) + order G
proof
let G be finite SimpleGraph;
set uG = union G; set MG = Mycielskian G;
set A = { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set B = { {uG,[y,uG]} where y is Element of uG : y in union G };
per cases;
suppose A1: G is void;
then A2: MG = {{},{uG}} by Th88;
A3: size G = 0 by A1,Th17,CARD_1:27;
size MG = 0 proof
assume not thesis;
then Edges MG <> {};
then consider e being object such that
A4: e in Edges MG by XBOOLE_0:def 1;
consider x, y being set such that
A5: x <> y and x in Vertices MG & y in Vertices MG and
A6: e = {x, y} by A4,Th11;
e = {} or e = {uG} by A2,A4,TARSKI:def 2;
hence thesis by A6,A5,ZFMISC_1:5;
end;
hence thesis by A1,A3;
end;
suppose G is non void;
then reconsider uGf = uG as non empty set by Th28;
A7: uGf is finite;
deffunc FB(set) = {uG,[$1,uG]};
{ FB(x) where x is Element of uGf : x in uGf } is finite
from FRAENKEL:sch 21(A7);
then reconsider B as finite set;
A8: uG is finite;
deffunc FA(set,set) = {$1,[$2,uG]};
set AA = { FA(x,y) where x is Element of uGf, y is Element of uGf
: x in uG & y in uG };
A9: AA is finite from FRAENKEL:sch 22(A8, A8);
A c= AA proof
let a be object;
assume a in A;
then consider x, y being Element of uG such that
A10: a = {x,[y,uG]} and {x,y} in Edges G;
thus a in AA by A10;
end;
then reconsider A as finite set by A9;
A11: card B = order G by Th10;
A12: card A = 2 * size G by Th15;
A13: now assume B meets (Edges G) \/ A;
then consider a being object such that
A14: a in B and
A15: a in (Edges G) \/ A by XBOOLE_0:3;
consider y being Element of uG such that
A16: a = {uG,[y,uG]} and y in union G by A14;
per cases by A15,XBOOLE_0:def 3;
suppose a in Edges G;
then consider xa, ya being set such that xa <> ya and
A17: xa in Vertices G and ya in Vertices G and
A18: a = {xa, ya} by Th11;
per cases by A16,A18,ZFMISC_1:6;
suppose xa = uG;
hence contradiction by A17;
end;
suppose xa = [y,uG];
hence contradiction by A17,Th1;
end;
end;
suppose a in A;
then consider xa, ya being Element of uG such that
A19: a = {xa,[ya,uG]} and
A20: {xa,ya} in Edges G;
A21: xa in uG by A20,Th13;
per cases by A16,A19,ZFMISC_1:6;
suppose xa = uG;
hence contradiction by A21;
end;
suppose xa = [y,uG];
hence contradiction by A21,Th1;
end;
end;
end;
A22: now assume A meets Edges G;
then consider a being object such that
A23: a in A and
A24: a in Edges G by XBOOLE_0:3;
consider xa, ya being Element of uG such that
A25: a = {xa,[ya,uG]} and {xa,ya} in Edges G by A23;
consider xe, ye being set such that xe <> ye and
A26: xe in Vertices G and
A27: ye in Vertices G and
A28: a = {xe, ye} by A24,Th11;
per cases by A25,A28,ZFMISC_1:6;
suppose xe = [ya,uG];
hence contradiction by A26,Th1;
end;
suppose ye = [ya,uG];
hence contradiction by A27,Th1;
end;
end;
thus size Mycielskian G = card ((Edges G) \/ A \/ B) by Th91
.= card ((Edges G) \/ A) + order G by A11,A13,CARD_2:40
.= card (Edges G) + 2*(size G) + order G by A12,A22,CARD_2:40
.= 3*(size G) + order G;
end;
end;
theorem Th93:
for G being SimpleGraph, s, t being object
st {s, t} in Edges Mycielskian G
holds {s, t} in Edges G or
(s in union G or s = union G)
& (ex y being object st y in union G & t = [y,union G]) or
(t in union G or t = union G)
& (ex y being object st y in union G & s = [y,union G])
proof
let G be SimpleGraph, s, t be object such that
A1: {s, t} in Edges Mycielskian G;
set uG = union G;
per cases by A1,Th90;
suppose {s, t} in Edges G;
hence thesis;
end;
suppose ex x, y being Element of uG
st {s,t} = {x,[y,uG]} & {x,y} in Edges G;
then consider x, y being Element of uG such that
A2: {s,t} = {x,[y,uG]} and
A3: {x,y} in Edges G;
A4: x in uG & y in uG by A3,Th13;
s = x & t = [y,uG] or t = x & s = [y,uG] by A2,ZFMISC_1:6;
hence thesis by A4;
end;
suppose ex y being Element of uG st {s,t} = {uG,[y,uG]} & y in uG;
then consider y being Element of uG such that
A5: {s,t} = {uG,[y,uG]} and
A6: y in uG;
s = uG & t = [y,uG] or t = uG & s = [y,uG] by A5,ZFMISC_1:6;
hence thesis by A6;
end;
end;
theorem Th94:
for G being SimpleGraph, u being object
st { union G, u } in Edges Mycielskian G
ex x being object st x in union G & u = [x, union G]
proof
let G be SimpleGraph, u be object such that
A1: { union G, u } in Edges Mycielskian G;
set uG = union G;
per cases by A1,Th93;
suppose {uG, u} in Edges G;
then uG in uG by Th13;
hence ex x being object st x in uG & u = [x, uG];
end;
suppose (uG in uG or uG = uG)
& (ex y being object st y in uG & u = [y,uG]);
hence ex x being object st x in uG & u = [x, union G];
end;
suppose (u in uG or u = uG)
& (ex y being object st y in uG & uG = [y,uG]);
then consider y being set such that y in uG and
A2: uG = [y,uG];
thus ex x being object st x in uG & u = [x, uG] by A2,Th2;
end;
end;
theorem Th95:
for G being SimpleGraph, u being object
st u in Vertices G holds { [u, union G] } in Mycielskian G
proof
let G be SimpleGraph, u be object such that
A1: u in Vertices G;
{ [u, union G], union G} in Edges Mycielskian G by A1,Th90;
then [u, union G] in Vertices Mycielskian G by Th13;
hence { [u, union G] } in Mycielskian G by Th24;
end;
theorem Th96:
for G being SimpleGraph, u being set
st u in Vertices G holds { [u, union G], union G} in Mycielskian G
proof
let G be SimpleGraph, u be set such that
A1: u in Vertices G;
{ [u, union G], union G} in Edges Mycielskian G by A1,Th90;
hence { [u, union G], union G} in Mycielskian G;
end;
theorem Th97:
for G being SimpleGraph, x, y being object
holds not {[x,union G],[y,union G]} in Edges Mycielskian G
proof
let G be SimpleGraph, x, y be object such that
A1: {[x,union G],[y,union G]} in Edges Mycielskian G;
A2: union G in {x,union G} by TARSKI:def 2;
A3: {x,union G} in {{x},{x,union G}} by TARSKI:def 2;
A4: not [x,union G] in union G by A2,A3,XREGULAR:7;
A5: not [x,union G] = union G by A2,TARSKI:def 2;
A6: union G in {y,union G} by TARSKI:def 2;
A7: {y,union G} in {{y},{y,union G}} by TARSKI:def 2;
A8: not [y,union G] in union G by A6,A7,XREGULAR:7;
A9: not [y,union G] = union G by A6,TARSKI:def 2;
{[x,union G],[y,union G]} in Edges G by A1,A4,A5,A8,A9,Th93;
hence contradiction by A4,Th13;
end;
theorem Th98:
for G being SimpleGraph, x, y being object
st x <> y holds not {[x,union G],[y,union G]} in Mycielskian G
proof
let G be SimpleGraph, x, y be object such that
A1: x <> y and
A2: {[x,union G],[y,union G]} in Mycielskian G;
[x,union G] <> [y,union G] by A1,XTUPLE_0:1;
then card {[x,union G],[y,union G]} = 2 by CARD_2:57;
then {[x,union G],[y,union G]} in Edges Mycielskian G by A2,Def1;
hence contradiction by Th97;
end;
theorem Th99:
for G being SimpleGraph, x, y being object
st {[x,union G], y} in Edges Mycielskian G
holds x <> y & x in union G & (y in union G or y = union G)
proof
let G be SimpleGraph, x, y be object such that
A1: {[x,union G], y} in Edges Mycielskian G;
set uG = union G; set e = {[x,union G],y};
per cases by A1,Th90;
suppose e in Edges G;
then [x,uG] in uG by Th13;
hence x<>y & x in union G & (y in union G or y = union G) by Th1;
end;
suppose ex x, y being Element of uG
st e = {x,[y,union G]} & {x,y} in Edges G;
then consider xa, ya being Element of uG such that
A2: e = {xa,[ya,union G]} and
A3: {xa,ya} in Edges G;
consider xx, yy being set such that
A4: xx <> yy and
A5: xx in Vertices G & yy in Vertices G and
A6: {xa,ya} = {xx, yy} by A3,Th11;
A7: xa = xx & ya = yy or xa =yy & ya = xx by A6,ZFMISC_1:6;
per cases by A2,ZFMISC_1:6;
suppose xa = [x,uG] & y = [ya,uG];
hence thesis by A5,Th1;
end;
suppose xa = y & [ya,uG] = [x,uG];
hence x<>y & x in union G & (y in union G or y = union G)
by A4,A5,A7,XTUPLE_0:1;
end;
end;
suppose ex y being Element of union G
st e = {union G,[y,union G]} & y in union G;
then consider yy being Element of uG such that
A8: e = {union G,[yy,union G]} and
A9: yy in union G;
A10: uG = [x,uG] & y = [yy,uG] or uG = y & [x,uG] = [yy, uG]
by A8,ZFMISC_1:6;
x = yy by A10,Th2,XTUPLE_0:1;
hence x<>y & x in union G & (y in union G or y = union G) by A10,A9;
end;
end;
theorem Th100:
for G being SimpleGraph, x, y being set
st {[x,union G], y} in Mycielskian G holds x <> y
proof
let G be SimpleGraph, x, y be set;
set MG = Mycielskian G; set uG = union G;
assume A1: {[x,uG], y} in MG;
assume A2: x = y;
then [x,uG] <> y by Th3;
then {[x,uG], y} in Edges MG by A1,Th12;
hence thesis by A2,Th99;
end;
theorem Th101:
for G being SimpleGraph, x, y being set
st y in union G & {[x,union G], y} in Mycielskian G holds {x, y} in G
proof
let G be SimpleGraph;
set MG = Mycielskian G; set uG = union G;
set A = { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set B = { {uG,[y,uG]} where y is Element of uG : y in uG };
let x, y be set;
assume A1: y in uG;
assume {[x,uG], y} in MG;
then {[x,uG], y} in { {} } \/ singletons Vertices MG \/ Edges MG by Th27;
then A2: {[x,uG], y} in { {} } \/ singletons Vertices MG
or {[x,uG], y} in Edges MG by XBOOLE_0:def 3;
per cases by A2,XBOOLE_0:def 3;
suppose {[x,uG], y} in { {} };
hence thesis by TARSKI:def 1;
end;
suppose {[x,uG], y} in singletons Vertices MG;
then consider f being Subset of Vertices MG such that
A3: f = {[x,uG], y} and
A4: f is 1-element;
consider s being set such that s in Vertices MG and
A5: f = {s} by A4,Th9;
A6: card f = 1 by A5,CARD_1:30;
y = [x,uG] by A6,A3,CARD_2:57;
hence thesis by A1,Th1;
end;
suppose {[x,uG], y} in Edges MG;
then {[x,uG], y} in (Edges G) \/ A \/ B by Th91;
then A7: {[x,uG], y} in (Edges G) \/ A or {[x,uG], y} in B
by XBOOLE_0:def 3;
per cases by A7,XBOOLE_0:def 3;
suppose {[x,uG], y} in Edges G;
then [x,uG] in uG by Th13;
hence thesis by Th1;
end;
suppose {[x,uG], y} in A;
then consider xx, yy being Element of uG such that
A8: {[x,uG], y} = {xx,[yy,uG]} and
A9: {xx,yy} in Edges G;
A10: xx in uG & yy in uG by A9,Th13;
[x,uG] = xx & y = [yy,uG] or [x,uG] = [yy,uG] & y = xx
by A8,ZFMISC_1:6;
then x = yy & y = xx by A10,Th1,XTUPLE_0:1;
hence thesis by A9;
end;
suppose {[x,uG], y} in B;
then consider yy being Element of uG such that
A11: {[x,uG], y} = {uG,[yy,uG]} and yy in uG;
[x,uG] = uG & y = [yy,uG] or [x,uG] = [yy,uG] & y = uG
by A11,ZFMISC_1:6;
hence thesis by Th1,A1;
end;
end;
end;
theorem Th102:
for G being SimpleGraph, x, y being set
st {x, y} in Edges G holds {[x,union G], y} in Mycielskian G
proof
let G be SimpleGraph;
set uG = union G;
let x, y be set;
A1: { {xx,[yy,uG]} where xx, yy is Element of uG : {xx,yy} in Edges G }
c= Mycielskian G by MYCIELSK:3;
assume A2: {x, y} in Edges G;
then x in uG & y in uG by Th13;
then {[x,uG], y} in
{ {xx,[yy,uG]} where xx, yy is Element of uG : {xx,yy} in Edges G } by A2;
hence {[x,union G], y} in Mycielskian G by A1;
end;
theorem Th103:
for G being SimpleGraph, x, y being set
st x in Vertices G & y in Vertices G & {x, y} in Mycielskian G
holds {x, y} in G
proof
let G be SimpleGraph, s, t be set such that
A1: s in Vertices G and
A2: t in Vertices G and
A3: {s, t} in Mycielskian G;
per cases;
suppose s = t;
then {s,t} = {s} by ENUMSET1:29;
hence {s, t} in G by A1,Th24;
end;
suppose s<>t;
then card {s,t} = 2 by CARD_2:57;
then A4: {s, t} in Edges Mycielskian G by A3,Def1;
per cases by A4,Th93;
suppose {s, t} in Edges G;
hence {s, t} in G;
end;
suppose (s in union G or s = union G)
& (ex y being object st y in union G & t = [y,union G]);
then consider y be set such that y in union G and
A5: t = [y,union G];
thus {s, t} in G by A5,A2,Th1;
end;
suppose (t in union G or t = union G)
& (ex y being object st y in union G & s = [y,union G]);
then consider y being set such that y in union G and
A6: s = [y,union G];
thus {s, t} in G by A6,A1,Th1;
end;
end;
end;
theorem Th104:
for G being SimpleGraph holds G = (Mycielskian G) SubgraphInducedBy Vertices G
proof
let G be SimpleGraph;
set L = Vertices G, MG = Mycielskian G;
thus G c= MG SubgraphInducedBy L by Th84,Th44;
thus MG SubgraphInducedBy L c= G proof
let a be object;
assume A1: a in MG SubgraphInducedBy L;
reconsider m = a as set by TARSKI:1;
A2: m in bool L by A1,XBOOLE_0:def 4;
per cases by A1,MYCIELSK:4;
suppose m in { {} };
then m = {} by TARSKI:def 1;
hence a in G by Th20;
end;
suppose m in the set of all {x} where x is Element of L \/ [:L,{L}:] \/ {L};
then consider x being Element of L \/ [:L,{L}:] \/ {L} such that
A3: m = {x};
x in m by A3,TARSKI:def 1;
hence a in G by A2,A3,Th24;
end;
suppose m in Edges G;
hence a in G;
end;
suppose m in { {x,[y,L]} where x, y is Element of L :
{x,y} in Edges G };
then consider x, y being Element of L such that
A4: m = {x,[y,L]} and {x,y} in Edges G;
[y,L] in m by A4,TARSKI:def 2;
hence a in G by A2,Th1;
end;
suppose m in { {L,[x,L]} where x is Element of L : x in Vertices G };
then consider x being Element of L such that
A5: m = {L,[x,L]} and x in Vertices G;
L in m by A5,TARSKI:def 2;
then L in L by A2;
hence a in G;
end;
end;
end;
theorem Th105:
for G being SimpleGraph, C being finite Clique of Mycielskian G
st 3 <= order C for v being Vertex of C holds v <> union G
proof
let G be SimpleGraph, C be finite Clique of Mycielskian G such that
A1: 3 <= order C;
set MG = Mycielskian G;
let v be Vertex of C such that
A2: v = union G;
Segm 3 c= Segm order C by A1,NAT_1:39;
then consider v1, v2 being object such that
A3: v1 in Vertices C and
A4: v2 in Vertices C and
A5: v1<>v and
A6: v2<>v and
A7: v1<>v2 by Th5;
A8: {v,v1} in C by A3,Th53;
A9: {v,v2} in C by A4,Th53;
A10: {v, v1} in Edges MG by A8,A5,Th12;
A11: {v, v2} in Edges MG by A6,A9,Th12;
consider x1 being object such that x1 in union G and
A12: v1 = [x1, union G] by A2,A10,Th94;
consider x2 being object such that x2 in union G and
A13: v2 = [x2, union G] by A2,A11,Th94;
{v1, v2} in C by A3,A4,Th53;
hence contradiction by A12,A13,A7,Th98;
end;
theorem Th106: :: MClique0
for G being with_finite_clique# SimpleGraph st clique# G = 0
for D being finite Clique of Mycielskian G holds order D <= 1
proof
let G be with_finite_clique# SimpleGraph such that
A1: clique# G = 0;
set uG = union G;
A2: Vertices G = {} by A1,Th54;
A3: G is void by A2,Th28;
A4: union Mycielskian G
= union {{},{uG}} by A3,Th88
.= {} \/ {uG} by ZFMISC_1:75
.= {uG};
let D be finite Clique of Mycielskian G;
Vertices D c= {uG} by A4,ZFMISC_1:77;
then Segm card Vertices D c= Segm card {uG} by CARD_1:11;
then card Vertices D <= card {uG} by NAT_1:39;
hence order D <= 1 by CARD_1:30;
end;
theorem :: MGsingle:
for G being SimpleGraph, x being set st Vertices G = {x}
holds Mycielskian G = {{},{x},{[x,union G]}, {union G}, {[x,union G],union G}}
proof
let G be SimpleGraph, a be set such that A1: Vertices G = {a};
A2: card Vertices G = 1 by A1,CARD_1:30;
A3: a in Vertices G by A1,TARSKI:def 1;
set uG = union G; set MG = Mycielskian G;
set A = the set of all
{x} where x is Element of (union G)\/[:uG,{uG}:] \/ {uG};
set B = {{x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
set C = { {uG,[x,uG]} where x is Element of uG : x in Vertices G };
consider aa being object such that
A4: uG = {aa} by A2,CARD_2:42;
A5: a = aa by A4,A3,TARSKI:def 1;
A6: [:uG,{uG}:] = {[a,uG]} by A4,A5,ZFMISC_1:29;
A7: G is edgeless by A2,Th19;
thus Mycielskian G c= {{},{a},{[a,uG]}, {uG}, {[a,uG],uG}} proof
let e be object;
assume A8: e in MG;
per cases by A8,MYCIELSK:4;
suppose e in {{}};
then e = {} by TARSKI:def 1;
hence e in {{},{a},{[a,uG]}, {uG}, {[a,uG],uG}} by ENUMSET1:def 3;
end;
suppose e in A;
then consider x being Element of uG \/ [:uG,{uG}:] \/ {uG} such that
A9: e = {x};
x in uG \/ [:uG,{uG}:] or x in {uG} by XBOOLE_0:def 3;
then x in uG or x in [:uG,{uG}:] or x in {uG} by XBOOLE_0:def 3;
then x = a or x = [a,uG] or x = uG by A4,A5,A6,TARSKI:def 1;
hence thesis by A9,ENUMSET1:def 3;
end;
suppose e in Edges G;
hence thesis by A7;
end;
suppose e in B;
then consider x, y being Element of uG such that e = {x,[y,uG]} and
A10: {x,y} in Edges G;
thus thesis by A10,A7;
end;
suppose e in C;
then consider x being Element of uG such that
A11: e = {uG,[x,uG]} and x in Vertices G;
x = a by A4,A5,TARSKI:def 1;
hence thesis by A11,ENUMSET1:def 3;
end;
end;
thus {{},{a},{[a,union G]}, {union G}, {[a,union G],union G}} c= Mycielskian G
proof
let e be object;
assume A12: e in {{},{a},{[a,union G]}, {union G}, {[a,union G],union G}};
per cases by A12,ENUMSET1:def 3;
suppose e = {};
hence e in MG by Th20;
end;
suppose A13: e = {a};
a in uG \/ [:uG,{uG}:] by A3,XBOOLE_0:def 3;
then a in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then e in A by A13;
hence e in MG by MYCIELSK:4;
end;
suppose A14: e = {[a,union G]};
[a,union G] in [:uG,{uG}:] by A6,TARSKI:def 1;
then [a,union G] in uG \/ [:uG,{uG}:] by XBOOLE_0:def 3;
then [a,union G] in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then e in A by A14;
hence e in MG by MYCIELSK:4;
end;
suppose A15: e = {uG};
uG in {uG} by TARSKI:def 1;
then uG in uG \/ [:uG,{uG}:] \/ {uG} by XBOOLE_0:def 3;
then e in A by A15;
hence e in MG by MYCIELSK:4;
end;
suppose e = {[a,uG],uG};
then e in C by A3;
hence e in MG by MYCIELSK:4;
end;
end;
end;
theorem Th108: :: MClique1
for G being with_finite_clique# SimpleGraph st clique# G = 1
for D being finite Clique of Mycielskian G holds order D <= 2
proof
let G be with_finite_clique# SimpleGraph such that
A1: clique# G = 1;
set uG = union G; set MG = Mycielskian G; set uMG = union MG;
let D be finite Clique of Mycielskian G;
set uD = union D;
assume A2: order D > 2;
then A3: order D >= 2+1 by NAT_1:13;
uD is non empty by A2;
then consider v being object such that
A4: v in uD;
A5: v <> uG by A4,A3,Th105;
Segm 3 c= Segm order D by A3,NAT_1:39;
then consider v1, v2 being object such that
A6: v1 in uD and v2 in uD and
A7: v1<>v and v2<>v and v1<>v2 by Th5;
A8: v1 <> uG by A6,A3,Th105;
set e = {v,v1};
e in D by A4,A6,Th53;
then A9: e in Edges MG by A7,Th12;
per cases by A9,Th90;
suppose e in Edges G;
hence contradiction by A1,Th57;
end;
suppose ex x, y being Element of union G
st e = {x,[y,uG]} & {x,y} in Edges G;
then consider x, y being Element of uG such that e = {x,[y,uG]} and
A10: {x,y} in Edges G;
thus contradiction by A1,A10,Th57;
end;
suppose ex y being Element of union G st e = {uG,[y,uG]} & y in uG;
then consider y being Element of uG such that
A11: e = {uG,[y,uG]} and y in uG;
thus contradiction by A5,A8,A11,ZFMISC_1:6;
end;
end;
theorem Th109: :: MClique2
for G being with_finite_clique# SimpleGraph st 2 <= clique# G
for D being finite Clique of Mycielskian G holds order D <= clique# G
proof
let G be with_finite_clique# SimpleGraph such that
A1: 2 <= clique# G;
let D be finite Clique of Mycielskian G such that
A2: order D > clique# G;
set MG = Mycielskian G, uG = union G;
A3: Vertices D c= Vertices MG by ZFMISC_1:77;
A4: Edges D c= Edges MG by Th14;
2 < order D by A2,A1,XXREAL_0:2;
then A5: 2+1 <= order D by NAT_1:13;
per cases;
suppose D c= G;
hence contradiction by A2,Def15;
end;
suppose not D c= G;
then consider e being object such that
A6: e in D and
A7: not e in G;
now
assume A8: Vertices D c= Vertices G;
A9: e <> {} by A7,Th20;
now assume not e in Edges D;
then consider y being set such that
A10: e = {y} and
A11: y in Vertices D by A9,A6,Th29;
thus contradiction by A7,A10,A11,A8,Th24;
end;
then consider x, y being set such that x <> y and
A12: x in Vertices D and
A13: y in Vertices D and
A14: e = {x, y} by Th11;
thus contradiction by A6,A8,A14,A7,Th103,A12,A13;
end;
then consider v being object such that
A15: v in Vertices D and
A16: not v in Vertices G;
Segm 3 c= Segm order D by A5,NAT_1:39;
then consider v1, v2 being object such that
A17: v1 in Vertices D and
A18: v2 in Vertices D and
A19: v1<>v and
A20: v2<>v and
A21: v1<>v2 by Th5;
{v,v1} in D by A15,A17,Th53; then
A22: {v, v1} in Edges D by A19,Th12;
{v,v2} in D by A15,A18,Th53; then
A23: {v, v2} in Edges D by A20,Th12;
{v1,v2} in D by A17,A18,Th53; then
A24: {v1, v2} in Edges D by A21,Th12;
per cases by A15,A3,A16,Th85;
suppose A25: v = uG;
consider x being object such that x in union G and
A26: v1 = [x, union G] by A25,A22,A4,Th94;
consider y being object such that y in union G and
A27: v2 = [y, union G] by A25,A23,A4,Th94;
thus contradiction by A24,A4,A26,A27,Th97;
end;
suppose ex x being set st x in union G & v = [x,union G];
then consider x being set such that
A28: x in uG and
A29: v = [x,uG];
set E = D SubgraphInducedBy union G;
reconsider F = G SubgraphInducedBy ({x} \/ union E) as finite SimpleGraph;
A30: Vertices F = {x} \/ Vertices E proof
thus Vertices F c= {x} \/ Vertices E proof
let a be object;
assume a in Vertices F;
then a in (union G) /\ ({x} \/ union E) by Th45;
then A31: a in {x} \/ union E by XBOOLE_0:def 4;
per cases by A31,XBOOLE_0:def 3;
suppose a in {x};
hence thesis by XBOOLE_0:def 3;
end;
suppose a in union E;
hence thesis by XBOOLE_0:def 3;
end;
end;
let a be object;
assume A32: a in {x} \/ Vertices E;
per cases by A32,XBOOLE_0:def 3;
suppose a in {x};
then A33: a = x by TARSKI:def 1;
x in {x} by TARSKI:def 1;
then x in {x} \/ union E by XBOOLE_0:def 3;
then x in (union G) /\ ({x} \/ union E) by A28,XBOOLE_0:def 4;
hence a in Vertices F by A33,Th45;
end;
suppose a in Vertices E;
then a in (union D) /\ union G by Th45;
then a in union G by XBOOLE_0:def 4;
then a in (union G) /\ ({x} \/ union E) by A32,XBOOLE_0:def 4;
hence a in Vertices F by Th45;
end;
end;
A34: union E c= union D by ZFMISC_1:77;
A35: now
assume x in union E;
then {[x,uG],x} in D by A34,A15,A29,Th53;
hence contradiction by Th100;
end;
reconsider Fs = F as SimpleGraph-like Subset of G;
now
let a, b be set such that
A36: a <> b and
A37: a in union Fs and
A38: b in union Fs;
A39: a in (union G) /\ ({x} \/ union E) by A37,Th45;
then A40: a in union G & a in {x} \/ union E by XBOOLE_0:def 4;
A41: b in (union G) /\ ({x} \/ union E) by A38,Th45;
then A42: b in union G & b in {x} \/ union E by XBOOLE_0:def 4;
A43: a in Vertices G by A39,XBOOLE_0:def 4;
A44: b in Vertices G by A41,XBOOLE_0:def 4;
x in {x} by TARSKI:def 1;
then A45: x in {x} \/ union E by XBOOLE_0:def 3;
{a,b} in Fs proof
per cases by A40,A42,XBOOLE_0:def 3;
suppose a in {x} & b in {x};
then A46: a = x & b = x by TARSKI:def 1;
then {a,b} = {x} by ENUMSET1:29;
hence {a,b} in Fs by A46,A37,Th24;
end;
suppose A47: a in {x} & b in union E;
then A48: a = x by TARSKI:def 1;
b in (union D) /\ union G by A47,Th45;
then A49: b in union D & b in uG by XBOOLE_0:def 4;
then {[x,uG], b} in D by A15,A29,Th53;
then {x,b} in G by A49,Th101;
hence {a,b} in Fs by A45,A48,A42,Lm10;
end;
suppose A50: b in {x} & a in union E;
then A51: b = x by TARSKI:def 1;
a in (union D) /\ union G by A50,Th45;
then A52: a in union D & a in uG by XBOOLE_0:def 4;
then {[x,uG], a} in D by A15,A29,Th53;
then {x,a} in G by A52,Th101;
hence {a,b} in Fs by A45,A51,A40,Lm10;
end;
suppose a in union E & b in union E;
then a in (union D) /\ union G & b in (union D) /\ union G by Th45;
then a in union D & b in union D by XBOOLE_0:def 4;
then {a,b} in D by Th53;
then {a,b} in G by A43,A44,Th103;
hence {a,b} in Fs by A40,A42,Lm10;
end;
end;
hence {a,b} in Edges Fs by A36,Th12;
end; then
A53: Fs is clique by Th47;
A54: Vertices D c= {v} \/ Vertices E proof
let a be object such that
A55: a in Vertices D;
per cases;
suppose a = v;
then a in {v} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose A56: a <> v;
{a,[x,uG]} in D by A29,A15,A55,Th53; then
{a,[x,uG]} in Edges D by A56,A29,Th12;
then a in uG or a = uG by A4,Th99;
then a in Vertices E by A5,Th105,A55,Lm8;
hence thesis by XBOOLE_0:def 3;
end;
end;
A57: Vertices E c= Vertices D by ZFMISC_1:77;
A58: {v} \/ Vertices E c= Vertices D proof
let a be object;
assume a in {v} \/ Vertices E;
then a in {v} or a in Vertices E by XBOOLE_0:def 3;
hence thesis by A15,A57,TARSKI:def 1;
end;
A59: not v in Vertices E by A29,Lm7,Th1;
order F = 1 + card Vertices E by A30,A35,CARD_2:41
.= card ({v} \/ Vertices E) by A59,CARD_2:41
.= order D by A58,A54,XBOOLE_0:def 10;
hence contradiction by A2,A53,Def15;
end;
end;
end;
registration
let G be with_finite_clique# SimpleGraph;
cluster Mycielskian G -> with_finite_clique#;
coherence proof
set MG = Mycielskian G; set uG = union G;
per cases by NAT_1:25;
suppose A1: clique# G = 0;
then uG = {} by Th54;
then {} in union MG by Th87;
then consider C being finite Clique of MG such that
A2: Vertices C = {{}} by Th52;
take C;
order C = 1 by A2,CARD_1:30;
hence for D being finite Clique of MG holds order D <= order C
by A1,Th106;
end;
suppose A3: clique# G = 1;
then consider C being finite Clique of G such that
A4: order C = 1 by Def15;
A5: union C c= union G by ZFMISC_1:77;
Vertices C <> {} by A4;
then consider v being object such that
A6: v in Vertices C by XBOOLE_0:def 1;
A7: [v,uG] in union MG by A6,A5,Th85;
A8: uG in union MG by Th87;
A9: {[v,uG],uG} in MG by A6,A5,Th96;
reconsider CC = {{},{[v,uG]},{uG},{[v,uG],uG}}
as finite Clique of MG by A7,A8,A9,Th51;
A10: CC = CompleteSGraph {[v,uG],uG} by Th37;
A11: Vertices CC = {[v,uG],uG} by A10,Lm1;
take CC;
order CC = 2 by A11,Th2,CARD_2:57;
hence for D being finite Clique of MG holds order D <= order CC
by A3,Th108;
end;
suppose clique# G > 1;
then A12: clique# G >= 1+1 by NAT_1:13;
consider C being finite Clique of G such that
A13: order C = clique# G by Def15;
G c= MG by Th84; then
reconsider CC = C as finite Clique of MG by XBOOLE_1:1;
take CC;
thus for D being finite Clique of MG holds order D <= order CC
by A13,A12,Th109;
end;
end;
end;
theorem Th110: :: MClique
for G being with_finite_clique# SimpleGraph
st 2 <= clique# G holds clique# Mycielskian G = clique# G
proof
let G be with_finite_clique# SimpleGraph such that
A1: 2 <= clique# G and
A2: clique# Mycielskian G <> clique# G;
set MG = Mycielskian G;
consider D being finite Clique of MG such that
A3: order D = clique# MG by Def15;
clique# G <= clique# MG by Th84,Th58;
then clique# G < clique# MG by A2,XXREAL_0:1;
hence contradiction by A1,A3,Th109;
end;
theorem Th111:
for G being finitely_colorable SimpleGraph
ex E being Coloring of Mycielskian G st card E = 1 + chromatic# G
proof
let G be finitely_colorable SimpleGraph;
set uG = union G;
set MG = Mycielskian G; set uMG = union MG;
set cnG = chromatic# G;
consider C being finite Coloring of G such that
A1: card C = cnG by Def22;
defpred P[object,object] means
ex A being set st A = $1 &
$2 = { [x,uG] where x is Element of uG : x in A };
A2: for e being object st e in C ex u being object st P[e,u]
proof let e be object such that
e in C;
reconsider A = e as set by TARSKI:1;
take u = { [x,uG] where x is Element of uG : x in A };
thus P[e,u];
end;
consider r being Function such that dom r = C and
A3: for e being object st e in C holds P[e,r.e] from CLASSES1:sch 1(A2);
set D = { d \/ r.d where d is Element of C : d in C };
A4: card D = card C proof
per cases;
suppose A5: D is empty;
now assume C is non empty;
then consider c being object such that
A6: c in C;
reconsider c as set by TARSKI:1;
c \/ r.c in D by A6;
hence contradiction by A5;
end;
hence thesis by A5;
end;
suppose A7: D is non empty;
defpred R[object,object] means
ex A being set st A = $1 & $2 = A \/ r.$1;
A8: for e being object st e in C ex u being object st R[e,u]
proof let e be object such that
e in C;
reconsider A = e as set by TARSKI:1;
take u = A \/ r.e;
thus R[e,u];
end;
consider s being Function such that
A9: dom s = C and
A10: for e being object st e in C holds R[e,s.e] from CLASSES1:sch 1(A8);
A11: rng s c= D proof
let y be object;
assume y in rng s;
then consider x being object such that
A12: x in dom s and
A13: y = s.x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
R[x,y] by A12,A13,A9,A10;
then y = x \/ r.x;
hence y in D by A12,A9;
end;
then reconsider s as Function of C, D by A9,FUNCT_2:2;
D c= rng s proof
let x be object;
assume x in D;
then consider c being Element of C such that
A14: x = c \/ r.c and
A15: c in C;
R[c,s.c] by A15,A10;
then x = s.c by A14;
hence x in rng s by A15,A9,FUNCT_1:def 3;
end;
then rng s = D by A11;
then
A16: s is onto by FUNCT_2:def 3;
s is one-to-one proof
let x1,x2 be object such that
A17: x1 in dom s and
A18: x2 in dom s and
A19: s.x1 = s.x2;
reconsider x1,x2 as set by TARSKI:1;
R[x1,s.x1] by A17,A9,A10;
then
A20: s.x1 = x1 \/ r.x1;
R[x2,s.x2] by A18,A9,A10;
then
A21: s.x2 = x2 \/ r.x2;
A22: x1 c= x2 proof
let x be object;
assume A23: x in x1;
A24: x in s.x1 by A20,A23,XBOOLE_0:def 3;
per cases by A24,A19,A21,XBOOLE_0:def 3;
suppose x in x2;
hence thesis;
end;
suppose
A25: x in r.x2;
P[x2,r.x2] by A3,A9,A18;
then x in { [xx,uG] where xx is Element of uG : xx in x2 }
by A25;
then consider xx being Element of uG such that
A26: x = [xx,uG] and xx in x2;
thus thesis by A26,A17,A23,A9,Th1;
end;
end;
x2 c= x1 proof
let x be object;
assume A27: x in x2;
A28: x in s.x2 by A21,A27,XBOOLE_0:def 3;
per cases by A28,A19,A20,XBOOLE_0:def 3;
suppose x in x1;
hence thesis;
end;
suppose
A29: x in r.x1;
P[x1,r.x1] by A3,A9,A17;
then x in { [xx,uG] where xx is Element of uG : xx in x1 }
by A29;
then consider xx being Element of uG such that
A30: x = [xx,uG] and xx in x1;
thus thesis by A30,A18,A27,A9,Th1;
end;
end;
hence thesis by A22,XBOOLE_0:def 10;
end;
hence thesis by A16,A7,EULER_1:11;
end;
end;
A31: D is finite by A4;
set E = D \/ {{uG}};
A32: union E = uMG proof
thus union E c= uMG proof
let x be object;
assume x in union E;
then consider Y being set such that
A33: x in Y and
A34: Y in E by TARSKI:def 4;
per cases by A34,XBOOLE_0:def 3;
suppose Y in D;
then consider d being Element of C such that
A35: Y = d \/ r.d and
A36: d in C;
per cases by A35,A33,XBOOLE_0:def 3;
suppose A37: x in d;
A38: uG c= uMG by Th84,ZFMISC_1:77;
x in uG by A37;
hence x in uMG by A38;
end;
suppose
A39: x in r.d;
P[d,r.d] by A3,A36;
then x in { [yy,uG] where yy is Element of uG : yy in d } by A39;
then consider yy being Element of uG such that
A40: x = [yy,uG] and
A41: yy in d;
{x} in MG by A40,A41,Th95;
hence x in uMG by Th24;
end;
end;
suppose Y in {{uG}};
then Y = {uG} by TARSKI:def 1;
then x = uG by A33,TARSKI:def 1;
hence x in uMG by Th87;
end;
end;
thus uMG c= union E proof
let a be object;
assume a in uMG;
then consider Y being set such that
A42: a in Y and
A43: Y in MG by TARSKI:def 4;
A44: a in uG implies a in union E proof
assume a in uG;
then a in union C by EQREL_1:def 4;
then consider d being set such that
A45: a in d and
A46: d in C by TARSKI:def 4;
A47: a in d \/ r.d by A45,XBOOLE_0:def 3;
d \/ r.d in D by A46;
then d \/ r.d in E by XBOOLE_0:def 3;
hence a in union E by A47,TARSKI:def 4;
end;
A48: now let x be set;
assume A49: a = [x,uG];
assume A50: x in uG; then
x in union C by EQREL_1:def 4;
then consider d being set such that
A51: x in d and
A52: d in C by TARSKI:def 4;
d \/ r.d in D by A52;
then A53: d \/ r.d in E by XBOOLE_0:def 3;
A54: a in { [xx,uG] where xx is Element of uG : xx in d }
by A51,A49,A50;
P[d,r.d] by A3,A52;
then a in r.d by A54;
then a in d \/ r.d by XBOOLE_0:def 3;
hence a in union E by A53,TARSKI:def 4;
end;
per cases by A43,MYCIELSK:4;
suppose Y in { {} };
hence a in union E by A42,TARSKI:def 1;
end;
suppose Y in the set of all
{x} where x is Element of (uG) \/ [:uG,{uG}:] \/ {uG};
then consider x being Element of (uG) \/ [:uG,{uG}:] \/ {uG} such that
A55: Y = {x};
A56: a = x by A55,A42,TARSKI:def 1;
A57: a in (uG) \/ [:uG,{uG}:] or a in {uG} by A56,XBOOLE_0:def 3;
per cases by A57,XBOOLE_0:def 3;
suppose a in uG;
hence a in union E by A44;
end;
suppose a in [:uG,{uG}:];
then consider x, y being object such that
A58: x in uG and
A59: y in {uG} and
A60: a = [x,y] by ZFMISC_1:def 2;
y = uG by A59,TARSKI:def 1;
hence a in union E by A58,A60,A48;
end;
suppose A61: a in {uG};
{uG} in {{uG}} by TARSKI:def 1;
then {uG} in E by XBOOLE_0:def 3;
hence a in union E by A61,TARSKI:def 4;
end;
end;
suppose Y in (Edges G);
then consider p, r being set such that p <> r and
A62: p in Vertices G and
A63: r in Vertices G and
A64: Y = {p, r} by Th11;
thus a in union E by A44,A62,A63,A64,A42,TARSKI:def 2;
end;
suppose Y in { {x,[y,uG]} where x, y is Element of uG : {x,y} in Edges G };
then consider x, y being Element of uG such that
A65: Y = {x,[y,uG]} and
A66: {x,y} in Edges G;
A67: a = x or a = [y,uG] by A42,A65,TARSKI:def 2;
x in uG by A66,Th13;
hence a in union E by A67,A44,A48;
end;
suppose Y in { {uG,[x,uG]} where x is Element of uG : x in Vertices G };
then consider x being Element of uG such that
A68: Y = {uG,[x,uG]} and
A69: x in Vertices G;
per cases by A42,A68,TARSKI:def 2;
suppose a = uG;
then A70: a in {uG} by TARSKI:def 1;
{uG} in {{uG}} by TARSKI:def 1;
then {uG} in E by XBOOLE_0:def 3;
hence a in union E by A70,TARSKI:def 4;
end;
suppose A71: a = [x,uG];
thus a in union E by A71,A48,A69;
end;
end;
end;
end;
A72: now let A be Subset of uMG such that
A73: A in E;
per cases by A73,XBOOLE_0:def 3;
suppose A in D;
then consider d being Element of C such that
A74: A = d \/ r.d and
A75: d in C;
thus A<>{} by A74,A75;
thus for B being Subset of uMG st B in E holds A = B or A misses B proof
let B be Subset of uMG such that
A76: B in E;
per cases by A76,XBOOLE_0:def 3;
suppose B in D;
then consider e being Element of C such that
A77: B = e \/ r.e and
A78: e in C;
now assume A meets B;
then consider x being object such that
A79: x in A and
A80: x in B by XBOOLE_0:3;
per cases by A79,A80,A77,A74,XBOOLE_0:def 3;
suppose x in d & x in e;
then d = e by EQREL_1:70;
hence A = B by A77,A74;
end;
suppose A81: x in d & x in r.e;
then P[e,r.e] by A3;
then x in { [yy,uG] where yy is Element of uG : yy in e } by A81;
then consider yy being Element of uG such that
A82: x = [yy,uG] and yy in e;
thus A = B by A82,Th1,A81;
end;
suppose A83: x in r.d & x in e;
then P[d,r.d] by A3;
then x in { [yy,uG] where yy is Element of uG : yy in d } by A83;
then consider yy being Element of uG such that
A84: x = [yy,uG] and yy in d;
thus A = B by A84,Th1,A83;
end;
suppose A85: x in r.d & x in r.e;
P[d,r.d] by A3,A75;
then x in { [yy,uG] where yy is Element of uG : yy in d }
by A85;
then consider yy being Element of uG such that
A86: x = [yy,uG] and
A87: yy in d;
P[e,r.e] by A3,A78;
then x in { [zz,uG] where zz is Element of uG : zz in e }
by A85;
then consider zz being Element of uG such that
A88: x = [zz,uG] and
A89: zz in e;
yy = zz by A86,A88,XTUPLE_0:1;
then d = e by A87,A89,EQREL_1:70;
hence A = B by A77,A74;
end;
end;
hence A = B or A misses B;
end;
suppose B in {{uG}};
then A90: B = {uG} by TARSKI:def 1;
now assume A meets B;
then consider x being object such that
A91: x in A and
A92: x in B by XBOOLE_0:3;
A93: x = uG by A92,A90,TARSKI:def 1;
per cases by A93,A91,A74,XBOOLE_0:def 3;
suppose uG in d;
then uG in uG;
hence contradiction;
end;
suppose
A94: uG in r.d;
P[d,r.d] by A3,A75;
then uG in { [yy,uG] where yy is Element of uG : yy in d } by A94;
then consider yy being Element of uG such that
A95: uG = [yy,uG] and yy in d;
thus contradiction by A95,Th2;
end;
end;
hence A = B or A misses B;
end;
end;
end;
suppose A96: A in {{uG}};
then A97: A = {uG} by TARSKI:def 1;
thus A<>{} by A96;
thus for B being Subset of uMG st B in E holds A = B or A misses B proof
let B be Subset of uMG such that
A98: B in E;
per cases by A98,XBOOLE_0:def 3;
suppose B in D;
then consider d being Element of C such that
A99: B = d \/ r.d and
A100: d in C;
now assume A meets B;
then consider x being object such that
A101: x in A and
A102: x in B by XBOOLE_0:3;
A103: x = uG by A101,A97,TARSKI:def 1;
per cases by A103,A102,A99,XBOOLE_0:def 3;
suppose uG in d;
then uG in uG;
hence contradiction;
end;
suppose
A104: uG in r.d;
P[d,r.d] by A3,A100;
then uG in { [yy,uG] where yy is Element of uG : yy in d } by A104;
then consider yy being Element of uG such that
A105: uG = [yy,uG] and yy in d;
thus contradiction by A105,Th2;
end;
end;
hence A = B or A misses B;
end;
suppose B in {{uG}};
hence A = B or A misses B by A97,TARSKI:def 1;
end;
end;
end;
end;
A106: E c= bool uMG proof
let x be object;
reconsider x1 = x as set by TARSKI:1;
assume A107: x in E;
per cases by A107,XBOOLE_0:def 3;
suppose x in D;
then consider d being Element of C such that
A108: x = d \/ r.d and
A109: d in C;
A110: uG c= uMG by Th84,ZFMISC_1:77;
A111: d c= uMG by A110;
r.d c= uMG proof
let y be object;
assume
A112: y in r.d;
P[d,r.d] by A3,A109;
then y in { [yy,uG] where yy is Element of uG : yy in d } by A112;
then consider yy being Element of uG such that
A113: y = [yy,uG] and
A114: yy in d;
{y} in MG by A113,A114,Th95;
hence y in uMG by Th24;
end;
then x1 c= uMG by A108,A111,XBOOLE_1:8;
hence x in bool uMG;
end;
suppose x in {{uG}};
then A115: x = {uG} by TARSKI:def 1;
uG in uMG by Th87;
then x1 c= uMG by A115,ZFMISC_1:31;
hence x in bool uMG;
end;
end;
reconsider E as a_partition of uMG by A32,A72,A106,EQREL_1:def 4;
E is StableSet-wise proof
let e be set such that
A116: e in E;
reconsider e1 = e as Subset of uMG by A116;
e1 is stable proof
let x, y be set such that
A117: x <> y and
A118: x in e1 and
A119: y in e1;
per cases by A116,XBOOLE_0:def 3;
suppose e in D;
then consider d being Element of C such that
A120: e = d \/ r.d and
A121: d in C;
A122: P[d,r.d] by A3,A121;
A123: d is stable by Def20;
per cases by A120,A118,A119,XBOOLE_0:def 3;
suppose A124: x in d & y in d;
then {x,y} nin G by A123,A117;
hence {x,y} nin MG by A124,Th103;
end;
suppose that A125: x in d and A126: y in r.d;
consider x1 being Element of uG such that
A127: y = [x1,uG] and
A128: x1 in d by A126,A122;
per cases;
suppose x1 = x;
hence {x,y} nin MG by A127,Th100;
end;
suppose x1 <> x;
then {x1,x} nin G by A125,A128,A123;
hence {x,y} nin MG by A125,A127,Th101;
end;
end;
suppose that A129: x in r.d and A130: y in d;
consider x1 being Element of uG such that
A131: x = [x1,uG] and
A132: x1 in d by A129,A122;
per cases;
suppose x1 = y;
hence {x,y} nin MG by A131,Th100;
end;
suppose x1 <> y;
then {x1,y} nin G by A130,A132,A123;
hence {x,y} nin MG by A131,A130,Th101;
end;
end;
suppose that A133: x in r.d and A134: y in r.d;
consider x1 being Element of uG such that
A135: x = [x1,uG] and x1 in d by A133,A122;
consider y1 being Element of uG such that
A136: y = [y1,uG] and y1 in d by A134,A122;
thus {x,y} nin MG by A135,A136,A117,Th98;
end;
end;
suppose e in {{uG}};
then e = {uG} by TARSKI:def 1;
then x = uG & y = uG by A118,A119,TARSKI:def 1;
hence thesis by A117;
end;
end;
hence e is StableSet of MG;
end;
then reconsider E as Coloring of MG;
take E;
now
assume {uG} in D;
then consider d being Element of C such that
A137: {uG} = d \/ r.d and
A138: d in C;
A139: uG in d \/ r.d by A137,TARSKI:def 1;
per cases by A139,XBOOLE_0:def 3;
suppose uG in d;
then uG in uG;
hence contradiction;
end;
suppose
A140: uG in r.d;
P[d,r.d] by A3,A138;
then uG in { [x,uG] where x is Element of uG : x in d } by A140;
then consider x being Element of uG such that
A141: uG = [x,uG] and x in d;
thus contradiction by A141,Th2;
end;
end;
hence card E = 1 + cnG by A4,A31,A1,CARD_2:41;
end;
registration
let G be finitely_colorable SimpleGraph;
cluster Mycielskian G -> finitely_colorable;
coherence proof
consider E being Coloring of Mycielskian G such that
A1: card E = 1+chromatic# G by Th111;
E is finite by A1;
hence thesis;
end;
end;
theorem Th112:
for G being finitely_colorable SimpleGraph
holds chromatic# Mycielskian G = 1 + chromatic# G
proof :: Mfc1 + contradiction that there is a smaller one
let G be finitely_colorable SimpleGraph;
set uG = union G; set MG = Mycielskian G; set uMG = union MG;
set cnG = chromatic# G; set cnMG = chromatic# MG;
consider D being Coloring of MG such that
A1: card D = 1+cnG by Th111;
D is finite by A1; then
A2: cnMG <= 1 + cnG by A1,Def22;
now
assume A3: 1+cnG > cnMG;
A4: cnG >= cnMG by A3,NAT_1:13;
A5: cnG <= cnMG by Th84,Th68;
A6: cnG = cnMG by A4,A5,XXREAL_0:1;
consider E being finite Coloring of MG such that
A7: card E = cnMG by Def22;
A8: union E = union MG by EQREL_1:def 4;
A9: G = MG SubgraphInducedBy uG by Th104;
reconsider S = uG as Subset of Vertices MG by Th84,ZFMISC_1:77;
reconsider C = E | S as finite Coloring of G by A9,Th67;
A10: card C >= cnG by Def22;
A11: card C <= cnG by A6,A7,MYCIELSK:8;
A12: card C = cnG by A10,A11,XXREAL_0:1;
A13: uG in union MG by Th87;
then consider EuG being set such that
A14: uG in EuG and
A15: EuG in E by A8,TARSKI:def 4;
reconsider EuG as Subset of Vertices MG by A15;
reconsider uG as Element of Vertices MG by A14,A15;
set se = EuG /\ S;
A16: EuG meets S by A15,A6,A7,A12,MYCIELSK:9;
se in C by A15,A16;
then consider sev being Element of Vertices G such that
A17: sev in se and
A18: for d being Element of C st d <> se
ex w being Element of Vertices G st w in Adjacent(sev) & w in d
by A10,A11,Th70,XXREAL_0:1;
A19: uG is non empty by A16;
then {[sev,uG]} in MG by Th95;
then reconsider csev = [sev,uG] as Element of Vertices MG by Th24;
csev in Vertices MG by A13;
then csev in union E by EQREL_1:def 4;
then consider Ecse being set such that
A20: csev in Ecse and
A21: Ecse in E by TARSKI:def 4;
reconsider Ecse as Subset of Vertices MG by A21;
A22: now assume A23: EuG <> Ecse;
set sf = Ecse /\ S;
A24: Ecse meets S by A21,A6,A7,A12,MYCIELSK:9;
A25: sf in C by A24,A21;
now assume se = sf;
then sev in EuG & sev in Ecse by A17,XBOOLE_0:def 4;
then EuG meets Ecse by XBOOLE_0:3;
hence contradiction by A23,A21,A15,EQREL_1:def 4;
end;
then consider w being Element of Vertices G such that
A26: w in Adjacent(sev) and
A27: w in sf by A25,A18;
A28: w in Ecse by A27,XBOOLE_0:def 4;
A29: Ecse is stable by A21,Def20;
A30: csev <> w by A19,Th1;
{sev, w} in Edges G by A26,Def8;
then {csev,w} in MG by Th102;
hence contradiction by A29,A30,A28,A20;
end;
A31: {csev,uG} in Edges MG by A19,Th90;
A32: csev <> uG by Th2;
EuG is stable by A15,Def20;
hence contradiction by A32,A31,A22,A20,A14;
end;
hence thesis by A2,XXREAL_0:1;
end;
definition
let G be SimpleGraph;
func MycielskianSeq G -> ManySortedSet of NAT means :Def26:
ex myc being Function
st it = myc & myc.0 = G &
for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G;
existence proof
defpred P[Nat,set,set] means
($2 is SimpleGraph implies
ex G being SimpleGraph st $2 = G & $3 = Mycielskian G) &
(not $2 is SimpleGraph implies $3 = $2);
A1: for n being Nat, x being set ex y being set st P[n,x,y]
proof
let n be Nat, x be set;
per cases;
suppose x is SimpleGraph;
then reconsider G = x as SimpleGraph;
Mycielskian G = Mycielskian G;
hence ex y being set st P[n,x,y];
end;
suppose not x is SimpleGraph;
hence thesis;
end;
end;
consider f being Function such that
A2: dom f = NAT and
A3: f.0 = G and
A4: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 1(A1);
reconsider f as NAT-defined Function by A2,RELAT_1:def 18;
reconsider f as ManySortedSet of NAT by A2,PARTFUN1:def 2;
take f;
take myc = f;
thus f = myc;
thus myc.0 = G by A3;
let k be Nat, G be SimpleGraph such that
A5: G = myc.k;
ex G being SimpleGraph st f.k = G & f.(k+1) = Mycielskian G by A4,A5;
hence myc.(k+1) = Mycielskian G by A5;
end;
uniqueness proof
let it1, it2 be ManySortedSet of NAT;
given myc1 being Function such that
A6: it1 = myc1 and
A7: myc1.0 = G and
A8: for k being Nat, G being SimpleGraph
st G = myc1.k holds myc1.(k+1) = Mycielskian G;
given myc2 being Function such that
A9: it2 = myc2 and
A10: myc2.0 = G and
A11: for k being Nat, G being SimpleGraph
st G = myc2.k holds myc2.(k+1) = Mycielskian G;
defpred P[Nat] means myc1.$1 is SimpleGraph & myc1.$1 = myc2.$1;
A12: P[0] by A7,A10;
A13: for k being Nat st P[k] holds P[k+1] proof
let k be Nat;
assume A14: P[k];
reconsider H = myc1.k as SimpleGraph by A14;
myc1.(k+1) = Mycielskian H by A8;
hence myc1.(k+1) is SimpleGraph;
thus myc1.(k+1) = Mycielskian H by A8 .= myc2.(k+1) by A14,A11;
end;
A15: for k being Nat holds P[k] from NAT_1:sch 2(A12,A13);
for i being object st i in NAT holds myc1.i = myc2.i by A15;
hence it1 = it2 by A6,A9,PBOOLE:3;
end;
end;
theorem Th113:
for G being SimpleGraph holds (MycielskianSeq G).0 = G
proof
let G be SimpleGraph;
consider myc being Function such that
A1: MycielskianSeq G = myc and
A2: myc.0 = G and
for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G by Def26;
thus (MycielskianSeq G).0 = G by A1,A2;
end;
theorem Th114:
for G being SimpleGraph, n be Nat holds (MycielskianSeq G).n is SimpleGraph
proof
let G be SimpleGraph, n be Nat;
set MG = MycielskianSeq G;
defpred P[Nat] means MG.$1 is SimpleGraph;
consider myc being Function such that
A1: MycielskianSeq G = myc and
A2: myc.0 = G and
A3: for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G by Def26;
A4: P[0] by A1,A2;
A5: for k being Nat st P[k] holds P[k+1] proof
let k be Nat;
assume P[k];
then reconsider H = MG.k as SimpleGraph;
MG.(k+1) = Mycielskian H by A1,A3;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
registration
let G be SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> SimpleGraph-like;
coherence by Th114;
end;
theorem Th115:
for G, H being SimpleGraph, n be Nat
holds (MycielskianSeq G).(n+1) = Mycielskian (MycielskianSeq G).n
proof
let G, H be SimpleGraph, n be Nat;
set H = (MycielskianSeq G).n;
consider myc being Function such that
A1: MycielskianSeq G = myc and myc.0 = G and
A2: for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G by Def26;
thus (MycielskianSeq G).(n+1) = Mycielskian H by A1,A2;
end;
registration
let G be with_finite_clique# SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> with_finite_clique#;
coherence proof
set MG = MycielskianSeq G;
defpred P[Nat] means MG.$1 is with_finite_clique#;
consider myc being Function such that
A1: MycielskianSeq G = myc and
A2: myc.0 = G and
A3: for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G by Def26;
A4: P[0] by A1,A2;
A5: for k being Nat st P[k] holds P[k+1] proof
let k be Nat;
assume P[k];
then reconsider H = MG.k as with_finite_clique# SimpleGraph;
MG.(k+1) = Mycielskian H by A1,A3;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
end;
registration
let G be finitely_colorable SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> finitely_colorable;
coherence proof
set MG = MycielskianSeq G;
defpred P[Nat] means MG.$1 is finitely_colorable;
consider myc being Function such that
A1: MycielskianSeq G = myc and
A2: myc.0 = G and
A3: for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G by Def26;
A4: P[0] by A1,A2;
A5: for k being Nat st P[k] holds P[k+1] proof
let k be Nat;
assume P[k];
then reconsider H = MG.k as finitely_colorable SimpleGraph;
MG.(k+1) = Mycielskian H by A1,A3;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence thesis;
end;
end;
registration
let G be finite SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> finite;
coherence proof
defpred P[Nat] means (MycielskianSeq G).$1 is finite;
A1: P[0] by Th113;
A2: now let k be Nat;
assume A3: P[k];
set H = (MycielskianSeq G).k;
(MycielskianSeq G).(k+1) = Mycielskian H by Th115;
hence P[k+1] by A3;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
end;
theorem Th116:
for G being finite SimpleGraph, n being Nat
holds order ((MycielskianSeq G).n) = 2|^n*(order G) + 2|^n - 1
proof
let G be finite SimpleGraph, n being Nat;
set g = order G;
set MG = MycielskianSeq G;
defpred P[Nat] means
order ((MG).$1) = 2|^$1*g + 2|^$1 - 1;
A1: P[0] proof
thus order (MG.0)
= g + 1 - 1 by Th113
.= 1*g+2|^0-1 by NEWTON:4
.= 2|^0*g+2|^0-1 by NEWTON:4;
end;
A2: for n being Nat st P[n] holds P[n+1] proof
let n be Nat such that
A3: P[n];
thus order ((MG).(n+1))
= order (Mycielskian ((MG.n))) by Th115
.= 2*(2|^n*g + 2|^n - 1) + 1 by A3,Th89
.= 2*(2|^n)*g + 2*(2|^n) - 2*1 + 1
.= 2|^(n+1)*g + 2*(2|^n) - 2*1 + 1 by NEWTON:6
.= 2|^(n+1)*g + 2|^(n+1) - 2 + 1 by NEWTON:6
.= 2|^(n+1)*g + 2|^(n+1) - 1;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence order ((MG).n) = 2|^n*g + 2|^n - 1;
end;
theorem :: MSnsize:
for G being finite SimpleGraph, n being Nat
holds size (MycielskianSeq G).n
= 3|^n*(size G) + (3|^n - 2|^n)*(order G) + (n+1) block 3
proof
let G be finite SimpleGraph, n being Nat;
set g = order G; set s = size G;
set MG = MycielskianSeq G;
defpred P[Nat] means
size ((MG)).$1 = 3|^$1*s + (3|^$1 - 2|^$1)*g + ($1+1) block 3;
A1: P[0] proof
thus size ((MG).0)
= 1*s + 0*g + 0 by Th113
.= 3|^0*s + (1 - 1)*g + 0 by NEWTON:4
.= 3|^0*s + (3|^0 - 1)*g + 0 by NEWTON:4
.= 3|^0*s + (3|^0 - 2|^0)*g + 0 by NEWTON:4
.= 3|^0*s + (3|^0 - 2|^0)*g + (0+1) block 3 by STIRL2_1:29;
end;
A2: for n being Nat st P[n] holds P[n+1] proof
let n be Nat such that
A3: P[n];
A4: n+1 >= 0+1 by XREAL_1:6;
A5: 1/2*(2|^(n+1) - 2)
= 1/2*(2*2|^n - 2*1) by NEWTON:6
.= 2|^n -1;
thus size ((MG).(n+1))
= size (Mycielskian ((MG.n))) by Th115
.= 3*(3|^n*s + (3|^n - 2|^n)*g + (n+1) block 3) + order (MG.n)
by A3,Th92
.= 3*3|^n*s + 3*(3|^n - 2|^n)*g + 3*((n+1) block 3) + order (MG.n)
.= 3|^(n+1)*s + 3*(3|^n - 2|^n)*g + 3*((n+1) block 3) + order (MG.n)
by NEWTON:6
.= 3|^(n+1)*s + 3*(3|^n - 2|^n)*g + 3*((n+1) block 3) + (2|^n*g + 2|^n -1)
by Th116
.= 3|^(n+1)*s + 3*(3|^n - 2|^n)*g + 2|^n*g + (3*((n+1) block 3) + (2|^n -1))
.= 3|^(n+1)*s + 3*(3|^n - 2|^n)*g + 2|^n*g + ((2+1)*((n+1) block (2+1))
+ ((n+1) block 2)) by A5,A4,STIRL2_1:47
.= 3|^(n+1)*s + (3*3|^n*g - (2*2|^n*g+2|^n*g) + 2|^n*g) + ((n+1)+1) block 3
by STIRL2_1:46
.= 3|^(n+1)*s + (3*3|^n*g - (2|^(n+1)*g+2|^n*g) + 2|^n*g) + ((n+1)+1) block 3
by NEWTON:6
.= 3|^(n+1)*s + (3*3|^n*g - 2|^(n+1)*g - 2|^n*g + 2|^n*g) + ((n+1)+1) block 3
.= 3|^(n+1)*s + (3|^(n+1)*g - 2|^(n+1)*g-2|^n*g+2|^n*g) + ((n+1)+1) block 3
by NEWTON:6
.= 3|^(n+1)*s + (3|^(n+1) - 2|^(n+1))*g + ((n+1)+1) block 3;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence size ((MG).n) = 3|^n*s + (3|^n - 2|^n)*g + (n+1) block 3;
end;
theorem Th118:
for n being Nat
holds clique# ((MycielskianSeq CompleteSGraph 2).n) = 2 &
chromatic# ((MycielskianSeq CompleteSGraph 2).n) = n+2
proof
A1: card 2 = 2;
set P2 = CompleteSGraph 2;
defpred P[Nat] means
clique# ((MycielskianSeq P2).$1) = 2 &
chromatic# ((MycielskianSeq P2).$1) = $1+2;
A2: clique# ((MycielskianSeq P2).0) = clique# P2 by Th113 .= 2 by A1,Th59;
chromatic# ((MycielskianSeq P2).0) = chromatic# P2 by Th113
.= 0+2 by A1,Th69;
then
A3: P[0] by A2;
A4: for n being Nat st P[n] holds P[n+1] proof
let n be Nat;
assume A5: P[n];
thus clique# ((MycielskianSeq P2).(n+1))
= clique# Mycielskian((MycielskianSeq P2).n) by Th115
.= 2 by Th110,A5;
thus chromatic# ((MycielskianSeq P2).(n+1))
= chromatic# Mycielskian((MycielskianSeq P2).n) by Th115
.= 1+(n+2) by A5,Th112
.= (n+1)+2;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem
for n being Nat
ex G being finite SimpleGraph st clique# G = 2 & chromatic# G > n
proof
let n be Nat;
set P2 = CompleteSGraph 2;
reconsider G = (MycielskianSeq P2).n as finite SimpleGraph;
take G;
n+1+1 > n+1 & n+1 > n by NAT_1:13;
then n+2 > n by XXREAL_0:2;
hence thesis by Th118;
end;
theorem
for n being Nat
ex G being finite SimpleGraph st stability# G = 2 & cliquecover# G > n
proof
let n be Nat;
set G = (MycielskianSeq CompleteSGraph 2).n;
n+1+1 > n+1 & n+1 > n by NAT_1:13;
then n+2 > n by XXREAL_0:2;
then A1: clique# G = 2 & chromatic# G > n by Th118;
take S = Complement G;
thus stability# S = 2 by A1,Th76;
thus cliquecover# S > n by A1,Th82;
end;