:: The {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received July 2, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users

defpred S₁[ set ] means verum;

theorem :: MYCIELSK:1

for x, y, z being Real st 0 <= x holds
x * (y -' z) = (x * y) -' (x * z)

proof end;

theorem Th2: :: MYCIELSK:2

for x, y, z being Nat holds
( x in (Segm y) \ (Segm z) iff ( z <= x & x < y ) )

proof end;

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

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 ) )

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;

theorem Th6: :: MYCIELSK:6

for R being symmetric RelStr
for x, y being Element of R st x <= y holds
y <= x

proof end;

theorem Th7: :: MYCIELSK:7

for X being set
for P being a_partition of X holds card P c= card X

proof end;

definition

let X be set ;
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 } is a_partition of S

proof end;

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

registration

let X be set ;

cluster V23() finite V96() for a_partition of X;

existence
ex b₁ being a_partition of X st b₁ is finite

proof end;

end;

registration

let X be set ;
let P be finite a_partition of X;
let S be Subset of X;

cluster P | S -> finite ;

coherence
P | S is finite

proof end;

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

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 )

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)

proof end;

:: This section could be moved to DILWORTH or better yet to some
:: article with preliminaries where RelStr represents a graph.
:: But then some stuff from NECKLACE would have to be moved.
:: I decided not to move stuff around until there is much more
:: material and then a bigger reorganisation would be in place
:: 2009.08.06

definition

let R be RelStr ;

attr R is with_finite_chromatic# means :Def2: :: MYCIELSK:def 2
ex C being Coloring of R st C is finite ;

end;

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

registration

cluster with_finite_chromatic# for RelStr ;

existence
ex b₁ being RelStr st b₁ is with_finite_chromatic#

proof end;

end;

registration

cluster finite -> with_finite_chromatic# for RelStr ;

coherence
for b₁ being RelStr st b₁ is finite holds
b₁ is with_finite_chromatic#

proof end;

end;

registration

let R be with_finite_chromatic# RelStr ;

cluster V23() finite V96() StableSet-wise for a_partition of the carrier of R;

existence
ex b₁ being Coloring of R st b₁ is finite by Def2;

end;

registration

let R be with_finite_chromatic# RelStr ;
let S be Subset of R;

cluster subrelstr S -> with_finite_chromatic# ;

coherence
subrelstr S is with_finite_chromatic#

proof end;

end;

definition

