:: Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received February 8, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users


:: Could not find in MML
theorem Th1: :: SCMYCIEL:1
for x being object
for X being set holds not [x,X] in X
proof end;

theorem Th2: :: SCMYCIEL:2
for x, X being object holds [x,X] <> X
proof end;

theorem Th3: :: SCMYCIEL:3
for x, X being object holds [x,X] <> x
proof end;

theorem Th4: :: SCMYCIEL:4
for x1, y1, x2, y2 being object
for X being set st x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]} holds
( x1 = x2 & y1 = y2 )
proof end;

theorem Th5: :: SCMYCIEL:5
for X being set
for v being object st 3 c= card X holds
ex v1, v2 being object st
( v1 in X & v2 in X & v1 <> v & v2 <> v & v1 <> v2 )
proof end;

theorem Th6: :: SCMYCIEL:6
for x being set holds singletons {x} = {{x}}
proof end;

registration
cluster Relation-like NAT -defined Function-like finite V40() FinSequence-like FinSubsequence-like for set ;
existence
not for b1 being FinSequence holds b1 is V40()
proof end;
end;

theorem Th7: :: SCMYCIEL:7
for X being non empty finite set
for P being a_partition of X st card P < card X holds
ex p being set ex x, y being object st
( p in P & x in p & y in p & x <> y )
proof end;

registration
cluster Vertices {{}} -> empty ;
correctness
coherence
union {{}} is empty ;
;
end;

theorem Th8: :: SCMYCIEL:8
for x being set holds union {{},{x}} = {x}
proof end;

theorem Th9: :: SCMYCIEL:9
for X being set
for s being Subset of X st s is 1 -element holds
ex x being set st
( x in X & s = {x} )
proof end;

theorem Th10: :: SCMYCIEL:10
for X being set holds card { {X,[x,X]} where x is Element of X : x in X } = card X
proof end;

definition
let G be set ;
func PairsOf G -> Subset of G means :Def1: :: SCMYCIEL:def 1
 for e being set holds
( e in it iff ( e in G & card e = 2 ) );
existence
ex b1 being Subset of G st
for e being set holds
( e in b1 iff ( e in G & card e = 2 ) )
proof end;
uniqueness
for b1, b2 being Subset of G st ( for e being set holds
( e in b1 iff ( e in G & card e = 2 ) ) ) & ( for e being set holds
( e in b2 iff ( e in G & card e = 2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines PairsOf SCMYCIEL:def 1 :
for G being set
for b2 being Subset of G holds
( b2 = PairsOf G iff for e being set holds
( e in b2 iff ( e in G & card e = 2 ) ) );

theorem Th11: :: SCMYCIEL:11
for X, e being set st e in PairsOf X holds
ex x, y being set st
( x <> y & x in union X & y in union X & e = {x,y} )
proof end;

theorem Th12: :: SCMYCIEL:12
for X being set
for x, y being object st x <> y & {x,y} in X holds
{x,y} in PairsOf X
proof end;

theorem Th13: :: SCMYCIEL:13
for X being set
for x, y being object st {x,y} in PairsOf X holds
( x <> y & x in union X & y in union X )
proof end;

theorem Th14: :: SCMYCIEL:14
for G, H being set st G c= H holds
PairsOf G c= PairsOf H
proof end;

theorem Th15: :: SCMYCIEL:15
for X being finite set holds card { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))
proof end;

theorem :: SCMYCIEL:16
for X being finite set holds card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))
proof end;

registration
let X be finite set ;
cluster PairsOf X -> finite ;
coherence
PairsOf X is finite ;
end;

definition
let X be set ;
attr X is void means :Def2: :: SCMYCIEL:def 2
X = {{}};
end;

:: deftheorem Def2 defines void SCMYCIEL:def 2 :
for X being set holds
( X is void iff X = {{}} );

registration
cluster void for set ;
existence
ex b1 being set st b1 is void by Def2;
end;

registration
cluster void -> finite for set ;
coherence
for b1 being set st b1 is void holds
b1 is finite ;
end;

registration
let G be void set ;
cluster Vertices G -> empty ;
coherence
union G is empty
proof end;
end;

theorem Th17: :: SCMYCIEL:17
for X being set st X is void holds
PairsOf X = {}
proof end;

theorem Th18: :: SCMYCIEL:18
for X being set holds
( not union X = {} or X = {} or X = {{}} )
proof end;

definition
let X be set ;
attr X is pairfree means :: SCMYCIEL:def 3
 PairsOf X is empty ;
end;

:: deftheorem defines pairfree SCMYCIEL:def 3 :
for X being set holds
( X is pairfree iff PairsOf X is empty );

theorem Th19: :: SCMYCIEL:19
for X, x being set st card (union X) = 1 holds
X is pairfree
proof end;

Lm1: for X being set holds union { V where V is finite Subset of X : card V <= 2 } = X
proof end;

registration
cluster non empty finite-membered for set ;
existence
ex b1 being set st
( b1 is finite-membered & not b1 is empty )
proof end;
end;

registration
let X be finite-membered set ;
let Y be set ;
cluster X /\ Y -> finite-membered ;
coherence
X /\ Y is finite-membered
proof end;
cluster X \ Y -> finite-membered ;
coherence
X \ Y is finite-membered ;
end;

definition
let n be Nat;
let X be set ;
attr X is n -at_most_dimensional means :Def4: :: SCMYCIEL:def 4
 for x being set st x in X holds
card x c= n + 1;
end;

:: deftheorem Def4 defines -at_most_dimensional SCMYCIEL:def 4 :
for n being Nat
for X being set holds
( X is n -at_most_dimensional iff for x being set st x in X holds
card x c= n + 1 );

registration
let n be Nat;
cluster n -at_most_dimensional -> finite-membered for set ;
correctness
coherence
for b1 being set st b1 is n -at_most_dimensional holds
b1 is finite-membered ;
proof end;
end;

