:: by Piotr Rudnicki and Lorna Stewart

::

:: Received July 2, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

defpred S

theorem Th3: :: MYCIELSK:3

for A, B, C, D, E, X being set st ( X c= A or X c= B or X c= C or X c= D or X c= E ) holds

X c= (((A \/ B) \/ C) \/ D) \/ E

X c= (((A \/ B) \/ C) \/ D) \/ E

proof end;

theorem Th4: :: MYCIELSK:4

for A, B, C, D, E, x being set holds

( x in (((A \/ B) \/ C) \/ D) \/ E iff ( x in A or x in B or x in C or x in D or x in E ) )

( x in (((A \/ B) \/ C) \/ D) \/ E iff ( x in A or x in B or x in C or x in D or x in E ) )

proof end;

theorem Th5: :: MYCIELSK:5

for R being symmetric RelStr

for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds

[y,x] in the InternalRel of R by NECKLACE:def 3, RELAT_2:def 3;

for x, y being set st x in the carrier of R & y in the carrier of R & [x,y] in the InternalRel of R holds

[y,x] in the InternalRel of R by NECKLACE:def 3, RELAT_2:def 3;

definition

let X be set ;

let P be a_partition of X;

let S be Subset of X;

{ (x /\ S) where x is Element of P : x meets S } is a_partition of S

end;
let P be a_partition of X;

let S be Subset of X;

func P | S -> a_partition of S equals :: MYCIELSK:def 1

{ (x /\ S) where x is Element of P : x meets S } ;

coherence { (x /\ S) where x is Element of P : x meets S } ;

{ (x /\ S) where x is Element of P : x meets S } is a_partition of S

proof end;

:: deftheorem defines | MYCIELSK:def 1 :

for X being set

for P being a_partition of X

for S being Subset of X holds P | S = { (x /\ S) where x is Element of P : x meets S } ;

for X being set

for P being a_partition of X

for S being Subset of X holds P | S = { (x /\ S) where x is Element of P : x meets S } ;

registration
end;

registration

let X be set ;

let P be finite a_partition of X;

let S be Subset of X;

coherence

P | S is finite

end;
let P be finite a_partition of X;

let S be Subset of X;

coherence

P | S is finite

proof end;

theorem Th8: :: MYCIELSK:8

for X being set

for P being finite a_partition of X

for S being Subset of X holds card (P | S) <= card P

for P being finite a_partition of X

for S being Subset of X holds card (P | S) <= card P

proof end;

theorem Th9: :: MYCIELSK:9

for X being set

for P being finite a_partition of X

for S being Subset of X holds

( ( for p being set st p in P holds

p meets S ) iff card (P | S) = card P )

for P being finite a_partition of X

for S being Subset of X holds

( ( for p being set st p in P holds

p meets S ) iff card (P | S) = card P )

proof end;

theorem Th10: :: MYCIELSK:10

for R being RelStr

for C being Coloring of R

for S being Subset of R holds C | S is Coloring of (subrelstr S)

for C being Coloring of R

for S being Subset of R holds C | S is Coloring of (subrelstr S)

proof end;

definition

let R be RelStr ;

end;
attr R is with_finite_chromatic# means :Def2: :: MYCIELSK:def 2

ex C being Coloring of R st C is finite ;

ex C being Coloring of R st C is finite ;

:: deftheorem Def2 defines with_finite_chromatic# MYCIELSK:def 2 :

for R being RelStr holds