let R be with_finite_chromatic# RelStr ;

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 b₁ being Nat st
( ex C being finite Coloring of R st card C = b₁ & ( for C being finite Coloring of R holds b₁ <= card C ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex C being finite Coloring of R st card C = b₁ & ( for C being finite Coloring of R holds b₁ <= card C ) & ex C being finite Coloring of R st card C = b₂ & ( for C being finite Coloring of R holds b₂ <= card C ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines chromatic# MYCIELSK:def 3 :
for R being with_finite_chromatic# RelStr
for b₂ being Nat holds
( b₂ = chromatic# R iff ( ex C being finite Coloring of R st card C = b₂ & ( for C being finite Coloring of R holds b₂ <= card C ) ) );

registration

let R be empty RelStr ;

cluster chromatic# R -> empty ;

coherence
chromatic# R is empty

proof end;

end;

registration

let R be non empty with_finite_chromatic# RelStr ;

cluster chromatic# R -> positive ;

coherence
chromatic# R is positive

proof end;

end;

definition

let R be RelStr ;

attr R is with_finite_cliquecover# means :Def4: :: MYCIELSK:def 4
ex C being Clique-partition of R st C is finite ;

end;

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

registration

cluster with_finite_cliquecover# for RelStr ;

existence
ex b₁ being RelStr st b₁ is with_finite_cliquecover#

proof end;

end;

registration

cluster finite -> with_finite_cliquecover# for RelStr ;

coherence
for b₁ being RelStr st b₁ is finite holds
b₁ is with_finite_cliquecover#

proof end;

end;

registration

let R be with_finite_cliquecover# RelStr ;

cluster V23() finite V96() Clique-wise for a_partition of the carrier of R;

existence
ex b₁ being Clique-partition of R st b₁ is finite by Def4;

end;

registration

let R be with_finite_cliquecover# RelStr ;
let S be Subset of R;

cluster subrelstr S -> with_finite_cliquecover# ;

coherence
subrelstr S is with_finite_cliquecover#

proof end;

end;

definition

let R be with_finite_cliquecover# RelStr ;

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 b₁ being Nat st
( ex C being finite Clique-partition of R st card C = b₁ & ( for C being finite Clique-partition of R holds b₁ <= card C ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex C being finite Clique-partition of R st card C = b₁ & ( for C being finite Clique-partition of R holds b₁ <= card C ) & ex C being finite Clique-partition of R st card C = b₂ & ( for C being finite Clique-partition of R holds b₂ <= card C ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines cliquecover# MYCIELSK:def 5 :
for R being with_finite_cliquecover# RelStr
for b₂ being Nat holds
( b₂ = cliquecover# R iff ( ex C being finite Clique-partition of R st card C = b₂ & ( for C being finite Clique-partition of R holds b₂ <= card C ) ) );

registration

let R be empty RelStr ;

cluster cliquecover# R -> empty ;

coherence
cliquecover# R is empty

proof end;

end;

registration

let R be non empty with_finite_cliquecover# RelStr ;

cluster cliquecover# R -> positive ;

coherence
cliquecover# R is positive

proof end;

end;

:: Note: for empty RelStr clique# = 0, stability# = 0, chromatic# = 0,
:: cliquecover# = 0 follows from clusters.

theorem Th11: :: MYCIELSK:11

for R being finite RelStr holds clique# R <= card the carrier of R

proof end;

theorem :: MYCIELSK:12

for R being finite RelStr holds stability# R <= card the carrier of R

proof end;

theorem Th13: :: MYCIELSK:13

for R being finite RelStr holds chromatic# R <= card the carrier of R

proof end;

theorem :: MYCIELSK:14

for R being finite RelStr holds cliquecover# R <= card the carrier of R

proof end;

theorem Th15: :: MYCIELSK:15

for R being with_finite_clique# with_finite_chromatic# RelStr holds clique# R <= chromatic# R

proof end;

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

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

proof end;

registration

let R be finite RelStr ;

cluster ComplRelStr R -> finite ;

coherence
ComplRelStr R is finite

proof end;

end;

theorem Th19: :: MYCIELSK:19

for R being symmetric RelStr
for C being Clique of R holds C is StableSet of (ComplRelStr R)

proof end;

theorem Th20: :: MYCIELSK:20

for R being symmetric RelStr
for C being Clique of (ComplRelStr R) holds C is StableSet of R

proof end;

theorem Th21: :: MYCIELSK:21

for R being RelStr
for C being StableSet of R holds C is Clique of (ComplRelStr R)

proof end;

theorem Th22: :: MYCIELSK:22

for R being RelStr
for C being StableSet of (ComplRelStr R) holds C is Clique of R

proof end;

registration

let R be with_finite_clique# RelStr ;

cluster ComplRelStr R -> with_finite_stability# ;

coherence
ComplRelStr R is with_finite_stability#

proof end;

end;

registration

let R be symmetric with_finite_stability# RelStr ;

cluster ComplRelStr R -> with_finite_clique# ;

coherence
ComplRelStr R is with_finite_clique#

proof end;

end;

theorem Th23: :: MYCIELSK:23

for R being symmetric with_finite_clique# RelStr holds clique# R = stability# (ComplRelStr R)

proof end;

theorem :: MYCIELSK:24

for R being symmetric with_finite_stability# RelStr holds stability# R = clique# (ComplRelStr R)

proof end;

theorem Th25: :: MYCIELSK:25

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

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

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)

proof end;

theorem Th28: :: MYCIELSK:28

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

proof end;

registration

let R be with_finite_chromatic# RelStr ;

cluster ComplRelStr R -> with_finite_cliquecover# ;

coherence
ComplRelStr R is with_finite_cliquecover#

proof end;

end;

registration

let R be symmetric with_finite_cliquecover# RelStr ;

cluster ComplRelStr R -> with_finite_chromatic# ;

coherence
ComplRelStr R is with_finite_chromatic#

proof end;

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;

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
ex b₁ being Subset of R st
for x being Element of R holds
( x in b₁ iff ( x < v or v < x ) )

proof end;

uniqueness
for b₁, b₂ being Subset of R st ( for x being Element of R holds
( x in b₁ iff ( x < v or v < x ) ) ) & ( for x being Element of R holds
( x in b₂ iff ( x < v or v < x ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Adjacent MYCIELSK:def 6 :
for R being RelStr
for v being Element of R
for b₃ being Subset of R holds
( b₃ = Adjacent v iff for x being Element of R holds
( x in b₃ iff ( x < v or v < x ) ) );

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 ) ) )

proof end;

definition

let n be Nat;

mode NatRelStr of n -> strict RelStr means :Def7: :: MYCIELSK:def 7
the carrier of it = n;

existence
ex b₁ being strict RelStr st the carrier of b₁ = n

proof end;

end;

:: deftheorem Def7 defines NatRelStr MYCIELSK:def 7 :
for n being Nat
for b₂ being strict RelStr holds
( b₂ is NatRelStr of n iff the carrier of b₂ = n );

registration

cluster -> empty for NatRelStr of 0 ;

coherence
for b₁ being NatRelStr of 0 holds b₁ is empty by Def7;

end;

registration

let n be non zero Nat;

cluster -> non empty for NatRelStr of n;

coherence
for b₁ being NatRelStr of n holds not b₁ is empty by Def7;

end;

registration

let n be Nat;

cluster -> finite for NatRelStr of n;

coherence
for b₁ being NatRelStr of n holds b₁ is finite by Def7;

cluster strict irreflexive for NatRelStr of n;

existence
ex b₁ being NatRelStr of n st b₁ is irreflexive

proof end;

end;

definition

let n be Nat;

func CompleteRelStr n -> NatRelStr of n means :Def8: :: MYCIELSK:def 8
the InternalRel of it = [:n,n:] \ (id n);

existence
ex b₁ being NatRelStr of n st the InternalRel of b₁ = [:n,n:] \ (id n)

proof end;

uniqueness
for b₁, b₂ being NatRelStr of n st the InternalRel of b₁ = [:n,n:] \ (id n) & the InternalRel of b₂ = [:n,n:] \ (id n) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines CompleteRelStr MYCIELSK:def 8 :
for n being Nat
for b₂ being NatRelStr of n holds
( b₂ = CompleteRelStr n iff the InternalRel of b₂ = [:n,n:] \ (id n) );

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 )

proof end;

registration

let n be Nat;

cluster CompleteRelStr n -> symmetric irreflexive ;

coherence
( CompleteRelStr n is irreflexive & CompleteRelStr n is symmetric )

proof end;

end;

registration

let n be Nat;

cluster [#] (CompleteRelStr n) -> clique ;

coherence
[#] (CompleteRelStr n) is connected

proof end;

end;

theorem Th33: :: MYCIELSK:33

for n being Nat holds clique# (CompleteRelStr n) = n

proof end;

theorem :: MYCIELSK:34

for n being non zero Nat holds stability# (CompleteRelStr n) = 1

proof end;

theorem Th35: :: MYCIELSK:35

for n being Nat holds chromatic# (CompleteRelStr n) = n

proof end;

theorem :: MYCIELSK:36

for n being non zero Nat holds cliquecover# (CompleteRelStr n) = 1

proof end;

definition

let n be Nat;
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
ex b₁ being NatRelStr of (2 * n) + 1 st the InternalRel of b₁ = ((( 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)}:]

proof end;

uniqueness
for b₁, b₂ being NatRelStr of (2 * n) + 1 st the InternalRel of b₁ = ((( 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₂ = ((( 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₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Mycielskian MYCIELSK:def 9 :
for n being Nat
for R being NatRelStr of n
for b₃ being NatRelStr of (2 * n) + 1 holds
( b₃ = Mycielskian R iff the InternalRel of b₃ = ((( 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)}:] );

theorem Th37: :: MYCIELSK:37

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

proof end;

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 ) )

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)

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

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) )

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

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

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) )

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

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)

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)

proof end;

theorem Th48: :: MYCIELSK:48

for n being Nat
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

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₂[ 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₂[ 0 ] by A2, A5;
A8: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A9: S₂[k] ; :: thesis: S₂[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₂[k + 1] by A10, A9, A6; :: thesis: verum

end;

for n being Nat holds S₂[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;

definition

let n be Nat;

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 b₁ being NatRelStr of (3 * (2 |^ n)) -' 1 ex myc being Function st
( b₁ = 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 ) )

proof end;

uniqueness
for b₁, b₂ being NatRelStr of (3 * (2 |^ n)) -' 1 st ex myc being Function st
( b₁ = 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₂ = 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₁ = b₂ by Lm1;

end;

:: deftheorem Def10 defines Mycielskian MYCIELSK:def 10 :
for n being Nat
for b₂ being NatRelStr of (3 * (2 |^ n)) -' 1 holds
( b₂ = Mycielskian n iff ex myc being Function st
( b₂ = 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 ) ) );

theorem Th49: :: MYCIELSK:49

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

proof end;

registration

let n be Nat;

cluster Mycielskian n -> irreflexive ;

coherence
Mycielskian n is irreflexive

proof end;

end;

registration

let n be Nat;

cluster Mycielskian n -> symmetric ;

coherence
Mycielskian n is symmetric

proof end;

end;

theorem Th50: :: MYCIELSK:50

for n being Nat holds
( clique# (Mycielskian n) = 2 & chromatic# (Mycielskian n) = n + 2 )

proof end;

theorem :: MYCIELSK:51

for n being Nat ex R being finite RelStr st
( clique# R = 2 & chromatic# R > n )

proof end;

theorem :: MYCIELSK:52

for n being Nat ex R being finite RelStr st
( stability# R = 2 & cliquecover# R > n )

proof end;