:: 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 b₁ being FinSequence holds b₁ 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 b₁ being Subset of G st
for e being set holds
( e in b₁ iff ( e in G & card e = 2 ) )

proof end;

uniqueness
for b₁, b₂ being Subset of G st ( for e being set holds
( e in b₁ iff ( e in G & card e = 2 ) ) ) & ( for e being set holds
( e in b₂ iff ( e in G & card e = 2 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines PairsOf SCMYCIEL:def 1 :
for G being set
for b₂ being Subset of G holds
( b₂ = PairsOf G iff for e being set holds
( e in b₂ 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 b₁ being set st b₁ is void by Def2;

end;

registration

cluster void -> finite for set ;

coherence
for b₁ being set st b₁ is void holds
b₁ 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 b₁ being set st
( b₁ is finite-membered & not b₁ 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 b₁ being set st b₁ is n -at_most_dimensional holds
b₁ 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 b₁ being set st
( b₁ is n -at_most_dimensional & b₁ is subset-closed & not b₁ 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 b₁ -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 b₁ being Subset of X holds b₁ 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 b₁ being set st b₁ is SimpleGraph-like holds
( b₁ is 1 -at_most_dimensional & b₁ is subset-closed & not b₁ is empty );
;

cluster non empty subset-closed 1 -at_most_dimensional -> SimpleGraph-like for set ;

correctness
coherence
for b₁ being set st b₁ is 1 -at_most_dimensional & b₁ is subset-closed & not b₁ is empty holds
b₁ 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 b₁ being set st b₁ 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 b₁ being SimpleGraph st b₁ 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 b₁ being SimpleGraph st b₁ 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 b₁ being Subset of (Vertices G) st
for x being Element of Vertices G holds
( x in b₁ iff {v,x} in Edges G )

proof end;

uniqueness
for b₁, b₂ being Subset of (Vertices G) st ( for x being Element of Vertices G holds
( x in b₁ iff {v,x} in Edges G ) ) & ( for x being Element of Vertices G holds
( x in b₂ iff {v,x} in Edges G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Adjacent SCMYCIEL:def 8 :
for G being SimpleGraph
for v being Element of Vertices G
for b₃ being Subset of (Vertices G) holds
( b₃ = Adjacent v iff for x being Element of Vertices G holds
( x in b₃ 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 b₁ being SimpleGraph st Vertices b₁ = X

proof end;

end;

:: deftheorem Def9 defines SimpleGraph SCMYCIEL:def 9 :
for X being set
for b₂ being SimpleGraph holds
( b₂ is SimpleGraph of X iff Vertices b₂ = 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 b₁ being Subset of G st b₁ 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 b₁, b₂ being SimpleGraph st b₁ = (CompleteSGraph (Vertices b₂)) \ (Edges b₂) holds
b₂ = (CompleteSGraph (Vertices b₁)) \ (Edges b₁) 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 b₁ being SimpleGraph st b₁ 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 b₁ being Subgraph of G st b₁ 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 b₁ being Clique of G st b₁ 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 b₁ being SimpleGraph st b₁ is with_finite_clique#

proof end;

end;

registration

cluster finite SimpleGraph-like -> with_finite_clique# for set ;

coherence
for b₁ being SimpleGraph st b₁ is finite holds
b₁ 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 b₁ being Nat st
( ex C being finite Clique of G st order C = b₁ & ( for T being finite Clique of G holds order T <= b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex C being finite Clique of G st order C = b₁ & ( for T being finite Clique of G holds order T <= b₁ ) & ex C being finite Clique of G st order C = b₂ & ( for T being finite Clique of G holds order T <= b₂ ) holds
b₁ = b₂

proof end;

end;

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

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 b₁ being a_partition of Vertices G st b₁ 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 b₁ being a_partition of Vertices G st b₁ is empty holds
b₁ 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 b₁ being SimpleGraph st b₁ is finite holds
b₁ 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 b₁ being Clique-partition of G st b₁ 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 b₁ being Nat st
( ex C being finite Clique-partition of G st card C = b₁ & ( for C being finite Clique-partition of G holds b₁ <= card C ) )

proof end;

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

proof end;

end;

:: deftheorem Def18 defines cliquecover# SCMYCIEL:def 18 :
for G being with_finite_cliquecover# SimpleGraph
for b₂ being Nat holds
( b₂ = cliquecover# G iff ( ex C being finite Clique-partition of G st card C = b₂ & ( for C being finite Clique-partition of G holds b₂ <= 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 b₁ being Subset of (Vertices G) st b₁ is trivial holds
b₁ is stable

proof end;

end;

registration

let G be SimpleGraph;

cluster stable for Element of bool (Vertices G);

existence
ex b₁ being Subset of (Vertices G) st b₁ 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 b₁ being StableSet of G st b₁ 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 b₁ being a_partition of Vertices G st b₁ 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 b₁ being SimpleGraph st b₁ is finitely_colorable

proof end;

end;

registration

cluster finite SimpleGraph-like -> finitely_colorable for set ;

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

proof end;

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

proof end;

end;

:: deftheorem Def22 defines chromatic# SCMYCIEL:def 22 :
for G being finitely_colorable SimpleGraph
for b₂ being Nat holds
( b₂ = chromatic# G iff ( ex C being finite Coloring of G st card C = b₂ & ( for C being finite Coloring of G holds b₂ <= 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 b₁ being SimpleGraph st b₁ is finite holds
b₁ 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 b₁ being StableSet of G holds b₁ 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 b₁ being SimpleGraph st
( b₁ is with_finite_stability# & not b₁ 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 b₁ being Nat st
( ex A being finite StableSet of G st card A = b₁ & ( for T being finite StableSet of G holds card T <= b₁ ) )

proof end;

uniqueness
for b₁, b₂ being Nat st ex A being finite StableSet of G st card A = b₁ & ( for T being finite StableSet of G holds card T <= b₁ ) & ex A being finite StableSet of G st card A = b₂ & ( for T being finite StableSet of G holds card T <= b₂ ) holds
b₁ = b₂

proof end;

end;

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

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 b₁ being SimpleGraph st b₁ is with_finite_clique# & b₁ is with_finite_stability# holds
b₁ 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 b₁ being ManySortedSet of NAT ex myc being Function st
( b₁ = 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 b₁, b₂ being ManySortedSet of NAT st ex myc being Function st
( b₁ = 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
( b₂ = myc & myc . 0 = G & ( for k being Nat
for G being SimpleGraph st G = myc . k holds
myc . (k + 1) = Mycielskian G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def26 defines MycielskianSeq SCMYCIEL:def 26 :
for G being SimpleGraph
for b₂ being ManySortedSet of NAT holds
( b₂ = MycielskianSeq G iff ex myc being Function st
( b₂ = 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;