Lm2: for n being Nat holds {{}} is n -at_most_dimensional
proof end;

registration
let n be Nat;
cluster non empty subset-closed n -at_most_dimensional for set ;
existence
ex b1 being set st
( b1 is n -at_most_dimensional & b1 is subset-closed & not b1 is empty )
proof end;
end;

theorem Th20: :: SCMYCIEL:20
for G being non empty subset-closed set holds {} in G
proof end;

theorem Th21: :: SCMYCIEL:21
for n being Nat
for X being b1 -at_most_dimensional set
for x being Element of X st x in X holds
card x <= n + 1
proof end;

registration
let n be Nat;
let X, Y be n -at_most_dimensional set ;
cluster X \/ Y -> n -at_most_dimensional ;
coherence
X \/ Y is n -at_most_dimensional
proof end;
end;

registration
let n be Nat;
let X be n -at_most_dimensional set ;
let Y be set ;
cluster X /\ Y -> n -at_most_dimensional ;
coherence
X /\ Y is n -at_most_dimensional
proof end;
cluster X \ Y -> n -at_most_dimensional ;
coherence
X \ Y is n -at_most_dimensional by Def4;
end;

registration
let n be Nat;
let X be n -at_most_dimensional set ;
cluster -> n -at_most_dimensional for Element of bool X;
correctness
coherence
for b1 being Subset of X holds b1 is n -at_most_dimensional ;
by Def4;
end;

definition
let s be set ;
attr s is SimpleGraph-like means :: SCMYCIEL:def 5
( s is 1 -at_most_dimensional & s is subset-closed & not s is empty );
end;

:: deftheorem defines SimpleGraph-like SCMYCIEL:def 5 :
for s being set holds
( s is SimpleGraph-like iff ( s is 1 -at_most_dimensional & s is subset-closed & not s is empty ) );

registration
cluster SimpleGraph-like -> non empty subset-closed 1 -at_most_dimensional for set ;
correctness
coherence
for b1 being set st b1 is SimpleGraph-like holds
( b1 is 1 -at_most_dimensional & b1 is subset-closed & not b1 is empty );
;
cluster non empty subset-closed 1 -at_most_dimensional -> SimpleGraph-like for set ;
correctness
coherence
for b1 being set st b1 is 1 -at_most_dimensional & b1 is subset-closed & not b1 is empty holds
b1 is SimpleGraph-like ;
;
end;

theorem Th22: :: SCMYCIEL:22
{{}} is SimpleGraph-like by Lm2;

registration
cluster {{}} -> SimpleGraph-like ;
correctness
coherence
{{}} is SimpleGraph-like ;
by Th22;
end;

registration
cluster SimpleGraph-like for set ;
existence
ex b1 being set st b1 is SimpleGraph-like by Th22;
end;

definition
mode SimpleGraph is SimpleGraph-like set ;
end;

registration
cluster non empty V38() finite-membered V243() V278() subset-closed void 1 -at_most_dimensional SimpleGraph-like for set ;
existence
ex b1 being SimpleGraph st b1 is void
proof end;
cluster non empty V38() finite finite-membered V243() V278() subset-closed 1 -at_most_dimensional SimpleGraph-like for set ;
existence
ex b1 being SimpleGraph st b1 is finite 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 edgeless X for pairfree ;
end;

theorem Th23: :: SCMYCIEL:23
for G being SimpleGraph st Vertices G is finite holds
G is finite
proof end;

theorem Th24: :: SCMYCIEL:24
for G being SimpleGraph
for x being object holds
( x in Vertices G iff {x} in G )
proof end;

theorem Th25: :: SCMYCIEL:25
for x being set holds {{},{x}} is SimpleGraph
proof end;

definition
let X be finite finite-membered set ;
func order X -> Nat equals :: SCMYCIEL:def 6
 card (union X);
coherence
card (union X) is Nat ;
end;

:: deftheorem defines order SCMYCIEL:def 6 :
for X being finite finite-membered set holds order X = card (union X);

definition
let X be finite set ;
func size X -> Nat equals :: SCMYCIEL:def 7
 card (PairsOf X);
coherence
card (PairsOf X) is Nat ;
end;

:: deftheorem defines size SCMYCIEL:def 7 :
for X being finite set holds size X = card (PairsOf X);

theorem Th26: :: SCMYCIEL:26
for G being finite SimpleGraph holds order G <= card G
proof end;

definition
let G be SimpleGraph;
mode Vertex of G is Element of Vertices G;
mode Edge of G is Element of Edges G;
end;

theorem Th27: :: SCMYCIEL:27
for G being SimpleGraph holds G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G)
proof end;

theorem Th28: :: SCMYCIEL:28
for G being SimpleGraph st Vertices G = {} holds
G is void by Th18;

theorem Th29: :: SCMYCIEL:29
for G being SimpleGraph
for x being set st x in G & x <> {} & ( for y being set holds
( not x = {y} or not y in Vertices G ) ) holds
x in Edges G
proof end;

theorem :: SCMYCIEL:30
for G being SimpleGraph
for x being set st Vertices G = {x} holds
G = {{},{x}}
proof end;

theorem Th31: :: SCMYCIEL:31
for X being set ex G being SimpleGraph st
( G is edgeless & Vertices G = X )
proof end;

definition
let G be SimpleGraph;
let v be Element of Vertices G;
func Adjacent v -> Subset of (Vertices G) means :Def8: :: SCMYCIEL:def 8
 for x being Element of Vertices G holds
