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


begin

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

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

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

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

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

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

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

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

registration
cluster Vertices {{}} -> empty ;
correctness
coherence
union {{}} is empty ;
by ZFMISC_1:25;
end;

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

theorem BSPACEdef9: :: 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 McopyV: :: 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 :LEdges: :: 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 LEdges 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 SG4: :: 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 SG4a: :: SCMYCIEL:12
for X, x, y being set st x <> y & {x,y} in X holds
{x,y} in PairsOf X
proof end;

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

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

theorem MnewE: :: 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 :Lvoid: :: SCMYCIEL:def 2
X = {{}};
end;

:: deftheorem Lvoid 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 Lvoid;
end;

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

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

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

theorem uVoid1: :: 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 :Ledgeless: :: SCMYCIEL:def 3
 PairsOf X is empty ;
end;

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

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

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

begin

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

:: deftheorem Lnatmost 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;

Void0: 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 SG1: :: SCMYCIEL:20
for G being non empty subset-closed set holds {} in G
proof end;

theorem Lnatmost1: :: SCMYCIEL:21
for n being natural number
for X being b1 -at_most_dimensional set
for x being Element of X st x in X holds
card x <= n + 1 by Lnatmost, NAT_1:39;

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
proof end;
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 ;
proof end;
end;

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

:: deftheorem LSGlike 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 );
by LSGlike;
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 ;
by LSGlike;
end;

theorem eSG1: :: SCMYCIEL:22
{{}} is SimpleGraph-like
proof end;

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

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

definition
mode SimpleGraph is SimpleGraph-like set ;
end;

registration
cluster non empty finite-membered V233() V267() 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 finite finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like for set ;
existence
ex b1 being SimpleGraph st b1 is finite by eSG1;
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 FinSG: :: SCMYCIEL:23
for G being SimpleGraph st Vertices G is finite holds
G is finite
proof end;

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

theorem SingleVertex: :: 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 Lorder1: :: 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 SG0: :: SCMYCIEL:27
for G being SimpleGraph holds G = ({{}} \/ (singletons (Vertices G))) \/ (Edges G)
proof end;

theorem VoidGV: :: SCMYCIEL:28
for G being SimpleGraph st Vertices G = {} holds
G is void by uVoid1, Lvoid;

theorem SG2: :: 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 size0SG: :: 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 :Ladj: :: 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 Ladj 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 :LSGofX: :: SCMYCIEL:def 9
 Vertices it = X;
existence
ex b1 being SimpleGraph st Vertices b1 = X
proof end;
end;

:: deftheorem LSGofX 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 CSGdef: :: 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 CSG1a: :: SCMYCIEL:33
for X, x being set st x in X holds
{x} in CompleteSGraph X
proof end;

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

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

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

theorem P2: :: 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 CSGsingle: :: 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;

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

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

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

Compl2: 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 CisSG;
involutiveness
for b1, b2 being SimpleGraph st b1 = (CompleteSGraph (Vertices b2)) \ (Edges b2) holds
b2 = (CompleteSGraph (Vertices b1)) \ (Edges b1) by Compl2;
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 Compl1;

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

begin

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 Sub3a: :: 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 Sub0b: :: SCMYCIEL:44
for G, H being SimpleGraph st G c= H holds
G c= H SubgraphInducedBy (Vertices G)
proof end;

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

Sub3: 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 Sub5: :: SCMYCIEL:45
for G being SimpleGraph
for L being set holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L
proof end;

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

Sub6: 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 SingleSub: :: SCMYCIEL:46
for G being SimpleGraph
for x being set st x in Vertices G holds
G SubgraphInducedBy {x} = {{},{x}}
proof end;

begin

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

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

theorem Lclique1: :: 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 eclique: :: SCMYCIEL:48
{{}} is clique
proof end;

registration
cluster non empty finite-membered V233() V267() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for set ;
existence
ex b1 being SimpleGraph st b1 is clique by eclique;
let G be SimpleGraph;
cluster non empty finite-membered V233() V267() 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 cliqueCSG0: :: SCMYCIEL:49
for X being set holds CompleteSGraph X is clique
proof end;

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

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

theorem Cliqueon2: :: 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 finite finite-membered V233() V267() 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 CliqueS: :: 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 Clique2a: :: 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 :Lwfcno: :: 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 Lwfcno 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 finite-membered V233() V267() 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 :Lcliqueno: :: 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 Lcliqueno 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 Cno0: :: 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 Th8: :: 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 Cno2: :: SCMYCIEL:57
for G being with_finite_clique# SimpleGraph st Edges G <> {} holds
clique# G >= 2
proof end;

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

theorem cliqueCSG: :: 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 :LCliquewise: :: SCMYCIEL:def 16
 for x being set st x in P holds
