:: Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: 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
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
correctness
coherence ;
;
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,()]} where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card ())
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 ())
proof end;

registration
let X be finite set ;
coherence ;
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 ;
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 () = 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
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 ;
coherence
proof end;
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;
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;
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 ;
coherence
proof end;
end;

registration
let n be Nat;
let X be n -at_most_dimensional set ;
let Y be set ;
coherence
proof end;
coherence 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
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 )
;
;
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

registration
correctness by Th22;
end;

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

definition end;

registration
existence
ex b1 being SimpleGraph st b1 is void
proof end;
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 ();
coherence
card () is Nat
;
end;

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

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

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

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

definition end;

theorem Th27: :: SCMYCIEL:27
for G being SimpleGraph holds 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 () 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 () 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 () 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 () 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 ()
proof end;

registration
let X be finite set ;
correctness
coherence ;
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
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;
existence
ex b1 being Subset of G st b1 is SimpleGraph-like
proof end;
end;

definition end;

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

Lm4: for G being SimpleGraph holds Vertices G = Vertices (() \ ())
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 (() \ ()) )

proof end;

Lm6: for G, CG being SimpleGraph st CG = () \ () holds
() \ (Edges CG) = G

proof end;

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

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

theorem :: SCMYCIEL:40
for G being SimpleGraph holds Vertices G = Vertices () 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 () ) 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 ;
coherence
proof end;
end;

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

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

registration
let G be finite SimpleGraph;
let L be set ;
coherence ;
end;

registration
let G be SimpleGraph;
let L be finite set ;
coherence ;
end;

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

Lm7: for G being SimpleGraph
for L, x being set st x in Vertices () 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 ()

proof end;

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

Lm9: for G being SimpleGraph
for L being set st L c= Vertices G holds
Vertices () = 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 ();
end;

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

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
existence
ex b1 being SimpleGraph st b1 is clique
by Th48;
let G be SimpleGraph;
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 ;
correctness
coherence ;
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;
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
existence
ex b1 being SimpleGraph st b1 is with_finite_clique#
proof end;
end;

registration
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# () = 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 end;

registration
let G be void SimpleGraph;
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
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;
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 ();
correctness
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 ();
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 () 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 {} () is stable ;

theorem Th61: :: SCMYCIEL:61
for G being SimpleGraph
for S being Subset of ()
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 ();
coherence
for b1 being Subset of () st b1 is trivial holds
b1 is stable
proof end;
end;

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

definition
let G be SimpleGraph;
mode StableSet of G is stable Subset of ();
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 ();
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 () is StableSet-wise
proof end;

registration
let G be SimpleGraph;
existence
ex b1 being a_partition of Vertices G st b1 is StableSet-wise
proof end;
end;

definition 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
existence
ex b1 being SimpleGraph st b1 is finitely_colorable
proof end;
end;

registration
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;
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 () holds C | S is Coloring of ()
proof end;

registration
let G be finitely_colorable SimpleGraph;
let S be set ;
coherence
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# () = 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
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 ();
correctness
coherence
for b1 being StableSet of G holds b1 is finite
;
proof end;
end;

registration
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;
correctness
coherence ;
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
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 ()
proof end;

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

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

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

registration
let G be with_finite_clique# SimpleGraph;
correctness
proof end;
end;

registration
let G be with_finite_stability# SimpleGraph;
correctness
proof end;
end;

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

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

theorem Th78: :: SCMYCIEL:78
for G being SimpleGraph
for C being Clique-partition of () 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 ()
proof end;

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

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

registration
let G be finitely_colorable SimpleGraph;
correctness
proof end;
end;

registration
let G be with_finite_cliquecover# SimpleGraph;
correctness
proof end;
end;

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

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

definition
let G be SimpleGraph;
func Mycielskian G -> SimpleGraph equals :: SCMYCIEL:def 25
((( \/ { {x} where x is Element of (() \/ [:(),{()}:]) \/ {()} : verum } ) \/ ()) \/ { {x,[y,()]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(),[x,()]} where x is Element of union G : x in Vertices G } ;
correctness
coherence
((( \/ { {x} where x is Element of (() \/ [:(),{()}:]) \/ {()} : verum } ) \/ ()) \/ { {x,[y,()]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(),[x,()]} 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 (() \/ [:(),{()}:]) \/ {()} : verum } ) \/ ()) \/ { {x,[y,()]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(),[x,()]} 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 () iff ( v in union G or ex x being set st
( x in union G & v = [x,()] ) or v = union G ) )
proof end;

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

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

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

registration
let G be finite SimpleGraph;
correctness
coherence ;
proof end;
end;

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

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

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

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

theorem Th93: :: SCMYCIEL:93
for G being SimpleGraph
for s, t being object holds
( not {s,t} in Edges () 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,()] ) ) or ( ( t in union G or t = union G ) & ex y being object st
( y in union G & s = [y,()] ) ) )
proof end;

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

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

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

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

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

theorem Th99: :: SCMYCIEL:99
for G being SimpleGraph
for x, y being object st {[x,()],y} in Edges () 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,()],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,()],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,()],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 = () SubgraphInducedBy ()
proof end;

theorem Th105: :: SCMYCIEL:105
for G being SimpleGraph
for C being finite Clique of () 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 () 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,()]},{()},{[x,()],()}}
proof end;

theorem Th108: :: SCMYCIEL:108
for G being with_finite_clique# SimpleGraph st clique# G = 1 holds
for D being finite Clique of () 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 () holds order D <= clique# G
proof end;

registration
let G be with_finite_clique# SimpleGraph;
coherence
proof end;
end;

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

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

registration
let G be finitely_colorable SimpleGraph;
coherence
proof end;
end;

theorem Th112: :: SCMYCIEL:112
for G being finitely_colorable SimpleGraph holds chromatic# () = 1 + ()
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 () . 0 = G
proof end;

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

registration
let G be SimpleGraph;
let n be Nat;
coherence by Th114;
end;

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

registration
let G be with_finite_clique# SimpleGraph;
let n be Nat;
coherence
proof end;
end;

registration
let G be finitely_colorable SimpleGraph;
let n be Nat;
coherence
proof end;
end;

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

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

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

theorem Th118: :: SCMYCIEL:118
for n being Nat holds
( clique# (() . n) = 2 & chromatic# (() . 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;