scmyciel.miz
begin
theorem ::
SCMYCIEL:1
Th1: for x be
object, X be
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 ::
SCMYCIEL:2
Th2: for x,X be
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 ::
SCMYCIEL:3
Th3: for x,X be
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 ::
SCMYCIEL:4
Th4: for x1,y1,x2,y2 be
object, X be
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 ::
SCMYCIEL:5
Th5: for X be
set, v be
object st 3
c= (
card X) holds ex v1,v2 be
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 be
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 be
object st v1
in X & v2
in X & v1
<> v & v2
<> v & v1
<> v2 by
A1,
A2,
A3,
A4,
A5,
A6;
end;
theorem ::
SCMYCIEL:6
Th6: for x be
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 be
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
reconsider f =
<*
{} *> as
FinSequence;
take f;
now
let x be
set;
assume x
in (
rng f);
then x
in
{
{} } by
FINSEQ_1: 39;
hence x is
finite;
end;
hence thesis;
end;
end
theorem ::
SCMYCIEL:7
Th7: for X be non
empty
finite
set, P be
a_partition of X st (
card P)
< (
card X) holds ex p be
set, x,y be
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 be
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 ::
SCMYCIEL:8
Th8: for x be
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 ::
SCMYCIEL:9
Th9: for X be
set, s be
Subset of X st s is 1
-element holds ex x be
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 be
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 ::
SCMYCIEL:10
Th10: for X be
set holds (
card {
{X,
[x, X]} where x be
Element of X : x
in X })
= (
card X)
proof
let X be
set;
set uG = X;
set A = {
{uG,
[x, uG]} where x be
Element of uG : x
in uG };
deffunc
F(
object) =
{uG,
[$1, uG]};
consider f be
Function such that
A1: (
dom f)
= uG and
A2: for x be
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 be
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 be
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;
::
SCMYCIEL:def1
func
PairsOf G ->
Subset of G means
:
Def1: for e be
set holds e
in it iff e
in G & (
card e)
= 2;
existence
proof
defpred
P[
set] means (
card $1)
= 2;
consider X be
Subset of G such that
A1: for x be
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 be
set holds e
in it1 iff e
in G & (
card e)
= 2 and
A3: for e be
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 ::
SCMYCIEL:11
Th11: for X be
set, e be
set st e
in (
PairsOf X) holds ex x,y be
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 be
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 ::
SCMYCIEL:12
Th12: for X be
set, x,y be
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 ::
SCMYCIEL:13
Th13: for X be
set, x,y be
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 be
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 ::
SCMYCIEL:14
Th14: for G,H be
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 ::
SCMYCIEL:15
Th15: for X be
finite
set holds (
card {
{x,
[y, (
union X)]} where x,y be
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 be
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 be
set st $1
=
{a, b} holds $2
=
{
{a,
[b, Y]},
{b,
[a, Y]}};
A3: for x,y1,y2 be
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 be
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 be
object st x
in EG holds ex y be
object st
P[x, y]
proof
let x be
object;
assume x
in EG;
then
consider x1,y1 be
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 be
Function such that
A10: (
dom f)
= EG and
A11: for x be
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 be
object such that
A12: x
in (
dom f) and
A13: y
= (f
. x) by
FUNCT_1:def 3;
consider x1,y1 be
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 be
FinSequence of
NAT such that
A16: (
len L)
= (
len S) and
A17: for j be
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 be
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 be
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 be
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 be
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 be
set such that
A49: a
in YY and
A50: YY
in (
rng S) by
TARSKI:def 4;
consider b be
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 be
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 be
Element of uG such that
A58: a
=
{x,
[y, Y]} and
A59:
{x, y}
in EG;
consider c be
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 ::
SCMYCIEL:16
for X be
finite
set holds (
card {
[x, y] where x,y be
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 be
Element of Y :
{x, y}
in (
PairsOf X) };
set A = {
{x,
[y, Y]} where x,y be
Element of Y :
{x, y}
in (
PairsOf X) };
per cases ;
suppose
A1: B is
empty;
now
assume A is non
empty;
then
consider a be
object such that
A2: a
in A;
consider x,y be
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 be
object such that
A5: b
in B;
consider x,y be
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 be
Element of Y st a
in Y & b
in Y & $1
=
{a,
[b, Y]} holds $2
=
[a, b];
A9: for c be
object st c
in A holds ex d be
object st d
in B &
P[c, d]
proof
let c be
object;
assume c
in A;
then
consider x,y be
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 be
Function of A, B such that
A13: for c be
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 be
Element of Y such that
A19: c1
=
{x1,
[y1, Y]} and
{x1, y1}
in (
PairsOf X) by
A16,
A14;
consider x2,y2 be
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 be
object such that
A24: a
in (
dom f) and
A25: b
= (f
. a) by
FUNCT_1:def 3;
consider x,y be
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 be
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;
::
SCMYCIEL:def2
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 ::
SCMYCIEL:17
Th17: for X be
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 be
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 ::
SCMYCIEL:18
Th18: for X be
set st (
union X)
=
{} holds X
=
{} or X
=
{
{} }
proof
let X be
set such that
A1: (
union X)
=
{} ;
assume X
<>
{} ;
then
consider x be
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;
::
SCMYCIEL:def3
attr X is
pairfree means (
PairsOf X) is
empty;
end
theorem ::
SCMYCIEL:19
Th19: for X,x be
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 be
object such that
A2: e
in (
PairsOf G) by
XBOOLE_0:def 1;
consider x,y be
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 be
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 be
set holds (
union { V where V be
finite
Subset of X : (
card V)
<= 2 })
= X
proof
let X be
set;
set G = { V where V be
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 be
set such that
A1: x
in a and
A2: a
in G by
TARSKI:def 4;
consider V be
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
definition
let n be
Nat;
let X be
set;
::
SCMYCIEL:def4
attr X is n
-at_most_dimensional means
:
Def4: for x be
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 be
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 ::
SCMYCIEL:20
Th20: for G be
subset-closed non
empty
set holds
{}
in G
proof
let G be
subset-closed non
empty
set;
consider z be
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 ::
SCMYCIEL:21
Th21: for n be
Nat, X be n
-at_most_dimensional
set, x be
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;
::
SCMYCIEL:def5
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 ::
SCMYCIEL:22
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
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 ::
SCMYCIEL:23
Th23: for G be
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 ::
SCMYCIEL:24
Th24: for G be
SimpleGraph, x be
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 be
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 ::
SCMYCIEL:25
Th25: for x be
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
let X be
finite
finite-membered
set;
::
SCMYCIEL:def6
func
order X ->
Nat equals (
card (
union X));
coherence ;
end
definition
let X be
finite
set;
::
SCMYCIEL:def7
func
size X ->
Nat equals (
card (
PairsOf X));
coherence ;
end
theorem ::
SCMYCIEL:26
Th26: for G be
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 be
Subset of uG such that
A2: x
= f and
A3: f is 1
-element;
consider a be
set such that
A4: a
in uG and
A5: f
=
{a} by
A3,
Th9;
consider y be
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 ::
SCMYCIEL:27
Th27: for G be
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;
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 be
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 be
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 be
Subset of (
Vertices G) such that
A9: x
= f and
A10: f is 1
-element;
consider v be
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 ::
SCMYCIEL:28
Th28: for G be
SimpleGraph st (
Vertices G)
=
{} holds G is
void by
Th18;
theorem ::
SCMYCIEL:29
Th29: for G be
SimpleGraph, x be
set st x
in G & x
<>
{} holds (ex y be
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 be
Subset of (
Vertices G) such that
A4: x
= f and
A5: f is 1
-element;
consider v be
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 ::
SCMYCIEL:30
for G be
SimpleGraph, x be
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 be
object such that
A3: e
in (
Edges G) by
XBOOLE_0:def 1;
consider x,y be
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 ::
SCMYCIEL:31
Th31: for X be
set holds ex G be
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 be
Subset of X such that
A4: x
= f and
A5: f is 1
-element;
consider v be
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 be
Subset of X such that
A9: x
= f and
A10: f is 1
-element;
consider v be
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 be
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 be
Subset of X such that
A15: e
= f and
A16: f is 1
-element;
consider v be
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 be
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 be
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);
::
SCMYCIEL:def8
func
Adjacent v ->
Subset of (
Vertices G) means
:
Def8: for x be
Element of (
Vertices G) holds x
in it iff
{v, x}
in (
Edges G);
existence
proof
set A = { x where x be
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 be
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 be
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 be
Element of (
Vertices G) holds x
in A1 iff
{v, x}
in (
Edges G) and
A6: for x be
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;
::
SCMYCIEL:def9
mode
SimpleGraph of X ->
SimpleGraph means
:
Def9: (
Vertices it )
= X;
existence
proof
consider G be
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;
::
SCMYCIEL:def10
func
CompleteSGraph X ->
SimpleGraph of X equals { V where V be
finite
Subset of X : (
card V)
<= 2 };
coherence
proof
set G = { V where V be
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 be
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 ::
SCMYCIEL:32
Th32: for G be
SimpleGraph st (for x,y be
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 be
set st x
in (
Vertices G) & y
in (
Vertices G) holds
{x, y}
in G;
set C = { V where V be
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 be
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;
per cases ;
suppose (
card V)
=
0 ;
then V
=
{} ;
hence a
in G by
A2,
Th20;
end;
suppose (
card V)
= 1;
then
consider c be
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 be
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 be
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 ::
SCMYCIEL:33
Th33: for X be
set, x be
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 ::
SCMYCIEL:34
Th34: for X be
set, x,y be
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 ::
SCMYCIEL:35
Th35: (
CompleteSGraph
{} )
=
{
{} }
proof
for x,y be
set st x
in (
union
{
{} }) & y
in (
union
{
{} }) holds
{x, y}
in
{
{} };
hence (
CompleteSGraph
{} )
=
{
{} } by
Th32;
end;
theorem ::
SCMYCIEL:36
Th36: for x be
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 be
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 ::
SCMYCIEL:37
Th37: for x,y be
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 be
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 ::
SCMYCIEL:38
for X,Y be
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 be
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 ::
SCMYCIEL:39
Th39: for G be
SimpleGraph, x be
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 be
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 be
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 be
SimpleGraph holds (
Vertices G)
= (
Vertices ((
CompleteSGraph (
Vertices G))
\ (
Edges G)))
proof
let G be
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 be
SimpleGraph, x,y be
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 be
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 be
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 be
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;
::
SCMYCIEL:def11
func
Complement G ->
SimpleGraph equals ((
CompleteSGraph (
Vertices G))
\ (
Edges G));
correctness by
Lm3;
involutiveness by
Lm6;
end
theorem ::
SCMYCIEL:40
for G be
SimpleGraph holds (
Vertices G)
= (
Vertices (
Complement G)) by
Lm4;
theorem ::
SCMYCIEL:41
for G be
SimpleGraph, x,y be
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
definition
let G be
SimpleGraph, L be
set;
::
SCMYCIEL:def12
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 ::
SCMYCIEL:42
for G be
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 ::
SCMYCIEL:43
Th43: for G be
SimpleGraph, L be
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 ::
SCMYCIEL:44
Th44: for G,H be
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 be
SimpleGraph, L be
set, x be
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 be
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 be
SimpleGraph, L be
set, x be
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 ::
SCMYCIEL:45
Th45: for G be
SimpleGraph, L be
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 be
SimpleGraph, L be
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 be
SimpleGraph, L,x,y be
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 be
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 ::
SCMYCIEL:46
Th46: for G be
SimpleGraph, x be
set st x
in (
Vertices G) holds (G
SubgraphInducedBy
{x})
=
{
{} ,
{x}}
proof
let G be
SimpleGraph, x be
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
definition
let G be
SimpleGraph;
::
SCMYCIEL:def13
attr G is
clique means
:
Def13: G
= (
CompleteSGraph (
Vertices G));
end
theorem ::
SCMYCIEL:47
Th47: for G be
SimpleGraph st for x,y be
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 be
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 ::
SCMYCIEL:48
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 ::
SCMYCIEL:49
Th49: for X be
set holds (
CompleteSGraph X) is
clique by
Lm1;
registration
let X be
set;
cluster (
CompleteSGraph X) ->
clique;
correctness by
Th49;
end
theorem ::
SCMYCIEL:50
Th50: for G be
SimpleGraph, x be
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 ::
SCMYCIEL:51
Th51: for G be
SimpleGraph, x,y be
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 ::
SCMYCIEL:52
Th52: for G be
SimpleGraph, x be
set st x
in (
union G) holds ex C be
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 ::
SCMYCIEL:53
Th53: for C be
clique
SimpleGraph, u,v be
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;
::
SCMYCIEL:def14
attr G is
with_finite_clique# means
:
Def14: ex C be
finite
Clique of G st for D be
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 be
finite
Clique of G st (
order c)
= $1;
A1: for k be
Nat st
P[k] holds k
<= (
card R9)
proof
let k be
Nat;
assume
P[k];
then
consider c be
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 be
Nat st
P[k];
consider k be
Nat such that
A5:
P[k] and
A6: for n be
Nat st
P[n] holds n
<= k from
NAT_1:sch 6(
A1,
A4);
consider c be
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;
::
SCMYCIEL:def15
func
clique# G ->
Nat means
:
Def15: (ex C be
finite
Clique of G st (
order C)
= it ) & for T be
finite
Clique of G holds (
order T)
<= it ;
existence
proof
consider C be
finite
Clique of G such that
A1: for D be
finite
Clique of G holds (
order D)
<= (
order C) by
Def14;
take itt = (
order C);
thus ex A be
finite
Clique of G st (
order A)
= itt;
let T be
finite
Clique of G;
thus (
order T)
<= itt by
A1;
end;
uniqueness
proof
let it1,it2 be
Nat such that
A2: ex C be
finite
Clique of G st (
order C)
= it1 and
A3: for T be
finite
Clique of G holds (
order T)
<= it1 and
A4: ex C be
finite
Clique of G st (
order C)
= it2 and
A5: for T be
finite
Clique of G holds (
order T)
<= it2;
consider C1 be
finite
Clique of G such that
A6: (
order C1)
= it1 by
A2;
consider C2 be
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 ::
SCMYCIEL:54
Th54: for G be
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 be
object such that
A2: v
in (
Vertices G) by
XBOOLE_0:def 1;
consider D be
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 ::
SCMYCIEL:55
for G be
void
SimpleGraph holds (
clique# G)
=
0
proof
let G be
void
SimpleGraph;
assume
A1: (
clique# G)
<>
0 ;
consider C be
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 ::
SCMYCIEL:56
Th56: for G be
SimpleGraph, x,y be
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 ::
SCMYCIEL:57
Th57: for G be
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 be
object such that
A2: e
in (
Edges G) by
A1,
XBOOLE_0:def 1;
consider x,y be
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 ::
SCMYCIEL:58
Th58: for G,H be
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 be
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 ::
SCMYCIEL:59
Th59: for X be
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 be
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);
::
SCMYCIEL:def16
attr P is
Clique-wise means
:
Def16: for x be
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 be
Element of cRp1 by
EQREL_1: 37;
take S;
now
let z be
set;
assume
A2: z
in S;
consider x be
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;
::
SCMYCIEL:def17
attr G is
with_finite_cliquecover# means
:
Def17: ex C be
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 be
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 be
Element of cRp1 :
P[x] } by
EQREL_1: 37;
A4: {
F(x) where x be
Element of cRp1 :
P[x] } is
finite from
PRE_CIRC:sch 1;
now
let z be
set;
assume
A5: z
in S;
consider x be
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 be
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 be
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 be
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;
::
SCMYCIEL:def18
func
cliquecover# G ->
Nat means
:
Def18: (ex C be
finite
Clique-partition of G st (
card C)
= it ) & for C be
finite
Clique-partition of G holds it
<= (
card C);
existence
proof
defpred
P[
Nat] means ex C be
finite
Clique-partition of G st (
card C)
= $1;
consider C be
Clique-partition of G such that
A1: C is
finite by
Def17;
(
card C)
= (
card C);
then
A2: ex k be
Nat st
P[k] by
A1;
consider n be
Nat such that
A3:
P[n] and
A4: for k be
Nat st
P[k] holds n
<= k from
NAT_1:sch 5(
A2);
take n;
thus ex C be
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 be
finite
Clique-partition of G st (
card C)
= it1) and
A6: for C be
finite
Clique-partition of G holds it1
<= (
card C) and
A7: (ex C be
finite
Clique-partition of G st (
card C)
= it2) and
A8: for C be
finite
Clique-partition of G holds it2
<= (
card C);
consider C1 be
finite
Clique-partition of G such that
A9: (
card C1)
= it1 by
A5;
consider C2 be
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
definition
let G be
SimpleGraph, S be
Subset of (
Vertices G);
::
SCMYCIEL:def19
attr S is
stable means
:
Def19: for x,y be
set st x
<> y & x
in S & y
in S holds
{x, y}
nin G;
end
theorem ::
SCMYCIEL:60
for G be
SimpleGraph holds (
{} (
Vertices G)) is
stable;
theorem ::
SCMYCIEL:61
Th61: for G be
SimpleGraph, S be
Subset of (
Vertices G), v be
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 be
object st S
=
{c};
then
consider c be
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);
end
theorem ::
SCMYCIEL:62
Th62: for G be
SimpleGraph, x,y be
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 ::
SCMYCIEL:63
Th63: for G be
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 ::
SCMYCIEL:64
Th64: for G be
SimpleGraph, A be
StableSet of G, B be
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);
::
SCMYCIEL:def20
attr P is
StableSet-wise means
:
Def20: for x be
set st x
in P holds x is
StableSet of G;
end
theorem ::
SCMYCIEL:65
Th65: for G be
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 be
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;
::
SCMYCIEL:def21
attr G is
finitely_colorable means
:
Def21: ex C be
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 ::
SCMYCIEL:66
Th66: for G be
SimpleGraph, S be
Clique of G, L be
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 ::
SCMYCIEL:67
Th67: for G be
SimpleGraph, C be
Coloring of G, S be
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 be
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 be
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;
::
SCMYCIEL:def22
func
chromatic# G ->
Nat means
:
Def22: (ex C be
finite
Coloring of G st (
card C)
= it ) & for C be
finite
Coloring of G holds it
<= (
card C);
existence
proof
defpred
P[
Nat] means ex C be
finite
Coloring of G st (
card C)
= $1;
consider C be
Coloring of G such that
A1: C is
finite by
Def21;
(
card C)
= (
card C);
then
A2: ex k be
Nat st
P[k] by
A1;
consider n be
Nat such that
A3:
P[n] and
A4: for k be
Nat st
P[k] holds n
<= k from
NAT_1:sch 5(
A2);
take n;
thus ex C be
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 be
finite
Coloring of G st (
card C)
= it1 and
A6: for C be
finite
Coloring of G holds it1
<= (
card C) and
A7: ex C be
finite
Coloring of G st (
card C)
= it2 and
A8: for C be
finite
Coloring of G holds it2
<= (
card C);
consider C1 be
finite
Coloring of G such that
A9: (
card C1)
= it1 by
A5;
consider C2 be
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 ::
SCMYCIEL:68
Th68: for G,H be
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 be
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 ::
SCMYCIEL:69
Th69: for X be
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 be
Element of X by
EQREL_1: 37;
then
consider a be
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 be
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 be
set, x,y be
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 ::
SCMYCIEL:70
Th70: for G be
finitely_colorable
SimpleGraph, C be
finite
Coloring of G, c be
set st c
in C & (
card C)
= (
chromatic# G) holds ex v be
Element of (
Vertices G) st v
in c & for d be
Element of C st d
<> c holds ex w be
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 be
object such that
A7: v
in c by
A1,
XBOOLE_0:def 1;
reconsider v as
Element of uG by
A7;
consider d be
Element of C such that
A8: d
<> c and for w be
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 be
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 be
set st A
= $2 & for vv be
Element of uG st $1
= vv holds $2
<> c & $2
in C & for w be
Element of uG holds not (w
in (
Adjacent vv) & w
in A);
A10: for e be
object st e
in c holds ex u be
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 be
Element of C such that
A12: d
<> c and
A13: for w be
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 be
Function such that
A14: (
dom r)
= c and
A15: for e be
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 be
Element of Cc :
P[d] };
consider d be
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 be
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 be
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 be
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 be
Subset of uG st A
in D holds A
<>
{} & for B be
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 be
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 be
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 be
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 be
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 be
Function such that
A65: (
dom s)
= Cc and
A66: for x be
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 be
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 be
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;
::
SCMYCIEL:def23
attr G is
with_finite_stability# means
:
Def23: ex A be
finite
StableSet of G st for B be
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 be
finite
StableSet of R9 st (
card A)
= $1;
A1: for k be
Nat st
P[k] holds k
<= (
card VR) by
NAT_1: 43;
(
{} VR) is
StableSet of R & (
card
{} )
=
0 ;
then
A2: ex k be
Nat st
P[k];
consider k be
Nat such that
A3:
P[k] and
A4: for n be
Nat st
P[n] holds n
<= k from
NAT_1:sch 6(
A1,
A2);
consider S be
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 be
finite
StableSet of G such that
A1: for B be
finite
StableSet of G holds (
card A)
>= (
card B) by
Def23;
given B be
StableSet of G such that
A2: B is
infinite;
consider C be
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;
::
SCMYCIEL:def24
func
stability# G ->
Nat means
:
Def24: (ex A be
finite
StableSet of G st (
card A)
= it ) & for T be
finite
StableSet of G holds (
card T)
<= it ;
existence
proof
consider A be
finite
StableSet of G such that
A1: for B be
finite
StableSet of G holds (
card A)
>= (
card B) by
Def23;
take itt = (
card A);
thus ex A be
finite
StableSet of G st (
card A)
= itt;
let T be
finite
StableSet of G;
thus (
card T)
<= itt by
A1;
end;
uniqueness
proof
let it1,it2 be
Nat such that
A2: ex S1 be
finite
StableSet of G st (
card S1)
= it1 and
A3: for T be
finite
StableSet of G holds (
card T)
<= it1 and
A4: ex S2 be
finite
StableSet of G st (
card S2)
= it2 and
A5: for T be
finite
StableSet of G holds (
card T)
<= it2;
consider S1 be
finite
StableSet of G such that
A6: (
card S1)
= it1 by
A2;
consider S2 be
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 be
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 ::
SCMYCIEL:71
Th71: for G be
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
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 be
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 be
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 be
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 be
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 be
Nat such that
A16: for X be
finite
set, P be
a_partition of (
the_subsets_of_card (2,X)) st (
card X)
>= r & (
card P)
= 2 holds ex S be
Subset of X st (
card S)
>= m & S
is_homogeneous_for P by
RAMSEY_1: 17;
consider Y be
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 be
Element of VR : x
<> y & x
in X & y
in X &
{x, y}
in (
Edges R) };
set B = {
{x, y} where x,y be
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 be
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 be
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 be
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 be
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 be
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 be
Subset of X such that
A42: x
= xx and
A43: (
card xx)
= 2;
consider a,b be
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 be
Subset of E st a
in P holds a
<>
{} & for b be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 ::
SCMYCIEL:72
Th72: for G be
SimpleGraph, C be
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 ::
SCMYCIEL:73
Th73: for G be
SimpleGraph, C be
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 ::
SCMYCIEL:74
Th74: for G be
SimpleGraph, C be
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 ::
SCMYCIEL:75
Th75: for G be
SimpleGraph, C be
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 be
finite
Clique of G such that
A1: for B be
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 be
finite
StableSet of G such that
A1: for B be
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 ::
SCMYCIEL:76
Th76: for G be
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 be
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 ::
SCMYCIEL:77
for G be
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 ::
SCMYCIEL:78
Th78: for G be
SimpleGraph, C be
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 ::
SCMYCIEL:79
Th79: for G be
SimpleGraph, C be
Clique-partition of G holds C is
Coloring of (
Complement G)
proof
let G be
SimpleGraph, C be
Clique-partition of G;
(
Complement (
Complement G))
= G;
hence thesis by
Th78;
end;
theorem ::
SCMYCIEL:80
Th80: for G be
SimpleGraph, C be
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 ::
SCMYCIEL:81
for G be
SimpleGraph, C be
Coloring of (
Complement G) holds C is
Clique-partition of G
proof
let G be
SimpleGraph, C be
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 be
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 be
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 ::
SCMYCIEL:82
Th82: for G be
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 be
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 ::
SCMYCIEL:83
for G be
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
definition
let G be
SimpleGraph;
::
SCMYCIEL:def25
func
Mycielskian G ->
SimpleGraph equals ((((
{
{} }
\/ the set of all
{x} where x be
Element of (((
union G)
\/
[:(
union G),
{(
union G)}:])
\/
{(
union G)}))
\/ (
Edges G))
\/ {
{x,
[y, (
union G)]} where x,y be
Element of (
union G) :
{x, y}
in (
Edges G) })
\/ {
{(
union G),
[x, (
union G)]} where x be
Element of (
union G) : x
in (
Vertices G) });
correctness
proof
set uG = (
union G);
set C = the set of all
{x} where x be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
set A = {
{x,
[y, uG]} where x,y be
Element of uG :
{x, y}
in (
Edges G) };
set B = {
{uG,
[x, uG]} where x be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 ::
SCMYCIEL:84
Th84: for G be
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 be
Subset of uG such that
A2: x
= f and
A3: f is 1
-element;
consider a be
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 be
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 ::
SCMYCIEL:85
Th85: for G be
SimpleGraph, v be
set holds v
in (
Vertices (
Mycielskian G)) iff v
in (
union G) or (ex x be
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 be
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 be
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 be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
then
consider h be
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 be
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 be
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 be
Element of uG :
{x, y}
in (
Edges G) };
then
consider g1,g2 be
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 be
Element of uG : x
in (
Vertices G) };
then
consider x be
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 be
set st x
in (
union G) & v
=
[x, (
union G)]) or v
= (
union G);
A18: for a be
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 be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
A20: the set of all
{x} where x be
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 be
set st x
in (
union G) & v
=
[x, (
union G)]);
then
consider x be
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 ::
SCMYCIEL:86
Th86: for G be
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 be
set st x
in uG & v
=
[x, uG];
then
consider x be
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 be
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 ::
SCMYCIEL:87
Th87: for G be
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 ::
SCMYCIEL:88
Th88: for G be
void
SimpleGraph holds (
Mycielskian G)
=
{
{} ,
{(
union G)}}
proof
let G be
void
SimpleGraph;
set uG = (
union G);
A1: {
{uG,
[x, uG]} where x be
Element of uG : x
in (
Vertices G) }
=
{}
proof
assume not thesis;
then
consider e be
object such that
A2: e
in {
{uG,
[x, uG]} where x be
Element of uG : x
in (
Vertices G) } by
XBOOLE_0:def 1;
consider x be
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 be
Element of uG :
{x, y}
in (
Edges G) }
=
{}
proof
assume not thesis;
then
consider e be
object such that
A5: e
in {
{x,
[y, uG]} where x,y be
Element of uG :
{x, y}
in (
Edges G) } by
XBOOLE_0:def 1;
consider x,y be
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 be
object such that
A8: e
in (
Edges G) by
XBOOLE_0:def 1;
consider x,y be
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 be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG})
=
{
{uG}}
proof
thus the set of all
{x} where x be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG})
c=
{
{uG}}
proof
let a be
object;
assume a
in the set of all
{x} where x be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
then
consider x be
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 be
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 be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
set A = {
{x,
[y, uG]} where x,y be
Element of uG :
{x, y}
in (
Edges G) };
set B = {
{uG,
[x, uG]} where x be
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 be
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 be
Element of uGf, y be
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 be
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 be
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 ::
SCMYCIEL:89
Th89: for G be
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 be
object such that
A3: a
in uG and
A4: a
in
[:uG,
{uG}:] by
XBOOLE_0: 3;
consider x,y be
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 be
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 ::
SCMYCIEL:90
Th90: for G be
SimpleGraph, e be
set holds e
in (
Edges (
Mycielskian G)) iff e
in (
Edges G) or (ex x,y be
Element of (
union G) st e
=
{x,
[y, (
union G)]} &
{x, y}
in (
Edges G)) or (ex y be
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 be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
set A = {
{x,
[y, uG]} where x,y be
Element of uG :
{x, y}
in (
Edges G) };
set B = {
{uG,
[x, uG]} where x be
Element of uG : x
in (
Vertices G) };
hereby
assume
A1: e
in (
Edges (
Mycielskian G));
then
consider x,y be
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 be
Element of uG st e
=
{x,
[y, uG]} &
{x, y}
in (
Edges G)) or (ex y be
Element of uG st e
=
{uG,
[y, uG]} & y
in uG) by
A3,
TARSKI:def 1;
end;
suppose e
in C;
then
consider a be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG}) such that
A4: e
=
{a};
thus e
in (
Edges G) or (ex x,y be
Element of uG st e
=
{x,
[y, uG]} &
{x, y}
in (
Edges G)) or (ex y be
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 be
Element of uG st e
=
{x,
[y, uG]} &
{x, y}
in (
Edges G)) or (ex y be
Element of uG st e
=
{uG,
[y, uG]} & y
in uG);
end;
end;
assume
A5: e
in (
Edges G) or (ex x,y be
Element of uG st e
=
{x,
[y, uG]} &
{x, y}
in (
Edges G)) or (ex y be
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 be
Element of uG st e
=
{x,
[y, uG]} &
{x, y}
in (
Edges G);
then
consider x,y be
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 be
Element of uG st e
=
{uG,
[y, uG]} & y
in uG;
then
consider y be
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 ::
SCMYCIEL:91
Th91: for G be
SimpleGraph holds (
Edges (
Mycielskian G))
= (((
Edges G)
\/ {
{x,
[y, (
union G)]} where x,y be
Element of (
union G) :
{x, y}
in (
Edges G) })
\/ {
{(
union G),
[y, (
union G)]} where y be
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 be
Element of uG :
{x, y}
in (
Edges G) };
set B = {
{uG,
[y, uG]} where y be
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 be
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 be
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 be
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 be
Element of uG such that
A4: e
=
{(
union G),
[y, (
union G)]} & y
in uG;
thus thesis by
A4,
Th90;
end;
end;
end;
theorem ::
SCMYCIEL:92
Th92: for G be
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 be
Element of uG :
{x, y}
in (
Edges G) };
set B = {
{uG,
[y, uG]} where y be
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 be
object such that
A4: e
in (
Edges MG) by
XBOOLE_0:def 1;
consider x,y be
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 be
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 be
Element of uGf, y be
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 be
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 be
object such that
A14: a
in B and
A15: a
in ((
Edges G)
\/ A) by
XBOOLE_0: 3;
consider y be
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 be
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 be
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 be
object such that
A23: a
in A and
A24: a
in (
Edges G) by
XBOOLE_0: 3;
consider xa,ya be
Element of uG such that
A25: a
=
{xa,
[ya, uG]} and
{xa, ya}
in (
Edges G) by
A23;
consider xe,ye be
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 ::
SCMYCIEL:93
Th93: for G be
SimpleGraph, s,t be
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 be
object st y
in (
union G) & t
=
[y, (
union G)]) or (t
in (
union G) or t
= (
union G)) & (ex y be
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 be
Element of uG st
{s, t}
=
{x,
[y, uG]} &
{x, y}
in (
Edges G);
then
consider x,y be
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 be
Element of uG st
{s, t}
=
{uG,
[y, uG]} & y
in uG;
then
consider y be
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 ::
SCMYCIEL:94
Th94: for G be
SimpleGraph, u be
object st
{(
union G), u}
in (
Edges (
Mycielskian G)) holds ex x be
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 be
object st x
in uG & u
=
[x, uG];
end;
suppose (uG
in uG or uG
= uG) & (ex y be
object st y
in uG & u
=
[y, uG]);
hence ex x be
object st x
in uG & u
=
[x, (
union G)];
end;
suppose (u
in uG or u
= uG) & (ex y be
object st y
in uG & uG
=
[y, uG]);
then
consider y be
set such that y
in uG and
A2: uG
=
[y, uG];
thus ex x be
object st x
in uG & u
=
[x, uG] by
A2,
Th2;
end;
end;
theorem ::
SCMYCIEL:95
Th95: for G be
SimpleGraph, u be
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 ::
SCMYCIEL:96
Th96: for G be
SimpleGraph, u be
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 ::
SCMYCIEL:97
Th97: for G be
SimpleGraph, x,y be
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 ::
SCMYCIEL:98
Th98: for G be
SimpleGraph, x,y be
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 ::
SCMYCIEL:99
Th99: for G be
SimpleGraph, x,y be
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 be
Element of uG st e
=
{x,
[y, (
union G)]} &
{x, y}
in (
Edges G);
then
consider xa,ya be
Element of uG such that
A2: e
=
{xa,
[ya, (
union G)]} and
A3:
{xa, ya}
in (
Edges G);
consider xx,yy be
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 be
Element of (
union G) st e
=
{(
union G),
[y, (
union G)]} & y
in (
union G);
then
consider yy be
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 ::
SCMYCIEL:100
Th100: for G be
SimpleGraph, x,y be
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 ::
SCMYCIEL:101
Th101: for G be
SimpleGraph, x,y be
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 be
Element of uG :
{x, y}
in (
Edges G) };
set B = {
{uG,
[y, uG]} where y be
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 be
Subset of (
Vertices MG) such that
A3: f
=
{
[x, uG], y} and
A4: f is 1
-element;
consider s be
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 be
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 be
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 ::
SCMYCIEL:102
Th102: for G be
SimpleGraph, x,y be
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 be
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 be
Element of uG :
{xx, yy}
in (
Edges G) } by
A2;
hence
{
[x, (
union G)], y}
in (
Mycielskian G) by
A1;
end;
theorem ::
SCMYCIEL:103
Th103: for G be
SimpleGraph, x,y be
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 be
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 be
object st y
in (
union G) & s
=
[y, (
union G)]);
then
consider y be
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 ::
SCMYCIEL:104
Th104: for G be
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 be
Element of ((L
\/
[:L,
{L}:])
\/
{L});
then
consider x be
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 be
Element of L :
{x, y}
in (
Edges G) };
then
consider x,y be
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 be
Element of L : x
in (
Vertices G) };
then
consider x be
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 ::
SCMYCIEL:105
Th105: for G be
SimpleGraph, C be
finite
Clique of (
Mycielskian G) st 3
<= (
order C) holds for v be
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 be
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 be
object such that x1
in (
union G) and
A12: v1
=
[x1, (
union G)] by
A2,
A10,
Th94;
consider x2 be
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 ::
SCMYCIEL:106
Th106: for G be
with_finite_clique#
SimpleGraph st (
clique# G)
=
0 holds for D be
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 ::
SCMYCIEL:107
for G be
SimpleGraph, x be
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 be
Element of (((
union G)
\/
[:uG,
{uG}:])
\/
{uG});
set B = {
{x,
[y, uG]} where x,y be
Element of uG :
{x, y}
in (
Edges G) };
set C = {
{uG,
[x, uG]} where x be
Element of uG : x
in (
Vertices G) };
consider aa be
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 be
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 be
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 be
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 ::
SCMYCIEL:108
Th108: for G be
with_finite_clique#
SimpleGraph st (
clique# G)
= 1 holds for D be
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 be
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 be
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 be
Element of (
union G) st e
=
{x,
[y, uG]} &
{x, y}
in (
Edges G);
then
consider x,y be
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 be
Element of (
union G) st e
=
{uG,
[y, uG]} & y
in uG;
then
consider y be
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 ::
SCMYCIEL:109
Th109: for G be
with_finite_clique#
SimpleGraph st 2
<= (
clique# G) holds for D be
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 be
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 be
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 be
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 be
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 be
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 be
object such that x
in (
union G) and
A26: v1
=
[x, (
union G)] by
A25,
A22,
A4,
Th94;
consider y be
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 be
set st x
in (
union G) & v
=
[x, (
union G)];
then
consider x be
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 be
finite
Clique of MG such that
A2: (
Vertices C)
=
{
{} } by
Th52;
take C;
(
order C)
= 1 by
A2,
CARD_1: 30;
hence for D be
finite
Clique of MG holds (
order D)
<= (
order C) by
A1,
Th106;
end;
suppose
A3: (
clique# G)
= 1;
then
consider C be
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 be
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 be
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 be
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 be
finite
Clique of MG holds (
order D)
<= (
order CC) by
A13,
A12,
Th109;
end;
end;
end
theorem ::
SCMYCIEL:110
Th110: for G be
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 be
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 ::
SCMYCIEL:111
Th111: for G be
finitely_colorable
SimpleGraph holds ex E be
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 be
finite
Coloring of G such that
A1: (
card C)
= cnG by
Def22;
defpred
P[
object,
object] means ex A be
set st A
= $1 & $2
= {
[x, uG] where x be
Element of uG : x
in A };
A2: for e be
object st e
in C holds ex u be
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 be
Element of uG : x
in A };
thus
P[e, u];
end;
consider r be
Function such that (
dom r)
= C and
A3: for e be
object st e
in C holds
P[e, (r
. e)] from
CLASSES1:sch 1(
A2);
set D = { (d
\/ (r
. d)) where d be
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 be
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 be
set st A
= $1 & $2
= (A
\/ (r
. $1));
A8: for e be
object st e
in C holds ex u be
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 be
Function such that
A9: (
dom s)
= C and
A10: for e be
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 be
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 be
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 be
Element of uG : xx
in x2 } by
A25;
then
consider xx be
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 be
Element of uG : xx
in x1 } by
A29;
then
consider xx be
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 be
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 be
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 be
Element of uG : yy
in d } by
A39;
then
consider yy be
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 be
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 be
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 be
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 be
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 be
Element of ((uG
\/
[:uG,
{uG}:])
\/
{uG});
then
consider x be
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 be
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 be
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 be
Element of uG :
{x, y}
in (
Edges G) };
then
consider x,y be
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 be
Element of uG : x
in (
Vertices G) };
then
consider x be
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 be
Element of C such that
A74: A
= (d
\/ (r
. d)) and
A75: d
in C;
thus A
<>
{} by
A74,
A75;
thus for B be
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 be
Element of C such that
A77: B
= (e
\/ (r
. e)) and
A78: e
in C;
now
assume A
meets B;
then
consider x be
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 be
Element of uG : yy
in e } by
A81;
then
consider yy be
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 be
Element of uG : yy
in d } by
A83;
then
consider yy be
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 be
Element of uG : yy
in d } by
A85;
then
consider yy be
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 be
Element of uG : zz
in e } by
A85;
then
consider zz be
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 be
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 be
Element of uG : yy
in d } by
A94;
then
consider yy be
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 be
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 be
Element of C such that
A99: B
= (d
\/ (r
. d)) and
A100: d
in C;
now
assume A
meets B;
then
consider x be
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 be
Element of uG : yy
in d } by
A104;
then
consider yy be
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 be
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 be
Element of uG : yy
in d } by
A112;
then
consider yy be
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 be
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 be
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 be
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 be
Element of uG such that
A135: x
=
[x1, uG] and x1
in d by
A133,
A122;
consider y1 be
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 be
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 be
Element of uG : x
in d } by
A140;
then
consider x be
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 be
Coloring of (
Mycielskian G) such that
A1: (
card E)
= (1
+ (
chromatic# G)) by
Th111;
E is
finite by
A1;
hence thesis;
end;
end
theorem ::
SCMYCIEL:112
Th112: for G be
finitely_colorable
SimpleGraph holds (
chromatic# (
Mycielskian G))
= (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);
set cnMG = (
chromatic# MG);
consider D be
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 be
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 be
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 be
Element of (
Vertices G) such that
A17: sev
in se and
A18: for d be
Element of C st d
<> se holds ex w be
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 be
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 be
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;
::
SCMYCIEL:def26
func
MycielskianSeq G ->
ManySortedSet of
NAT means
:
Def26: ex myc be
Function st it
= myc & (myc
.
0 )
= G & for k be
Nat, G be
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 be
SimpleGraph st $2
= G & $3
= (
Mycielskian G)) & ( not $2 is
SimpleGraph implies $3
= $2);
A1: for n be
Nat, x be
set holds ex y be
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 be
set st
P[n, x, y];
end;
suppose not x is
SimpleGraph;
hence thesis;
end;
end;
consider f be
Function such that
A2: (
dom f)
=
NAT and
A3: (f
.
0 )
= G and
A4: for n be
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 be
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 be
Function such that
A6: it1
= myc1 and
A7: (myc1
.
0 )
= G and
A8: for k be
Nat, G be
SimpleGraph st G
= (myc1
. k) holds (myc1
. (k
+ 1))
= (
Mycielskian G);
given myc2 be
Function such that
A9: it2
= myc2 and
A10: (myc2
.
0 )
= G and
A11: for k be
Nat, G be
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 be
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 be
Nat holds
P[k] from
NAT_1:sch 2(
A12,
A13);
for i be
object st i
in
NAT holds (myc1
. i)
= (myc2
. i) by
A15;
hence it1
= it2 by
A6,
A9,
PBOOLE: 3;
end;
end
theorem ::
SCMYCIEL:113
Th113: for G be
SimpleGraph holds ((
MycielskianSeq G)
.
0 )
= G
proof
let G be
SimpleGraph;
consider myc be
Function such that
A1: (
MycielskianSeq G)
= myc and
A2: (myc
.
0 )
= G and for k be
Nat, G be
SimpleGraph st G
= (myc
. k) holds (myc
. (k
+ 1))
= (
Mycielskian G) by
Def26;
thus ((
MycielskianSeq G)
.
0 )
= G by
A1,
A2;
end;
theorem ::
SCMYCIEL:114
Th114: for G be
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 be
Function such that
A1: (
MycielskianSeq G)
= myc and
A2: (myc
.
0 )
= G and
A3: for k be
Nat, G be
SimpleGraph st G
= (myc
. k) holds (myc
. (k
+ 1))
= (
Mycielskian G) by
Def26;
A4:
P[
0 ] by
A1,
A2;
A5: for k be
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 be
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 ::
SCMYCIEL:115
Th115: for G,H be
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 be
Function such that
A1: (
MycielskianSeq G)
= myc and (myc
.
0 )
= G and
A2: for k be
Nat, G be
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 be
Function such that
A1: (
MycielskianSeq G)
= myc and
A2: (myc
.
0 )
= G and
A3: for k be
Nat, G be
SimpleGraph st G
= (myc
. k) holds (myc
. (k
+ 1))
= (
Mycielskian G) by
Def26;
A4:
P[
0 ] by
A1,
A2;
A5: for k be
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 be
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 be
Function such that
A1: (
MycielskianSeq G)
= myc and
A2: (myc
.
0 )
= G and
A3: for k be
Nat, G be
SimpleGraph st G
= (myc
. k) holds (myc
. (k
+ 1))
= (
Mycielskian G) by
Def26;
A4:
P[
0 ] by
A1,
A2;
A5: for k be
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 be
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 be
Nat holds
P[k] from
NAT_1:sch 2(
A1,
A2);
hence thesis;
end;
end
theorem ::
SCMYCIEL:116
Th116: for G be
finite
SimpleGraph, n be
Nat holds (
order ((
MycielskianSeq G)
. n))
= ((((2
|^ n)
* (
order G))
+ (2
|^ n))
- 1)
proof
let G be
finite
SimpleGraph, n be
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 be
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 be
Nat holds
P[n] from
NAT_1:sch 2(
A1,
A2);
hence (
order (MG
. n))
= ((((2
|^ n)
* g)
+ (2
|^ n))
- 1);
end;
theorem ::
SCMYCIEL:117
for G be
finite
SimpleGraph, n be
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 be
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 be
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 be
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 ::
SCMYCIEL:118
Th118: for n be
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 be
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 be
Nat holds
P[n] from
NAT_1:sch 2(
A3,
A4);
hence thesis;
end;
theorem ::
SCMYCIEL:119
for n be
Nat holds ex G be
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 ::
SCMYCIEL:120
for n be
Nat holds ex G be
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;