G SubgraphInducedBy x is Clique of G;
end;

:: deftheorem LCliquewise 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 V267() 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 ;
proof end;
end;

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

:: deftheorem Lwfclicov 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 finite V267() Clique-wise for a_partition of Vertices G;
correctness
existence
ex b1 being Clique-partition of G st b1 is finite ;
by Lwfclicov;
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 :Lclicovno: :: 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 Lclicovno 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 ) ) );

begin

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

:: deftheorem Lstable 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 stable0: :: SCMYCIEL:60
for G being SimpleGraph holds {} (Vertices G) is stable
proof end;

theorem stable1: :: SCMYCIEL:61
for G being SimpleGraph
for S being Subset of (Vertices G)
for v being set 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 Th14: :: 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 Th19: :: 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 Th16: :: 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 :LStableSetwise: :: SCMYCIEL:def 20
 for x being set st x in P holds
x is StableSet of G;
end;

:: deftheorem LStableSetwise 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 Coloring1: :: SCMYCIEL:65
for G being SimpleGraph holds SmallestPartition (Vertices G) is StableSet-wise
proof end;

registration
let G be SimpleGraph;
cluster V267() 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 :Lfc: :: SCMYCIEL:def 21
 ex C being Coloring of G st C is finite ;
end;

:: deftheorem Lfc 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 finite-membered V233() V267() 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 finite V267() StableSet-wise for a_partition of Vertices G;
existence
ex b1 being Coloring of G st b1 is finite by Lfc;
end;

theorem SGClique0: :: 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 Tsr0: :: 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 :Lchro: :: 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 Lchro 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 Subchro: :: SCMYCIEL:68
for G, H being finitely_colorable SimpleGraph st G c= H holds
chromatic# G <= chromatic# H
proof end;

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

theorem AdjCol: :: 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 :Lwfstab: :: 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 Lwfstab 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 finite-membered V233() V267() 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 :Lstabno: :: 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 Lstabno 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 Th21: :: 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 CliStaCompl: :: SCMYCIEL:72
for G being SimpleGraph
for C being Clique of G holds Vertices C is StableSet of (Complement G)
proof end;

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

theorem StaCliCompl: :: 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 StaComplCli: :: 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 cliRstaCR: :: 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 ClicoComplChr: :: SCMYCIEL:78
for G being SimpleGraph
for C being Clique-partition of (Complement G) holds C is Coloring of G
proof end;

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

theorem ChrClicoCompl: :: 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 chrRcovCR: :: 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;

begin

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 M0: :: SCMYCIEL:84
for G being SimpleGraph holds G c= Mycielskian G
proof end;

theorem M0v1: :: 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 M0v2: :: SCMYCIEL:86
for G being SimpleGraph holds Vertices (Mycielskian G) = ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)}
proof end;

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

theorem MGvoid: :: 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 M0order: :: SCMYCIEL:89
for G being finite SimpleGraph holds order (Mycielskian G) = (2 * (order G)) + 1
proof end;

theorem M0e0: :: 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 M0e: :: 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 M0size: :: SCMYCIEL:92
for G being finite SimpleGraph holds size (Mycielskian G) = (3 * (size G)) + (order G)
proof end;

theorem M0e1: :: SCMYCIEL:93
for G being SimpleGraph
for s, t being set 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 set st
( y in union G & t = [y,(union G)] ) ) or ( ( t in union G or t = union G ) & ex y being set st
( y in union G & s = [y,(union G)] ) ) )
proof end;

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

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

theorem M0e2a: :: 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 M0e3: :: SCMYCIEL:97
for G being SimpleGraph
for x, y being set holds not {[x,(union G)],[y,(union G)]} in Edges (Mycielskian G)
proof end;

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

theorem M0e4: :: SCMYCIEL:99
for G being SimpleGraph
for x, y being set 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 M0e4a: :: 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 M0e4b: :: 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 M0e4c: :: 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 M1: :: 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 GsubMG: :: SCMYCIEL:104
for G being SimpleGraph holds G = (Mycielskian G) SubgraphInducedBy (Vertices G)
proof end;

theorem MClique3: :: 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 MClique0: :: 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 MClique1: :: 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 MClique2: :: 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 MClique: :: SCMYCIEL:110
for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds
clique# (Mycielskian G) = clique# G
proof end;

theorem Mfc1: :: 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 Mcn1: :: 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 :LMycielskianSeq: :: 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 LMycielskianSeq 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 MSeq0: :: SCMYCIEL:113
for G being SimpleGraph holds (MycielskianSeq G) . 0 = G
proof end;

theorem MGS0: :: 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 MGS0;
end;

theorem MSeq1: :: 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 MSnorder: :: 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 MycTh: :: 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;