( R is with_finite_chromatic# iff ex C being Coloring of R st C is finite );

for R being RelStr holds

( R is with_finite_chromatic# iff ex C being Coloring of R st C is finite );

registration

coherence

for b_{1} being RelStr st b_{1} is finite holds

b_{1} is with_finite_chromatic#

end;
for b

b

proof end;

registration

let R be with_finite_chromatic# RelStr ;

existence

ex b_{1} being Coloring of R st b_{1} is finite
by Def2;

end;
existence

ex b

registration

let R be with_finite_chromatic# RelStr ;

let S be Subset of R;

coherence

subrelstr S is with_finite_chromatic#

end;
let S be Subset of R;

coherence

subrelstr S is with_finite_chromatic#

proof end;

definition

let R be with_finite_chromatic# RelStr ;

ex b_{1} being Nat st

( ex C being finite Coloring of R st card C = b_{1} & ( for C being finite Coloring of R holds b_{1} <= card C ) )

for b_{1}, b_{2} being Nat st ex C being finite Coloring of R st card C = b_{1} & ( for C being finite Coloring of R holds b_{1} <= card C ) & ex C being finite Coloring of R st card C = b_{2} & ( for C being finite Coloring of R holds b_{2} <= card C ) holds

b_{1} = b_{2}

end;
func chromatic# R -> Nat means :Def3: :: MYCIELSK:def 3

( ex C being finite Coloring of R st card C = it & ( for C being finite Coloring of R holds it <= card C ) );

existence ( ex C being finite Coloring of R st card C = it & ( for C being finite Coloring of R holds it <= card C ) );

ex b

( ex C being finite Coloring of R st card C = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines chromatic# MYCIELSK:def 3 :

for R being with_finite_chromatic# RelStr

for b_{2} being Nat holds

( b_{2} = chromatic# R iff ( ex C being finite Coloring of R st card C = b_{2} & ( for C being finite Coloring of R holds b_{2} <= card C ) ) );

for R being with_finite_chromatic# RelStr

for b

( b

registration
end;

registration
end;

definition

let R be RelStr ;

end;
attr R is with_finite_cliquecover# means :Def4: :: MYCIELSK:def 4

ex C being Clique-partition of R st C is finite ;

ex C being Clique-partition of R st C is finite ;

:: deftheorem Def4 defines with_finite_cliquecover# MYCIELSK:def 4 :

for R being RelStr holds

( R is with_finite_cliquecover# iff ex C being Clique-partition of R st C is finite );

for R being RelStr holds

( R is with_finite_cliquecover# iff ex C being Clique-partition of R st C is finite );

registration

coherence

for b_{1} being RelStr st b_{1} is finite holds

b_{1} is with_finite_cliquecover#

end;
for b

b

proof end;

registration

let R be with_finite_cliquecover# RelStr ;

existence

ex b_{1} being Clique-partition of R st b_{1} is finite
by Def4;

end;
existence

ex b

registration

let R be with_finite_cliquecover# RelStr ;

let S be Subset of R;

coherence

subrelstr S is with_finite_cliquecover#

end;
let S be Subset of R;

coherence

subrelstr S is with_finite_cliquecover#

proof end;

definition

let R be with_finite_cliquecover# RelStr ;

ex b_{1} being Nat st

( ex C being finite Clique-partition of R st card C = b_{1} & ( for C being finite Clique-partition of R holds b_{1} <= card C ) )

for b_{1}, b_{2} being Nat st ex C being finite Clique-partition of R st card C = b_{1} & ( for C being finite Clique-partition of R holds b_{1} <= card C ) & ex C being finite Clique-partition of R st card C = b_{2} & ( for C being finite Clique-partition of R holds b_{2} <= card C ) holds

b_{1} = b_{2}

end;
func cliquecover# R -> Nat means :Def5: :: MYCIELSK:def 5

( ex C being finite Clique-partition of R st card C = it & ( for C being finite Clique-partition of R holds it <= card C ) );

existence ( ex C being finite Clique-partition of R st card C = it & ( for C being finite Clique-partition of R holds it <= card C ) );

ex b

( ex C being finite Clique-partition of R st card C = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines cliquecover# MYCIELSK:def 5 :

for R being with_finite_cliquecover# RelStr

for b_{2} being Nat holds

( b_{2} = cliquecover# R iff ( ex C being finite Clique-partition of R st card C = b_{2} & ( for C being finite Clique-partition of R holds b_{2} <= card C ) ) );

for R being with_finite_cliquecover# RelStr

for b

( b

registration

let R be non empty with_finite_cliquecover# RelStr ;

coherence

cliquecover# R is positive

end;
coherence

cliquecover# R is positive

proof end;

:: Note: for empty RelStr clique# = 0, stability# = 0, chromatic# = 0,

:: cliquecover# = 0 follows from clusters.

:: cliquecover# = 0 follows from clusters.

theorem :: MYCIELSK:16

for R being with_finite_stability# with_finite_cliquecover# RelStr holds stability# R <= cliquecover# R

proof end;

theorem Th17: :: MYCIELSK:17

for R being RelStr

for x, y being Element of R

for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds

not a <= b

for x, y being Element of R

for a, b being Element of (ComplRelStr R) st x = a & y = b & x <= y holds

not a <= b

proof end;

theorem Th18: :: MYCIELSK:18

for R being RelStr

for x, y being Element of R

for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds

x <= y

for x, y being Element of R

for a, b being Element of (ComplRelStr R) st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds

x <= y

proof end;

registration
end;

registration

let R be symmetric with_finite_stability# RelStr ;

coherence

ComplRelStr R is with_finite_clique#

end;
coherence

ComplRelStr R is with_finite_clique#

proof end;

theorem Th26: :: MYCIELSK:26

for R being symmetric RelStr

for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R

for C being Clique-partition of (ComplRelStr R) holds C is Coloring of R

proof end;

theorem Th27: :: MYCIELSK:27

for R being symmetric RelStr

for C being Clique-partition of R holds C is Coloring of (ComplRelStr R)

for C being Clique-partition of R holds C is Coloring of (ComplRelStr R)

proof end;

registration

let R be with_finite_chromatic# RelStr ;

coherence

ComplRelStr R is with_finite_cliquecover#

end;
coherence

ComplRelStr R is with_finite_cliquecover#

proof end;

registration

let R be symmetric with_finite_cliquecover# RelStr ;

coherence

ComplRelStr R is with_finite_chromatic#

end;
coherence

ComplRelStr R is with_finite_chromatic#

proof end;

theorem Th29: :: MYCIELSK:29

for R being symmetric with_finite_chromatic# RelStr holds chromatic# R = cliquecover# (ComplRelStr R)

proof end;

theorem :: MYCIELSK:30

for R being symmetric with_finite_cliquecover# RelStr holds cliquecover# R = chromatic# (ComplRelStr R)

proof end;

definition

let R be RelStr ;

let v be Element of R;

ex b_{1} being Subset of R st

for x being Element of R holds

( x in b_{1} iff ( x < v or v < x ) )

for b_{1}, b_{2} being Subset of R st ( for x being Element of R holds

( x in b_{1} iff ( x < v or v < x ) ) ) & ( for x being Element of R holds

( x in b_{2} iff ( x < v or v < x ) ) ) holds

b_{1} = b_{2}

end;
let v be Element of R;

func Adjacent v -> Subset of R means :Def6: :: MYCIELSK:def 6

for x being Element of R holds

( x in it iff ( x < v or v < x ) );

existence for x being Element of R holds

( x in it iff ( x < v or v < x ) );

ex b

for x being Element of R holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines Adjacent MYCIELSK:def 6 :

for R being RelStr

for v being Element of R

for b_{3} being Subset of R holds

( b_{3} = Adjacent v iff for x being Element of R holds

( x in b_{3} iff ( x < v or v < x ) ) );

for R being RelStr

for v being Element of R

for b

( b

( x in b

theorem Th31: :: MYCIELSK:31

for R being with_finite_chromatic# RelStr

for C being finite Coloring of R

for c being set st c in C & card C = chromatic# R holds

ex v being Element of R st

( v in c & ( for d being Element of C st d <> c holds

ex w being Element of R st

( w in Adjacent v & w in d ) ) )

for C being finite Coloring of R

for c being set st c in C & card C = chromatic# R holds

ex v being Element of R st

( v in c & ( for d being Element of C st d <> c holds

ex w being Element of R st

( w in Adjacent v & w in d ) ) )

proof end;

definition
end;

:: deftheorem Def7 defines NatRelStr MYCIELSK:def 7 :

for n being Nat

for b_{2} being strict RelStr holds

( b_{2} is NatRelStr of n iff the carrier of b_{2} = n );

for n being Nat

for b

( b

registration
end;

registration

let n be Nat;

coherence

for b_{1} being NatRelStr of n holds b_{1} is finite
by Def7;

existence

ex b_{1} being NatRelStr of n st b_{1} is irreflexive

end;
coherence

for b

existence

ex b

proof end;

definition

let n be Nat;

ex b_{1} being NatRelStr of n st the InternalRel of b_{1} = [:n,n:] \ (id n)

for b_{1}, b_{2} being NatRelStr of n st the InternalRel of b_{1} = [:n,n:] \ (id n) & the InternalRel of b_{2} = [:n,n:] \ (id n) holds

b_{1} = b_{2}

end;
func CompleteRelStr n -> NatRelStr of n means :Def8: :: MYCIELSK:def 8

the InternalRel of it = [:n,n:] \ (id n);

existence the InternalRel of it = [:n,n:] \ (id n);

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines CompleteRelStr MYCIELSK:def 8 :

for n being Nat

for b_{2} being NatRelStr of n holds

( b_{2} = CompleteRelStr n iff the InternalRel of b_{2} = [:n,n:] \ (id n) );

for n being Nat

for b

( b

theorem Th32: :: MYCIELSK:32

for n being Nat

for x, y being set st x in n & y in n holds

( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )

for x, y being set st x in n & y in n holds

( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )

proof end;

registration

let n be Nat;

coherence

( CompleteRelStr n is irreflexive & CompleteRelStr n is symmetric )

end;
coherence

( CompleteRelStr n is irreflexive & CompleteRelStr n is symmetric )

proof end;

definition

let n be Nat;

let R be NatRelStr of n;

ex b_{1} being NatRelStr of (2 * n) + 1 st the InternalRel of b_{1} = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:]

for b_{1}, b_{2} being NatRelStr of (2 * n) + 1 st the InternalRel of b_{1} = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] & the InternalRel of b_{2} = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] holds

b_{1} = b_{2}

end;
let R be NatRelStr of n;

:: Note: no assumptions about R

func Mycielskian R -> NatRelStr of (2 * n) + 1 means :Def9: :: MYCIELSK:def 9

the InternalRel of it = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:];

existence the InternalRel of it = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:];

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines Mycielskian MYCIELSK:def 9 :

for n being Nat

for R being NatRelStr of n

for b_{3} being NatRelStr of (2 * n) + 1 holds

( b_{3} = Mycielskian R iff the InternalRel of b_{3} = ((( the InternalRel of R \/ { [x,(y + n)] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ { [(x + n),y] where x, y is Element of NAT : [x,y] in the InternalRel of R } ) \/ [:{(2 * n)},((2 * n) \ n):]) \/ [:((2 * n) \ n),{(2 * n)}:] );

for n being Nat

for R being NatRelStr of n

for b

( b

theorem Th38: :: MYCIELSK:38

for n being Nat

for R being NatRelStr of n

for x, y being Nat holds

( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )

for R being NatRelStr of n

for x, y being Nat holds

( not [x,y] in the InternalRel of (Mycielskian R) or ( x < n & y < n ) or ( x < n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y < n ) or ( x = 2 * n & n <= y & y < 2 * n ) or ( n <= x & x < 2 * n & y = 2 * n ) )

proof end;

theorem Th39: :: MYCIELSK:39

for n being Nat

for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R)

for R being NatRelStr of n holds the InternalRel of R c= the InternalRel of (Mycielskian R)

proof end;

theorem Th40: :: MYCIELSK:40

for n being Nat

for R being NatRelStr of n

for x, y being set st x in Segm n & y in Segm n & [x,y] in the InternalRel of (Mycielskian R) holds

[x,y] in the InternalRel of R

for R being NatRelStr of n

for x, y being set st x in Segm n & y in Segm n & [x,y] in the InternalRel of (Mycielskian R) holds

[x,y] in the InternalRel of R

proof end;

theorem Th41: :: MYCIELSK:41

for n being Nat

for R being NatRelStr of n

for x, y being Nat st [x,y] in the InternalRel of R holds

( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )

for R being NatRelStr of n

for x, y being Nat st [x,y] in the InternalRel of R holds

( [x,(y + n)] in the InternalRel of (Mycielskian R) & [(x + n),y] in the InternalRel of (Mycielskian R) )

proof end;

theorem Th42: :: MYCIELSK:42

for n being Nat

for R being NatRelStr of n

for x, y being Nat st x in Segm n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds

[x,y] in the InternalRel of R

for R being NatRelStr of n

for x, y being Nat st x in Segm n & [x,(y + n)] in the InternalRel of (Mycielskian R) holds

[x,y] in the InternalRel of R

proof end;

theorem Th43: :: MYCIELSK:43

for n being Nat

for R being NatRelStr of n

for x, y being Nat st y in Segm n & [(x + n),y] in the InternalRel of (Mycielskian R) holds

[x,y] in the InternalRel of R

for R being NatRelStr of n

for x, y being Nat st y in Segm n & [(x + n),y] in the InternalRel of (Mycielskian R) holds

[x,y] in the InternalRel of R

proof end;

theorem Th44: :: MYCIELSK:44

for n being Nat

for R being NatRelStr of n

for m being Nat st n <= m & m < 2 * n holds

( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )

for R being NatRelStr of n

for m being Nat st n <= m & m < 2 * n holds

( [m,(2 * n)] in the InternalRel of (Mycielskian R) & [(2 * n),m] in the InternalRel of (Mycielskian R) )

proof end;

theorem Th45: :: MYCIELSK:45

for n being Nat

for R being NatRelStr of n

for S being Subset of (Mycielskian R) st S = n holds

R = subrelstr S

for R being NatRelStr of n

for S being Subset of (Mycielskian R) st S = n holds

R = subrelstr S

proof end;

theorem Th46: :: MYCIELSK:46

for n being Nat

for R being irreflexive NatRelStr of n st 2 <= clique# R holds

clique# R = clique# (Mycielskian R)

for R being irreflexive NatRelStr of n st 2 <= clique# R holds

clique# R = clique# (Mycielskian R)

proof end;

theorem Th47: :: MYCIELSK:47

for R being with_finite_chromatic# RelStr

for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)

for S being Subset of R holds chromatic# R >= chromatic# (subrelstr S)

proof end;

theorem Th48: :: MYCIELSK:48

for n being Nat

for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)

for R being irreflexive NatRelStr of n holds chromatic# (Mycielskian R) = 1 + (chromatic# R)

proof end;

Lm1: now :: thesis: for myc1, myc2 being Function st dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds

myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds

myc2 . (k + 1) = Mycielskian R ) holds

myc1 = myc2

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds

myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds

myc2 . (k + 1) = Mycielskian R ) holds

myc1 = myc2

let myc1, myc2 be Function; :: thesis: ( dom myc1 = NAT & myc1 . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds

myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds

myc2 . (k + 1) = Mycielskian R ) implies myc1 = myc2 )

assume that

A1: dom myc1 = NAT and

A2: myc1 . 0 = CompleteRelStr 2 and

A3: for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds

myc1 . (k + 1) = Mycielskian R and

A4: dom myc2 = NAT and

A5: myc2 . 0 = CompleteRelStr 2 and

A6: for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds

myc2 . (k + 1) = Mycielskian R ; :: thesis: myc1 = myc2

defpred S_{2}[ Nat] means ( myc1 . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1 & myc1 . $1 = myc2 . $1 );

(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4

.= (2 + 1) -' 1

.= 2 by NAT_D:34 ;

then A7: S_{2}[ 0 ]
by A2, A5;

A8: for k being Nat st S_{2}[k] holds

S_{2}[k + 1]
_{2}[n]
from NAT_1:sch 2(A7, A8);

then for x being object st x in dom myc1 holds

myc1 . x = myc2 . x by A1;

hence myc1 = myc2 by A1, A4; :: thesis: verum

end;
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds

myc1 . (k + 1) = Mycielskian R ) & dom myc2 = NAT & myc2 . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds

myc2 . (k + 1) = Mycielskian R ) implies myc1 = myc2 )

assume that

A1: dom myc1 = NAT and

A2: myc1 . 0 = CompleteRelStr 2 and

A3: for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc1 . k holds

myc1 . (k + 1) = Mycielskian R and

A4: dom myc2 = NAT and

A5: myc2 . 0 = CompleteRelStr 2 and

A6: for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc2 . k holds

myc2 . (k + 1) = Mycielskian R ; :: thesis: myc1 = myc2

defpred S

(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4

.= (2 + 1) -' 1

.= 2 by NAT_D:34 ;

then A7: S

A8: for k being Nat st S

S

proof

for n being Nat holds S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[k + 1] )

assume A9: S_{2}[k]
; :: thesis: S_{2}[k + 1]

reconsider R = myc1 . k as NatRelStr of (3 * (2 |^ k)) -' 1 by A9;

A10: myc1 . (k + 1) = Mycielskian R by A3;

A11: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;

( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;

then 2 |^ k >= 1 by XXREAL_0:2;

then A12: 3 * (2 |^ k) >= 1 by A11, XXREAL_0:2;

then A13: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;

2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;

then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;

then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;

then 3 * (2 |^ (k + 1)) >= 1 by A12, XXREAL_0:2;

then A14: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;

(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A13, XREAL_0:def 2

.= ((3 * (2 * (2 |^ k))) - 2) + 1

.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6

.= (3 * (2 |^ (k + 1))) -' 1 by A14, XREAL_0:def 2 ;

hence S_{2}[k + 1]
by A10, A9, A6; :: thesis: verum

end;
assume A9: S

reconsider R = myc1 . k as NatRelStr of (3 * (2 |^ k)) -' 1 by A9;

A10: myc1 . (k + 1) = Mycielskian R by A3;

A11: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;

( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;

then 2 |^ k >= 1 by XXREAL_0:2;

then A12: 3 * (2 |^ k) >= 1 by A11, XXREAL_0:2;

then A13: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;

2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;

then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;

then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;

then 3 * (2 |^ (k + 1)) >= 1 by A12, XXREAL_0:2;

then A14: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;

(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A13, XREAL_0:def 2

.= ((3 * (2 * (2 |^ k))) - 2) + 1

.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6

.= (3 * (2 |^ (k + 1))) -' 1 by A14, XREAL_0:def 2 ;

hence S

then for x being object st x in dom myc1 holds

myc1 . x = myc2 . x by A1;

hence myc1 = myc2 by A1, A4; :: thesis: verum

definition

let n be Nat;

ex b_{1} being NatRelStr of (3 * (2 |^ n)) -' 1 ex myc being Function st

( b_{1} = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) )

for b_{1}, b_{2} being NatRelStr of (3 * (2 |^ n)) -' 1 st ex myc being Function st

( b_{1} = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) ) & ex myc being Function st

( b_{2} = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) ) holds

b_{1} = b_{2}
by Lm1;

end;
func Mycielskian n -> NatRelStr of (3 * (2 |^ n)) -' 1 means :Def10: :: MYCIELSK:def 10

ex myc being Function st

( it = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) );

existence ex myc being Function st

( it = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) );

ex b

( b

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) )

proof end;

uniqueness for b

( b

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) ) & ex myc being Function st

( b

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) ) holds

b

:: deftheorem Def10 defines Mycielskian MYCIELSK:def 10 :

for n being Nat

for b_{2} being NatRelStr of (3 * (2 |^ n)) -' 1 holds

( b_{2} = Mycielskian n iff ex myc being Function st

( b_{2} = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) ) );

for n being Nat

for b

( b

( b

for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds

myc . (k + 1) = Mycielskian R ) ) );

theorem Th49: :: MYCIELSK:49

( Mycielskian 0 = CompleteRelStr 2 & ( for k being Nat holds Mycielskian (k + 1) = Mycielskian (Mycielskian k) ) )

proof end;

registration
end;

:: article with preliminaries where RelStr represents a graph.

:: But then some stuff from NECKLACE would have to be moved.

:: I decided not to move stuff around until there is much more

:: material and then a bigger reorganisation would be in place

:: 2009.08.06