( x in it iff {v,x} in Edges G );
existence
ex b1 being Subset of (Vertices G) st
for x being Element of Vertices G holds
( x in b1 iff {v,x} in Edges G )
proof end;
uniqueness
for b1, b2 being Subset of (Vertices G) st ( for x being Element of Vertices G holds
( x in b1 iff {v,x} in Edges G ) ) & ( for x being Element of Vertices G holds
( x in b2 iff {v,x} in Edges G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Adjacent SCMYCIEL:def 8 :
for G being SimpleGraph
for v being Element of Vertices G
for b3 being Subset of (Vertices G) holds
( b3 = Adjacent v iff for x being Element of Vertices G holds
( x in b3 iff {v,x} in Edges G ) );

definition
let X be set ;
mode SimpleGraph of X -> SimpleGraph means :Def9: :: SCMYCIEL:def 9
 Vertices it = X;
existence
ex b1 being SimpleGraph st Vertices b1 = X
proof end;
end;

:: deftheorem Def9 defines SimpleGraph SCMYCIEL:def 9 :
for X being set
for b2 being SimpleGraph holds
( b2 is SimpleGraph of X iff Vertices b2 = X );

definition
let X be set ;
func CompleteSGraph X -> SimpleGraph of X equals :: SCMYCIEL:def 10
 { V where V is finite Subset of X : card V <= 2 } ;
coherence
{ V where V is finite Subset of X : card V <= 2 } is SimpleGraph of X
proof end;
end;

:: deftheorem defines CompleteSGraph SCMYCIEL:def 10 :
for X being set holds CompleteSGraph X = { V where V is finite Subset of X : card V <= 2 } ;

theorem Th32: :: SCMYCIEL:32
for G being SimpleGraph st ( for x, y being set st x in Vertices G & y in Vertices G holds
{x,y} in G ) holds
G = CompleteSGraph (Vertices G)
proof end;

registration
let X be finite set ;
cluster CompleteSGraph X -> finite ;
correctness
coherence
CompleteSGraph X is finite ;
proof end;
end;

theorem Th33: :: SCMYCIEL:33
for X, x being set st x in X holds
{x} in CompleteSGraph X
proof end;

theorem Th34: :: SCMYCIEL:34
for X, x, y being set st x in X & y in X holds
{x,y} in CompleteSGraph X
proof end;

theorem Th35: :: SCMYCIEL:35
CompleteSGraph {} = {{}}
proof end;

theorem Th36: :: SCMYCIEL:36
for x being set holds CompleteSGraph {x} = {{},{x}}
proof end;

theorem Th37: :: SCMYCIEL:37
for x, y being set holds CompleteSGraph {x,y} = {{},{x},{y},{x,y}}
proof end;

theorem :: SCMYCIEL:38
for X, Y being set st X c= Y holds
CompleteSGraph X c= CompleteSGraph Y
proof end;

theorem Th39: :: SCMYCIEL:39
for G being SimpleGraph
for x being set st x in Vertices G holds
CompleteSGraph {x} c= G
proof end;

registration
let G be SimpleGraph;
cluster finite-membered 1 -at_most_dimensional SimpleGraph-like for Element of bool G;
existence
ex b1 being Subset of G st b1 is SimpleGraph-like
proof end;
end;

definition
let G be SimpleGraph;
mode Subgraph of G is SimpleGraph-like Subset of G;
end;

Lm3: for G being SimpleGraph holds (CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph
proof end;

Lm4: for G being SimpleGraph holds Vertices G = Vertices ((CompleteSGraph (Vertices G)) \ (Edges G))
proof end;

Lm5: for G being SimpleGraph
for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges ((CompleteSGraph (Vertices G)) \ (Edges G)) )
proof end;

Lm6: for G, CG being SimpleGraph st CG = (CompleteSGraph (Vertices G)) \ (Edges G) holds
(CompleteSGraph (Vertices CG)) \ (Edges CG) = G
proof end;

definition
let G be SimpleGraph;
func Complement G -> SimpleGraph equals :: SCMYCIEL:def 11
(CompleteSGraph (Vertices G)) \ (Edges G);
correctness
coherence
(CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph;
by Lm3;
involutiveness
for b1, b2 being SimpleGraph st b1 = (CompleteSGraph (Vertices b2)) \ (Edges b2) holds
b2 = (CompleteSGraph (Vertices b1)) \ (Edges b1) by Lm6;
end;

:: deftheorem defines Complement SCMYCIEL:def 11 :
for G being SimpleGraph holds Complement G = (CompleteSGraph (Vertices G)) \ (Edges G);

theorem :: SCMYCIEL:40
for G being SimpleGraph holds Vertices G = Vertices (Complement G) by Lm4;

theorem :: SCMYCIEL:41
for G being SimpleGraph
for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
( {x,y} in Edges G iff {x,y} nin Edges (Complement G) ) by Lm5;

definition
let G be SimpleGraph;
let L be set ;
func G SubgraphInducedBy L -> Subset of G equals :: SCMYCIEL:def 12
G /\ (bool L);
coherence
G /\ (bool L) is Subset of G by XBOOLE_1:17;
end;

:: deftheorem defines SubgraphInducedBy SCMYCIEL:def 12 :
for G being SimpleGraph
for L being set holds G SubgraphInducedBy L = G /\ (bool L);

registration
let G be SimpleGraph;
let L be set ;
cluster G SubgraphInducedBy L -> SimpleGraph-like ;
coherence
G SubgraphInducedBy L is SimpleGraph-like
proof end;
end;

theorem :: SCMYCIEL:42
for G being SimpleGraph holds G = G SubgraphInducedBy (Vertices G)
proof end;

theorem Th43: :: SCMYCIEL:43
for G being SimpleGraph
for L being set holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ (Vertices G))
proof end;

registration
let G be finite SimpleGraph;
let L be set ;
cluster G SubgraphInducedBy L -> finite ;
coherence
G SubgraphInducedBy L is finite ;
end;

registration
let G be SimpleGraph;
let L be finite set ;
cluster G SubgraphInducedBy L -> finite ;
coherence
G SubgraphInducedBy L is finite ;
end;

theorem Th44: :: SCMYCIEL:44
for G, H being SimpleGraph st G c= H holds
G c= H SubgraphInducedBy (Vertices G)
proof end;

Lm7: for G being SimpleGraph
for L, x being set st x in Vertices (G SubgraphInducedBy L) holds
x in L
proof end;

Lm8: for G being SimpleGraph
for L, x being set st x in L & x in Vertices G holds
x in Vertices (G SubgraphInducedBy L)
proof end;

theorem Th45: :: SCMYCIEL:45
for G being SimpleGraph
for L being set holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L
proof end;

Lm9: for G being SimpleGraph
for L being set st L c= Vertices G holds
Vertices (G SubgraphInducedBy L) = L
proof end;

Lm10: for G being SimpleGraph
for L, x, y being set st x in L & y in L & {x,y} in G holds
{x,y} in G SubgraphInducedBy L
proof end;

theorem Th46: :: SCMYCIEL:46
for G being SimpleGraph
for x being set st x in Vertices G holds
G SubgraphInducedBy {x} = {{},{x}}
proof end;

definition
let G be SimpleGraph;
attr G is clique means :Def13: :: SCMYCIEL:def 13
G = CompleteSGraph (Vertices G);
end;

:: deftheorem Def13 defines clique SCMYCIEL:def 13 :
for G being SimpleGraph holds
( G is clique iff G = CompleteSGraph (Vertices G) );

theorem Th47: :: SCMYCIEL:47
for G being SimpleGraph st ( for x, y being set st x <> y & x in Vertices G & y in Vertices G holds
{x,y} in Edges G ) holds
G is clique
proof end;

theorem Th48: :: SCMYCIEL:48
{{}} is clique by Th35;

registration
cluster non empty V38() finite-membered V243() V278() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for set ;
existence
ex b1 being SimpleGraph st b1 is clique by Th48;
let G be SimpleGraph;
cluster non empty V38() finite-membered V243() V278() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for Element of bool G;
existence
ex b1 being Subgraph of G st b1 is clique
proof end;
end;

definition
let G be SimpleGraph;
mode Clique of G is clique Subgraph of G;
end;

theorem Th49: :: SCMYCIEL:49
for X being set holds CompleteSGraph X is clique by Lm1;

registration
let X be set ;
cluster CompleteSGraph X -> clique ;
correctness
coherence
CompleteSGraph X is clique ;
by Th49;
end;

theorem Th50: :: SCMYCIEL:50
for G being SimpleGraph
for x being set st x in Vertices G holds
{{},{x}} is Clique of G
proof end;

theorem Th51: :: SCMYCIEL:51
for G being SimpleGraph
for x, y being set st x in Vertices G & y in Vertices G & {x,y} in G holds
{{},{x},{y},{x,y}} is Clique of G
proof end;

registration
let G be SimpleGraph;
cluster non empty V38() finite finite-membered V243() V278() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for Element of bool G;
existence
ex b1 being Clique of G st b1 is finite
proof end;
end;

theorem Th52: :: SCMYCIEL:52
for G being SimpleGraph
for x being set st x in union G holds
ex C being finite Clique of G st Vertices C = {x}
proof end;

theorem Th53: :: SCMYCIEL:53
for C being clique SimpleGraph
for u, v being set st u in Vertices C & v in Vertices C holds
{u,v} in C
proof end;

definition
let G be SimpleGraph;
attr G is with_finite_clique# means :Def14: :: SCMYCIEL:def 14
 ex C being finite Clique of G st
for D being finite Clique of G holds order D <= order C;
end;

:: deftheorem Def14 defines with_finite_clique# SCMYCIEL:def 14 :
for G being SimpleGraph holds
( G is with_finite_clique# iff ex C being finite Clique of G st
for D being finite Clique of G holds order D <= order C );

registration
cluster non empty V38() finite-membered V243() V278() subset-closed 1 -at_most_dimensional SimpleGraph-like with_finite_clique# for set ;
existence
ex b1 being SimpleGraph st b1 is with_finite_clique#
proof end;
end;

registration
cluster finite SimpleGraph-like -> with_finite_clique# for set ;
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is with_finite_clique#
proof end;
end;

definition
let G be with_finite_clique# SimpleGraph;
func clique# G -> Nat means :Def15: :: SCMYCIEL:def 15
( ex C being finite Clique of G st order C = it & ( for T being finite Clique of G holds order T <= it ) );
existence
ex b1 being Nat st
( ex C being finite Clique of G st order C = b1 & ( for T being finite Clique of G holds order T <= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex C being finite Clique of G st order C = b1 & ( for T being finite Clique of G holds order T <= b1 ) & ex C being finite Clique of G st order C = b2 & ( for T being finite Clique of G holds order T <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines clique# SCMYCIEL:def 15 :
for G being with_finite_clique# SimpleGraph
for b2 being Nat holds
( b2 = clique# G iff ( ex C being finite Clique of G st order C = b2 & ( for T being finite Clique of G holds order T <= b2 ) ) );

theorem Th54: :: SCMYCIEL:54
for G being with_finite_clique# SimpleGraph st clique# G = 0 holds
Vertices G = {}
proof end;

theorem :: SCMYCIEL:55
for G being void SimpleGraph holds clique# G = 0
proof end;

theorem Th56: :: SCMYCIEL:56
for G being SimpleGraph
for x, y being set st {x,y} in G holds
G SubgraphInducedBy {x,y} is Clique of G
proof end;

theorem Th57: :: SCMYCIEL:57
for G being with_finite_clique# SimpleGraph st Edges G <> {} holds
clique# G >= 2
proof end;

theorem Th58: :: SCMYCIEL:58
for G, H being with_finite_clique# SimpleGraph st G c= H holds
clique# G <= clique# H
proof end;

theorem Th59: :: SCMYCIEL:59
for X being finite set holds clique# (CompleteSGraph X) = card X
proof end;

definition
let G be SimpleGraph;
let P be a_partition of Vertices G;
attr P is Clique-wise means :Def16: :: SCMYCIEL:def 16
 for x being set st x in P holds
G SubgraphInducedBy x is Clique of G;
end;

:: deftheorem Def16 defines Clique-wise SCMYCIEL:def 16 :
for G being SimpleGraph
for P being a_partition of Vertices G holds
( P is Clique-wise iff for x being set st x in P holds
G SubgraphInducedBy x is Clique of G );

registration
let G be SimpleGraph;
cluster V38() V278() Clique-wise for a_partition of Vertices G;
correctness
existence
ex b1 being a_partition of Vertices G st b1 is Clique-wise ;
proof 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
coherence
for b1 being a_partition of Vertices G st b1 is empty holds
b1 is Clique-wise ;
;
end;

definition
let G be SimpleGraph;
attr G is with_finite_cliquecover# means :Def17: :: SCMYCIEL:def 17
 ex C being Clique-partition of G st C is finite ;
end;

:: deftheorem Def17 defines with_finite_cliquecover# SCMYCIEL:def 17 :
for G being SimpleGraph holds
( G is with_finite_cliquecover# iff ex C being Clique-partition of G st C is finite );

registration
cluster finite SimpleGraph-like -> with_finite_cliquecover# for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is with_finite_cliquecover# ;
proof end;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
cluster V38() finite V278() Clique-wise for a_partition of Vertices G;
correctness
existence
ex b1 being Clique-partition of G st b1 is finite ;
by Def17;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
let S be Subset of (Vertices G);
cluster G SubgraphInducedBy S -> with_finite_cliquecover# ;
correctness
coherence
G SubgraphInducedBy S is with_finite_cliquecover# ;
proof end;
end;

definition
let G be with_finite_cliquecover# SimpleGraph;
func cliquecover# G -> Nat means :Def18: :: SCMYCIEL:def 18
( ex C being finite Clique-partition of G st card C = it & ( for C being finite Clique-partition of G holds it <= card C ) );
existence
ex b1 being Nat st
( ex C being finite Clique-partition of G st card C = b1 & ( for C being finite Clique-partition of G holds b1 <= card C ) )
proof end;
uniqueness
for b1, b2 being Nat st ex C being finite Clique-partition of G st card C = b1 & ( for C being finite Clique-partition of G holds b1 <= card C ) & ex C being finite Clique-partition of G st card C = b2 & ( for C being finite Clique-partition of G holds b2 <= card C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines cliquecover# SCMYCIEL:def 18 :
for G being with_finite_cliquecover# SimpleGraph
for b2 being Nat holds
( b2 = cliquecover# G iff ( ex C being finite Clique-partition of G st card C = b2 & ( for C being finite Clique-partition of G holds b2 <= card C ) ) );

definition
let G be SimpleGraph;
let S be Subset of (Vertices G);
attr S is stable means :Def19: :: SCMYCIEL:def 19
 for x, y being set st x <> y & x in S & y in S holds
{x,y} nin G;
end;

:: deftheorem Def19 defines stable SCMYCIEL:def 19 :
for G being SimpleGraph
for S being Subset of (Vertices G) holds
( S is stable iff for x, y being set st x <> y & x in S & y in S holds
{x,y} nin G );

theorem :: SCMYCIEL:60
for G being SimpleGraph holds {} (Vertices G) is stable ;

theorem Th61: :: SCMYCIEL:61
for G being SimpleGraph
for S being Subset of (Vertices G)
for v being object st S = {v} holds
S is stable
proof end;

registration
let G be SimpleGraph;
cluster trivial -> stable for Element of bool (Vertices G);
coherence
for b1 being Subset of (Vertices G) st b1 is trivial holds
b1 is stable
proof end;
end;

registration
let G be SimpleGraph;
cluster stable for Element of bool (Vertices G);
existence
ex b1 being Subset of (Vertices G) st b1 is stable
proof end;
end;

definition
let G be SimpleGraph;
mode StableSet of G is stable Subset of (Vertices G);
end;

theorem Th62: :: SCMYCIEL:62
for G being SimpleGraph
for x, y being set st x in Vertices G & y in Vertices G & {x,y} nin G holds
{x,y} is StableSet of G
proof end;

theorem Th63: :: SCMYCIEL:63
for G being with_finite_clique# SimpleGraph st clique# G = 1 holds
Vertices G is StableSet of G
proof end;

registration
let G be SimpleGraph;
cluster finite stable for Element of bool (Vertices G);
existence
ex b1 being StableSet of G st b1 is finite
proof end;
end;

theorem Th64: :: SCMYCIEL:64
for G being SimpleGraph
for A being StableSet of G
for B being Subset of A holds B is StableSet of G
proof end;

definition
let G be SimpleGraph;
let P be a_partition of Vertices G;
attr P is StableSet-wise means :Def20: :: SCMYCIEL:def 20
 for x being set st x in P holds
x is StableSet of G;
end;

:: deftheorem Def20 defines StableSet-wise SCMYCIEL:def 20 :
for G being SimpleGraph
for P being a_partition of Vertices G holds
( P is StableSet-wise iff for x being set st x in P holds
x is StableSet of G );

theorem Th65: :: SCMYCIEL:65
for G being SimpleGraph holds SmallestPartition (Vertices G) is StableSet-wise
proof end;

registration
let G be SimpleGraph;
cluster V38() V278() StableSet-wise for a_partition of Vertices G;
existence
ex b1 being a_partition of Vertices G st b1 is StableSet-wise
proof end;
end;

definition
let G be SimpleGraph;
mode Coloring of G is StableSet-wise a_partition of Vertices G;
end;

definition
let G be SimpleGraph;
attr G is finitely_colorable means :Def21: :: SCMYCIEL:def 21
 ex C being Coloring of G st C is finite ;
end;

:: deftheorem Def21 defines finitely_colorable SCMYCIEL:def 21 :
for G being SimpleGraph holds
( G is finitely_colorable iff ex C being Coloring of G st C is finite );

registration
cluster non empty V38() finite-membered V243() V278() subset-closed 1 -at_most_dimensional SimpleGraph-like finitely_colorable for set ;
existence
ex b1 being SimpleGraph st b1 is finitely_colorable
proof end;
end;

registration
cluster finite SimpleGraph-like -> finitely_colorable for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is finitely_colorable ;
proof end;
end;

registration
let G be finitely_colorable SimpleGraph;
cluster V38() finite V278() StableSet-wise for a_partition of Vertices G;
existence
ex b1 being Coloring of G st b1 is finite by Def21;
end;

theorem Th66: :: SCMYCIEL:66
for G being SimpleGraph
for S being Clique of G
for L being set st L c= Vertices S holds
G SubgraphInducedBy L is Clique of G
proof end;

theorem Th67: :: SCMYCIEL:67
for G being SimpleGraph
for C being Coloring of G
for S being Subset of (Vertices G) holds C | S is Coloring of (G SubgraphInducedBy S)
proof end;

registration
let G be finitely_colorable SimpleGraph;
let S be set ;
cluster G SubgraphInducedBy S -> finitely_colorable ;
coherence
G SubgraphInducedBy S is finitely_colorable
proof end;
end;

definition
let G be finitely_colorable SimpleGraph;
func chromatic# G -> Nat means :Def22: :: SCMYCIEL:def 22
( ex C being finite Coloring of G st card C = it & ( for C being finite Coloring of G holds it <= card C ) );
existence
ex b1 being Nat st
( ex C being finite Coloring of G st card C = b1 & ( for C being finite Coloring of G holds b1 <= card C ) )
proof end;
uniqueness
for b1, b2 being Nat st ex C being finite Coloring of G st card C = b1 & ( for C being finite Coloring of G holds b1 <= card C ) & ex C being finite Coloring of G st card C = b2 & ( for C being finite Coloring of G holds b2 <= card C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines chromatic# SCMYCIEL:def 22 :
for G being finitely_colorable SimpleGraph
for b2 being Nat holds
( b2 = chromatic# G iff ( ex C being finite Coloring of G st card C = b2 & ( for C being finite Coloring of G holds b2 <= card C ) ) );

theorem Th68: :: SCMYCIEL:68
for G, H being finitely_colorable SimpleGraph st G c= H holds
chromatic# G <= chromatic# H
proof end;

theorem Th69: :: SCMYCIEL:69
for X being finite set holds chromatic# (CompleteSGraph X) = card X
proof end;

theorem Th70: :: SCMYCIEL:70
for G being finitely_colorable SimpleGraph
for C being finite Coloring of G
for c being set st c in C & card C = chromatic# G holds
ex v being Element of Vertices G st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of Vertices G st
( w in Adjacent v & w in d ) ) )
proof end;

definition
let G be SimpleGraph;
attr G is with_finite_stability# means :Def23: :: SCMYCIEL:def 23
 ex A being finite StableSet of G st
for B being finite StableSet of G holds card B <= card A;
end;

:: deftheorem Def23 defines with_finite_stability# SCMYCIEL:def 23 :
for G being SimpleGraph holds
( G is with_finite_stability# iff ex A being finite StableSet of G st
for B being finite StableSet of G holds card B <= card A );

registration
cluster finite SimpleGraph-like -> with_finite_stability# for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is finite holds
b1 is with_finite_stability# ;
proof end;
end;

registration
let G be with_finite_stability# SimpleGraph;
cluster stable -> finite for Element of bool (Vertices G);
correctness
coherence
for b1 being StableSet of G holds b1 is finite ;
proof end;
end;

registration
cluster non empty V38() finite-membered V243() V278() subset-closed non void 1 -at_most_dimensional SimpleGraph-like with_finite_stability# for set ;
existence
ex b1 being SimpleGraph st
( b1 is with_finite_stability# & not b1 is void )
proof end;
end;

definition
let G be with_finite_stability# SimpleGraph;
func stability# G -> Nat means :Def24: :: SCMYCIEL:def 24
( ex A being finite StableSet of G st card A = it & ( for T being finite StableSet of G holds card T <= it ) );
existence
ex b1 being Nat st
( ex A being finite StableSet of G st card A = b1 & ( for T being finite StableSet of G holds card T <= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex A being finite StableSet of G st card A = b1 & ( for T being finite StableSet of G holds card T <= b1 ) & ex A being finite StableSet of G st card A = b2 & ( for T being finite StableSet of G holds card T <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines stability# SCMYCIEL:def 24 :
for G being with_finite_stability# SimpleGraph
for b2 being Nat holds
( b2 = stability# G iff ( ex A being finite StableSet of G st card A = b2 & ( for T being finite StableSet of G holds card T <= b2 ) ) );

registration
let G be non void with_finite_stability# SimpleGraph;
cluster stability# G -> positive ;
correctness
coherence
stability# G is positive ;
proof end;
end;

theorem Th71: :: SCMYCIEL:71
for G being with_finite_stability# SimpleGraph st stability# G = 1 holds
G is clique
proof end;

registration
cluster SimpleGraph-like with_finite_clique# with_finite_stability# -> finite for set ;
correctness
coherence
for b1 being SimpleGraph st b1 is with_finite_clique# & b1 is with_finite_stability# holds
b1 is finite ;
proof end;
end;

theorem Th72: :: SCMYCIEL:72
for G being SimpleGraph
for C being Clique of G holds Vertices C is StableSet of (Complement G)
proof end;

theorem Th73: :: SCMYCIEL:73
for G being SimpleGraph
for C being Clique of (Complement G) holds Vertices C is StableSet of G
proof end;

theorem Th74: :: SCMYCIEL:74
for G being SimpleGraph
for C being StableSet of G holds (Complement G) SubgraphInducedBy C is Clique of (Complement G)
proof end;

theorem Th75: :: SCMYCIEL:75
for G being SimpleGraph
for C being StableSet of (Complement G) holds G SubgraphInducedBy C is Clique of G
proof end;

registration
let G be with_finite_clique# SimpleGraph;
cluster Complement G -> with_finite_stability# ;
correctness
coherence
Complement G is with_finite_stability# ;
proof end;
end;

registration
let G be with_finite_stability# SimpleGraph;
cluster Complement G -> with_finite_clique# ;
correctness
coherence
Complement G is with_finite_clique# ;
proof end;
end;

theorem Th76: :: SCMYCIEL:76
for G being with_finite_clique# SimpleGraph holds clique# G = stability# (Complement G)
proof end;

theorem :: SCMYCIEL:77
for G being with_finite_stability# SimpleGraph holds stability# G = clique# (Complement G)
proof end;

theorem Th78: :: SCMYCIEL:78
for G being SimpleGraph
for C being Clique-partition of (Complement G) holds C is Coloring of G
proof end;

theorem Th79: :: SCMYCIEL:79
for G being SimpleGraph
for C being Clique-partition of G holds C is Coloring of (Complement G)
proof end;

theorem Th80: :: SCMYCIEL:80
for G being SimpleGraph
for C being Coloring of G holds C is Clique-partition of (Complement G)
proof end;

theorem :: SCMYCIEL:81
for G being SimpleGraph
for C being Coloring of (Complement G) holds C is Clique-partition of G
proof end;

registration
let G be finitely_colorable SimpleGraph;
cluster Complement G -> with_finite_cliquecover# ;
correctness
coherence
Complement G is with_finite_cliquecover# ;
proof end;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
cluster Complement G -> finitely_colorable ;
correctness
coherence
Complement G is finitely_colorable ;
proof end;
end;

theorem Th82: :: SCMYCIEL:82
for G being finitely_colorable SimpleGraph holds chromatic# G = cliquecover# (Complement G)
proof end;

theorem :: SCMYCIEL:83
for G being with_finite_cliquecover# SimpleGraph holds cliquecover# G = chromatic# (Complement G)
proof end;

definition
let G be SimpleGraph;
func Mycielskian G -> SimpleGraph equals :: SCMYCIEL:def 25
((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;
correctness
coherence
((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } is SimpleGraph;
proof end;
end;

:: deftheorem defines Mycielskian SCMYCIEL:def 25 :
for G being SimpleGraph holds Mycielskian G = ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;

theorem Th84: :: SCMYCIEL:84
for G being SimpleGraph holds G c= Mycielskian G
proof end;

theorem Th85: :: SCMYCIEL:85
for G being SimpleGraph
for v being set holds
( v in Vertices (Mycielskian G) iff ( v in union G or ex x being set st
( x in union G & v = [x,(union G)] ) or v = union G ) )
proof end;

theorem Th86: :: SCMYCIEL:86
for G being SimpleGraph holds Vertices (Mycielskian G) = ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}
proof end;

theorem Th87: :: SCMYCIEL:87
for G being SimpleGraph holds union G in union (Mycielskian G)
proof end;

theorem Th88: :: SCMYCIEL:88
for G being void SimpleGraph holds Mycielskian G = {{},{(union G)}}
proof end;

registration
let G be finite SimpleGraph;
cluster Mycielskian G -> finite ;
correctness
coherence
Mycielskian G is finite ;
proof end;
end;

theorem Th89: :: SCMYCIEL:89
for G being finite SimpleGraph holds order (Mycielskian G) = (2 * (order G)) + 1
proof end;

theorem Th90: :: SCMYCIEL:90
for G being SimpleGraph
for e being set holds
( e in Edges (Mycielskian G) iff ( e in Edges G or ex x, y being Element of union G st
( e = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( e = {(union G),[y,(union G)]} & y in union G ) ) )
proof end;

theorem Th91: :: SCMYCIEL:91
for G being SimpleGraph holds Edges (Mycielskian G) = ((Edges G) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[y,(union G)]} where y is Element of union G : y in union G }
proof end;

theorem Th92: :: SCMYCIEL:92
for G being finite SimpleGraph holds size (Mycielskian G) = (3 * (size G)) + (order G)
proof end;

theorem Th93: :: SCMYCIEL:93
for G being SimpleGraph
for s, t being object holds
( not {s,t} in Edges (Mycielskian G) or {s,t} in Edges G or ( ( s in union G or s = union G ) & ex y being object st
( y in union G & t = [y,(union G)] ) ) or ( ( t in union G or t = union G ) & ex y being object st
( y in union G & s = [y,(union G)] ) ) )
proof end;

theorem Th94: :: SCMYCIEL:94
for G being SimpleGraph
for u being object st {(union G),u} in Edges (Mycielskian G) holds
ex x being object st
( x in union G & u = [x,(union G)] )
proof end;

theorem Th95: :: SCMYCIEL:95
for G being SimpleGraph
for u being object st u in Vertices G holds
{[u,(union G)]} in Mycielskian G
proof end;

theorem Th96: :: SCMYCIEL:96
for G being SimpleGraph
for u being set st u in Vertices G holds
{[u,(union G)],(union G)} in Mycielskian G
proof end;

theorem Th97: :: SCMYCIEL:97
for G being SimpleGraph
for x, y being object holds not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
proof end;

theorem Th98: :: SCMYCIEL:98
for G being SimpleGraph
for x, y being object st x <> y holds
not {[x,(union G)],[y,(union G)]} in Mycielskian G
proof end;

theorem Th99: :: SCMYCIEL:99
for G being SimpleGraph
for x, y being object st {[x,(union G)],y} in Edges (Mycielskian G) holds
( x <> y & x in union G & ( y in union G or y = union G ) )
proof end;

theorem Th100: :: SCMYCIEL:100
for G being SimpleGraph
for x, y being set st {[x,(union G)],y} in Mycielskian G holds
x <> y
proof end;

theorem Th101: :: SCMYCIEL:101
for G being SimpleGraph
for x, y being set st y in union G & {[x,(union G)],y} in Mycielskian G holds
{x,y} in G
proof end;

theorem Th102: :: SCMYCIEL:102
for G being SimpleGraph
for x, y being set st {x,y} in Edges G holds
{[x,(union G)],y} in Mycielskian G
proof end;

theorem Th103: :: SCMYCIEL:103
for G being SimpleGraph
for x, y being set st x in Vertices G & y in Vertices G & {x,y} in Mycielskian G holds
{x,y} in G
proof end;

theorem Th104: :: SCMYCIEL:104
for G being SimpleGraph holds G = (Mycielskian G) SubgraphInducedBy (Vertices G)
proof end;

theorem Th105: :: SCMYCIEL:105
for G being SimpleGraph
for C being finite Clique of (Mycielskian G) st 3 <= order C holds
for v being Vertex of C holds v <> union G
proof end;

theorem Th106: :: SCMYCIEL:106
for G being with_finite_clique# SimpleGraph st clique# G = 0 holds
for D being finite Clique of (Mycielskian G) holds order D <= 1
proof end;

theorem :: SCMYCIEL:107
for G being SimpleGraph
for x being set st Vertices G = {x} holds
Mycielskian G = {{},{x},{[x,(union G)]},{(union G)},{[x,(union G)],(union G)}}
proof end;

theorem Th108: :: SCMYCIEL:108
for G being with_finite_clique# SimpleGraph st clique# G = 1 holds
for D being finite Clique of (Mycielskian G) holds order D <= 2
proof end;

theorem Th109: :: SCMYCIEL:109
for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds
for D being finite Clique of (Mycielskian G) holds order D <= clique# G
proof end;

registration
let G be with_finite_clique# SimpleGraph;
cluster Mycielskian G -> with_finite_clique# ;
coherence
Mycielskian G is with_finite_clique#
proof end;
end;

theorem Th110: :: SCMYCIEL:110
for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds
clique# (Mycielskian G) = clique# G
proof end;

theorem Th111: :: SCMYCIEL:111
for G being finitely_colorable SimpleGraph ex E being Coloring of (Mycielskian G) st card E = 1 + (chromatic# G)
proof end;

registration
let G be finitely_colorable SimpleGraph;
cluster Mycielskian G -> finitely_colorable ;
coherence
Mycielskian G is finitely_colorable
proof end;
end;

theorem Th112: :: SCMYCIEL:112
for G being finitely_colorable SimpleGraph holds chromatic# (Mycielskian G) = 1 + (chromatic# G)
proof end;

definition
let G be SimpleGraph;
func MycielskianSeq G -> ManySortedSet of NAT means :Def26: :: SCMYCIEL:def 26
 ex myc being Function st
( it = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) );
existence
ex b1 being ManySortedSet of NAT ex myc being Function st
( b1 = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of NAT st ex myc being Function st
( b1 = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) & ex myc being Function st
( b2 = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def26 defines MycielskianSeq SCMYCIEL:def 26 :
for G being SimpleGraph
for b2 being ManySortedSet of NAT holds
( b2 = MycielskianSeq G iff ex myc being Function st
( b2 = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) );

theorem Th113: :: SCMYCIEL:113
for G being SimpleGraph holds (MycielskianSeq G) . 0 = G
proof end;

theorem Th114: :: SCMYCIEL:114
for G being SimpleGraph
for n being Nat holds (MycielskianSeq G) . n is SimpleGraph
proof end;

registration
let G be SimpleGraph;
let n be Nat;
cluster (MycielskianSeq G) . n -> SimpleGraph-like ;
coherence
(MycielskianSeq G) . n is SimpleGraph-like by Th114;
end;

theorem Th115: :: SCMYCIEL:115
for G, H being SimpleGraph
for n being Nat holds (MycielskianSeq G) . (n + 1) = Mycielskian ((MycielskianSeq G) . n)
proof end;

registration
let G be with_finite_clique# SimpleGraph;
let n be Nat;
cluster (MycielskianSeq G) . n -> with_finite_clique# ;
coherence
(MycielskianSeq G) . n is with_finite_clique#
proof end;
end;

registration
let G be finitely_colorable SimpleGraph;
let n be Nat;
cluster (MycielskianSeq G) . n -> finitely_colorable ;
coherence
(MycielskianSeq G) . n is finitely_colorable
proof end;
end;

registration
let G be finite SimpleGraph;
let n be Nat;
cluster (MycielskianSeq G) . n -> finite ;
coherence
(MycielskianSeq G) . n is finite
proof end;
end;

theorem Th116: :: SCMYCIEL:116
for G being finite SimpleGraph
for n being Nat holds order ((MycielskianSeq G) . n) = (((2 |^ n) * (order G)) + (2 |^ n)) - 1
proof end;

theorem :: SCMYCIEL:117
for G being finite SimpleGraph
for n being Nat holds size ((MycielskianSeq G) . n) = (((3 |^ n) * (size G)) + (((3 |^ n) - (2 |^ n)) * (order G))) + ((n + 1) block 3)
proof end;

theorem Th118: :: SCMYCIEL:118
for n being Nat holds
( clique# ((MycielskianSeq (CompleteSGraph 2)) . n) = 2 & chromatic# ((MycielskianSeq (CompleteSGraph 2)) . n) = n + 2 )
proof end;

theorem :: SCMYCIEL:119
for n being Nat ex G being finite SimpleGraph st
( clique# G = 2 & chromatic# G > n )
proof end;

theorem :: SCMYCIEL:120
for n being Nat ex G being finite SimpleGraph st
( stability# G = 2 & cliquecover# G > n )
proof end;