:: by Piotr Rudnicki and Lorna Stewart

::

:: Received February 8, 2012

:: Copyright (c) 2012-2016 Association of Mizar Users

defpred S

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 )

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 )

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;

registration

not for b_{1} being FinSequence holds b_{1} is V40()
end;

cluster Relation-like NAT -defined Function-like finite V40() FinSequence-like FinSubsequence-like for set ;

existence not for b

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

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;

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

for s being Subset of X st s is 1 -element holds

ex x being set st

( x in X & s = {x} )

proof end;

definition

let G be set ;

ex b_{1} being Subset of G st

for e being set holds

( e in b_{1} iff ( e in G & card e = 2 ) )

for b_{1}, b_{2} being Subset of G st ( for e being set holds

( e in b_{1} iff ( e in G & card e = 2 ) ) ) & ( for e being set holds

( e in b_{2} iff ( e in G & card e = 2 ) ) ) holds

b_{1} = b_{2}

end;
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 for e being set holds

( e in it iff ( e in G & card e = 2 ) );

ex b

for e being set holds

( e in b

proof end;

uniqueness for b

( e in b

( e in b

b

proof end;

:: deftheorem Def1 defines PairsOf SCMYCIEL:def 1 :

for G being set

for b_{2} being Subset of G holds

( b_{2} = PairsOf G iff for e being set holds

( e in b_{2} iff ( e in G & card e = 2 ) ) );

for G being set

for b

( b

( e in b

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

ex x, y being set st

( x <> y & x in union X & y in union X & e = {x,y} )

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 )

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

registration
end;

:: deftheorem defines pairfree SCMYCIEL:def 3 :

for X being set holds

( X is pairfree iff PairsOf X is empty );

for X being set holds

( X is pairfree iff PairsOf X is empty );

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

proof end;

registration
end;

registration

let X be finite-membered set ;

let Y be set ;

coherence

X /\ Y is finite-membered

X \ Y is finite-membered ;

end;
let Y be set ;

coherence

X /\ Y is finite-membered

proof end;

coherence X \ Y is finite-membered ;

definition

let n be Nat;

let X be set ;

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

for x being set st x in X holds

card x c= n + 1;

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

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 b_{1} being set st b_{1} is n -at_most_dimensional holds

b_{1} is finite-membered ;

end;
correctness

coherence

for b

b

proof end;

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

proof end;

registration

let n be Nat;

existence

ex b_{1} being set st

( b_{1} is n -at_most_dimensional & b_{1} is subset-closed & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

theorem Th21: :: SCMYCIEL:21

for n being Nat

for X being b_{1} -at_most_dimensional set

for x being Element of X st x in X holds

card x <= n + 1

for X being b

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

X \/ Y is n -at_most_dimensional

end;
let X, Y be n -at_most_dimensional set ;

coherence

X \/ Y is n -at_most_dimensional

proof end;

registration

let n be Nat;

let X be n -at_most_dimensional set ;

let Y be set ;

coherence

X /\ Y is n -at_most_dimensional

X \ Y is n -at_most_dimensional by Def4;

end;
let X be n -at_most_dimensional set ;

let Y be set ;

coherence

X /\ Y is n -at_most_dimensional

proof end;

coherence X \ Y is n -at_most_dimensional by Def4;

registration

let n be Nat;

let X be n -at_most_dimensional set ;

correctness

coherence

for b_{1} being Subset of X holds b_{1} is n -at_most_dimensional ;

by Def4;

end;
let X be n -at_most_dimensional set ;

correctness

coherence

for b

by Def4;

definition

let s be set ;

end;
attr s is SimpleGraph-like means :: SCMYCIEL:def 5

( s is 1 -at_most_dimensional & s is subset-closed & not s is empty );

( s is 1 -at_most_dimensional & s is subset-closed & not s is empty );

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

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 b_{1} being set st b_{1} is SimpleGraph-like holds

( b_{1} is 1 -at_most_dimensional & b_{1} is subset-closed & not b_{1} is empty );

;

correctness

coherence

for b_{1} being set st b_{1} is 1 -at_most_dimensional & b_{1} is subset-closed & not b_{1} is empty holds

b_{1} is SimpleGraph-like ;

;

end;
coherence

for b

( b

;

correctness

coherence

for b

b

;

registration
end;

registration

ex b_{1} being SimpleGraph st b_{1} is void

ex b_{1} being SimpleGraph st b_{1} is finite
by Th22;

end;

cluster non empty V38() finite-membered V242() V277() subset-closed void 1 -at_most_dimensional SimpleGraph-like for set ;

existence ex b

proof end;

cluster non empty V38() finite finite-membered V242() V277() subset-closed 1 -at_most_dimensional SimpleGraph-like for set ;

existence ex b

:: deftheorem defines order SCMYCIEL:def 6 :

for X being finite finite-membered set holds order X = card (union X);

for X being finite finite-membered set holds order X = card (union X);

definition

let G be SimpleGraph;

mode Vertex of G is Element of Vertices G;

mode Edge of G is Element of Edges G;

end;
mode Vertex of G is Element of Vertices G;

mode Edge of G is Element of Edges G;

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

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;

definition

let G be SimpleGraph;

let v be Element of Vertices G;

ex b_{1} being Subset of (Vertices G) st

for x being Element of Vertices G holds

( x in b_{1} iff {v,x} in Edges G )

for b_{1}, b_{2} being Subset of (Vertices G) st ( for x being Element of Vertices G holds

( x in b_{1} iff {v,x} in Edges G ) ) & ( for x being Element of Vertices G holds

( x in b_{2} iff {v,x} in Edges G ) ) holds

b_{1} = b_{2}

end;
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 for x being Element of Vertices G holds

( x in it iff {v,x} in Edges G );

ex b

for x being Element of Vertices G holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def8 defines Adjacent SCMYCIEL:def 8 :

for G being SimpleGraph

for v being Element of Vertices G

for b_{3} being Subset of (Vertices G) holds

( b_{3} = Adjacent v iff for x being Element of Vertices G holds

( x in b_{3} iff {v,x} in Edges G ) );

for G being SimpleGraph

for v being Element of Vertices G

for b

( b

( x in b

definition
end;

:: deftheorem Def9 defines SimpleGraph SCMYCIEL:def 9 :

for X being set

for b_{2} being SimpleGraph holds

( b_{2} is SimpleGraph of X iff Vertices b_{2} = X );

for X being set

for b

( b

definition

let X be set ;

{ V where V is finite Subset of X : card V <= 2 } is SimpleGraph of X

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

{ V where V is finite Subset of X : card V <= 2 } is SimpleGraph of X

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

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)

{x,y} in G ) holds

G = CompleteSGraph (Vertices G)

proof end;

registration
end;

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

coherence

(CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph;

by Lm3;

involutiveness

for b_{1}, b_{2} being SimpleGraph st b_{1} = (CompleteSGraph (Vertices b_{2})) \ (Edges b_{2}) holds

b_{2} = (CompleteSGraph (Vertices b_{1})) \ (Edges b_{1})
by Lm6;

end;
func Complement G -> SimpleGraph equals :: SCMYCIEL:def 11

(CompleteSGraph (Vertices G)) \ (Edges G);

correctness (CompleteSGraph (Vertices G)) \ (Edges G);

coherence

(CompleteSGraph (Vertices G)) \ (Edges G) is SimpleGraph;

by Lm3;

involutiveness

for b

b

:: deftheorem defines Complement SCMYCIEL:def 11 :

for G being SimpleGraph holds Complement G = (CompleteSGraph (Vertices G)) \ (Edges G);

for G being SimpleGraph holds Complement G = (CompleteSGraph (Vertices G)) \ (Edges G);

theorem :: SCMYCIEL:41

definition
end;

:: deftheorem defines SubgraphInducedBy SCMYCIEL:def 12 :

for G being SimpleGraph

for L being set holds G SubgraphInducedBy L = G /\ (bool L);

for G being SimpleGraph

for L being set holds G SubgraphInducedBy L = G /\ (bool L);

registration
end;

theorem Th43: :: SCMYCIEL:43

for G being SimpleGraph

for L being set holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ (Vertices G))

for L being set holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ (Vertices G))

proof end;

registration
end;

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

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;

:: deftheorem Def13 defines clique SCMYCIEL:def 13 :

for G being SimpleGraph holds

( G is clique iff G = CompleteSGraph (Vertices G) );

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

{x,y} in Edges G ) holds

G is clique

proof end;

registration

ex b_{1} being SimpleGraph st b_{1} is clique
by Th48;

let G be SimpleGraph;

ex b_{1} being Subgraph of G st b_{1} is clique
end;

cluster non empty V38() finite-membered V242() V277() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for set ;

existence ex b

let G be SimpleGraph;

cluster non empty V38() finite-membered V242() V277() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for Element of bool G;

existence ex b

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

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;

ex b_{1} being Clique of G st b_{1} is finite

end;
cluster non empty V38() finite finite-membered V242() V277() subset-closed 1 -at_most_dimensional SimpleGraph-like clique for Element of bool G;

existence ex b

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

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

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;

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

ex C being finite Clique of G st

for D being finite Clique of G holds order D <= order C;

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

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

ex b_{1} being SimpleGraph st b_{1} is with_finite_clique#
end;

cluster non empty V38() finite-membered V242() V277() subset-closed 1 -at_most_dimensional SimpleGraph-like with_finite_clique# for set ;

existence ex b

proof end;

registration

coherence

for b_{1} being SimpleGraph st b_{1} is finite holds

b_{1} is with_finite_clique#

end;
for b

b

proof end;

definition

let G be with_finite_clique# SimpleGraph;

ex b_{1} being Nat st

( ex C being finite Clique of G st order C = b_{1} & ( for T being finite Clique of G holds order T <= b_{1} ) )

for b_{1}, b_{2} being Nat st ex C being finite Clique of G st order C = b_{1} & ( for T being finite Clique of G holds order T <= b_{1} ) & ex C being finite Clique of G st order C = b_{2} & ( for T being finite Clique of G holds order T <= b_{2} ) holds

b_{1} = b_{2}

end;
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 C being finite Clique of G st order C = it & ( for T being finite Clique of G holds order T <= it ) );

ex b

( ex C being finite Clique of G st order C = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines clique# SCMYCIEL:def 15 :

for G being with_finite_clique# SimpleGraph

for b_{2} being Nat holds

( b_{2} = clique# G iff ( ex C being finite Clique of G st order C = b_{2} & ( for T being finite Clique of G holds order T <= b_{2} ) ) );

for G being with_finite_clique# SimpleGraph

for b

( b

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

for x, y being set st {x,y} in G holds

G SubgraphInducedBy {x,y} is Clique of G

proof end;

definition

let G be SimpleGraph;

let P be a_partition of Vertices G;

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

for x being set st x in P holds

G SubgraphInducedBy x is Clique of G;

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

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;

correctness

existence

ex b_{1} being a_partition of Vertices G st b_{1} is Clique-wise ;

end;
correctness

existence

ex b

proof end;

definition
end;

registration

let G be void SimpleGraph;

correctness

coherence

for b_{1} being a_partition of Vertices G st b_{1} is empty holds

b_{1} is Clique-wise ;

;

end;
correctness

coherence

for b

b

;

definition

let G be SimpleGraph;

end;
attr G is with_finite_cliquecover# means :Def17: :: SCMYCIEL:def 17

ex C being Clique-partition of G st C is finite ;

ex C being Clique-partition of G st C is finite ;

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

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 b_{1} being SimpleGraph st b_{1} is finite holds

b_{1} is with_finite_cliquecover# ;

end;
coherence

for b

b

proof end;

registration

let G be with_finite_cliquecover# SimpleGraph;

correctness

existence

ex b_{1} being Clique-partition of G st b_{1} is finite ;

by Def17;

end;
correctness

existence

ex b

by Def17;

registration

let G be with_finite_cliquecover# SimpleGraph;

let S be Subset of (Vertices G);

correctness

coherence

G SubgraphInducedBy S is with_finite_cliquecover# ;

end;
let S be Subset of (Vertices G);

correctness

coherence

G SubgraphInducedBy S is with_finite_cliquecover# ;

proof end;

definition

let G be with_finite_cliquecover# SimpleGraph;

ex b_{1} being Nat st

( ex C being finite Clique-partition of G st card C = b_{1} & ( for C being finite Clique-partition of G holds b_{1} <= card C ) )

for b_{1}, b_{2} being Nat st ex C being finite Clique-partition of G st card C = b_{1} & ( for C being finite Clique-partition of G holds b_{1} <= card C ) & ex C being finite Clique-partition of G st card C = b_{2} & ( for C being finite Clique-partition of G holds b_{2} <= card C ) holds

b_{1} = b_{2}

end;
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 C being finite Clique-partition of G st card C = it & ( for C being finite Clique-partition of G holds it <= card C ) );

ex b

( ex C being finite Clique-partition of G st card C = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines cliquecover# SCMYCIEL:def 18 :

for G being with_finite_cliquecover# SimpleGraph

for b_{2} being Nat holds

( b_{2} = cliquecover# G iff ( ex C being finite Clique-partition of G st card C = b_{2} & ( for C being finite Clique-partition of G holds b_{2} <= card C ) ) );

for G being with_finite_cliquecover# SimpleGraph

for b

( b

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

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

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;

coherence

for b_{1} being Subset of (Vertices G) st b_{1} is trivial holds

b_{1} is stable

end;
coherence

for b

b

proof end;

registration
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

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;

registration
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

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;

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

for x being set st x in P holds

x is StableSet of G;

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

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

registration

let G be SimpleGraph;

existence

ex b_{1} being a_partition of Vertices G st b_{1} is StableSet-wise

end;
existence

ex b

proof end;

definition
end;

definition

let G be SimpleGraph;

end;
attr G is finitely_colorable means :Def21: :: SCMYCIEL:def 21

ex C being Coloring of G st C is finite ;

ex C being Coloring of G st C is finite ;

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

for G being SimpleGraph holds

( G is finitely_colorable iff ex C being Coloring of G st C is finite );

registration

ex b_{1} being SimpleGraph st b_{1} is finitely_colorable
end;

cluster non empty V38() finite-membered V242() V277() subset-closed 1 -at_most_dimensional SimpleGraph-like finitely_colorable for set ;

existence ex b

proof end;

registration

correctness

coherence

for b_{1} being SimpleGraph st b_{1} is finite holds

b_{1} is finitely_colorable ;

end;
coherence

for b

b

proof end;

registration

let G be finitely_colorable SimpleGraph;

existence

ex b_{1} being Coloring of G st b_{1} is finite
by Def21;

end;
existence

ex b

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

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)

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 ;

coherence

G SubgraphInducedBy S is finitely_colorable

end;
let S be set ;

coherence

G SubgraphInducedBy S is finitely_colorable

proof end;

definition

let G be finitely_colorable SimpleGraph;

ex b_{1} being Nat st

( ex C being finite Coloring of G st card C = b_{1} & ( for C being finite Coloring of G holds b_{1} <= card C ) )

for b_{1}, b_{2} being Nat st ex C being finite Coloring of G st card C = b_{1} & ( for C being finite Coloring of G holds b_{1} <= card C ) & ex C being finite Coloring of G st card C = b_{2} & ( for C being finite Coloring of G holds b_{2} <= card C ) holds

b_{1} = b_{2}

end;
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 C being finite Coloring of G st card C = it & ( for C being finite Coloring of G holds it <= card C ) );

ex b

( ex C being finite Coloring of G st card C = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def22 defines chromatic# SCMYCIEL:def 22 :

for G being finitely_colorable SimpleGraph

for b_{2} being Nat holds

( b_{2} = chromatic# G iff ( ex C being finite Coloring of G st card C = b_{2} & ( for C being finite Coloring of G holds b_{2} <= card C ) ) );

for G being finitely_colorable SimpleGraph

for b

( b

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

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;

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

ex A being finite StableSet of G st

for B being finite StableSet of G holds card B <= card A;

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

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 b_{1} being SimpleGraph st b_{1} is finite holds

b_{1} is with_finite_stability# ;

end;
coherence

for b

b

proof end;

registration

let G be with_finite_stability# SimpleGraph;

correctness

coherence

for b_{1} being StableSet of G holds b_{1} is finite ;

end;
correctness

coherence

for b

proof end;

registration

ex b_{1} being SimpleGraph st

( b_{1} is with_finite_stability# & not b_{1} is void )
end;

cluster non empty V38() finite-membered V242() V277() subset-closed non void 1 -at_most_dimensional SimpleGraph-like with_finite_stability# for set ;

existence ex b

( b

proof end;

definition

let G be with_finite_stability# SimpleGraph;

ex b_{1} being Nat st

( ex A being finite StableSet of G st card A = b_{1} & ( for T being finite StableSet of G holds card T <= b_{1} ) )

for b_{1}, b_{2} being Nat st ex A being finite StableSet of G st card A = b_{1} & ( for T being finite StableSet of G holds card T <= b_{1} ) & ex A being finite StableSet of G st card A = b_{2} & ( for T being finite StableSet of G holds card T <= b_{2} ) holds

b_{1} = b_{2}

end;
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 A being finite StableSet of G st card A = it & ( for T being finite StableSet of G holds card T <= it ) );

ex b

( ex A being finite StableSet of G st card A = b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def24 defines stability# SCMYCIEL:def 24 :

for G being with_finite_stability# SimpleGraph

for b_{2} being Nat holds

( b_{2} = stability# G iff ( ex A being finite StableSet of G st card A = b_{2} & ( for T being finite StableSet of G holds card T <= b_{2} ) ) );

for G being with_finite_stability# SimpleGraph

for b

( b

registration

let G be non void with_finite_stability# SimpleGraph;

correctness

coherence

stability# G is positive ;

end;
correctness

coherence

stability# G is positive ;

proof end;

registration

correctness

coherence

for b_{1} being SimpleGraph st b_{1} is with_finite_clique# & b_{1} is with_finite_stability# holds

b_{1} is finite ;

end;
coherence

for b

b

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)

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

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;

correctness

coherence

Complement G is with_finite_stability# ;

end;
correctness

coherence

Complement G is with_finite_stability# ;

proof end;

registration

let G be with_finite_stability# SimpleGraph;

correctness

coherence

Complement G is with_finite_clique# ;

end;
correctness

coherence

Complement G is with_finite_clique# ;

proof end;

registration

let G be finitely_colorable SimpleGraph;

correctness

coherence

Complement G is with_finite_cliquecover# ;

end;
correctness

coherence

Complement G is with_finite_cliquecover# ;

proof end;

registration

let G be with_finite_cliquecover# SimpleGraph;

correctness

coherence

Complement G is finitely_colorable ;

end;
correctness

coherence

Complement G is finitely_colorable ;

proof end;

definition

let G be SimpleGraph;

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;

end;
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 ((({{}} \/ { {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 } ;

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;

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

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

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;

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

for D being finite Clique of (Mycielskian G) holds order D <= clique# G

proof end;

registration
end;

theorem Th110: :: SCMYCIEL:110

for G being with_finite_clique# SimpleGraph st 2 <= clique# G holds

clique# (Mycielskian G) = clique# G

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

definition

let G be SimpleGraph;

ex b_{1} being ManySortedSet of NAT ex myc being Function st

( b_{1} = myc & myc . 0 = G & ( for k being Nat

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) )

for b_{1}, b_{2} being ManySortedSet of NAT st ex myc being Function st

( b_{1} = 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_{2} = myc & myc . 0 = G & ( for k being Nat

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) ) holds

b_{1} = b_{2}

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

ex b

( b

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) )

proof end;

uniqueness for b

( b

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) ) & ex myc being Function st

( b

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) ) holds

b

proof end;

:: deftheorem Def26 defines MycielskianSeq SCMYCIEL:def 26 :

for G being SimpleGraph

for b_{2} being ManySortedSet of NAT holds

( b_{2} = MycielskianSeq G iff ex myc being Function st

( b_{2} = myc & myc . 0 = G & ( for k being Nat

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) ) );

for G being SimpleGraph

for b

( b

( b

for G being SimpleGraph st G = myc . k holds

myc . (k + 1) = Mycielskian G ) ) );

registration
end;

theorem Th115: :: SCMYCIEL:115

for G, H being SimpleGraph

for n being Nat holds (MycielskianSeq G) . (n + 1) = Mycielskian ((MycielskianSeq G) . n)

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;

coherence

(MycielskianSeq G) . n is with_finite_clique#

end;
let n be Nat;

coherence

(MycielskianSeq G) . n is with_finite_clique#

proof end;

registration

let G be finitely_colorable SimpleGraph;

let n be Nat;

coherence

(MycielskianSeq G) . n is finitely_colorable

end;
let n be Nat;

coherence

(MycielskianSeq G) . n is finitely_colorable

proof end;

registration
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

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)

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 )

( clique# ((MycielskianSeq (CompleteSGraph 2)) . n) = 2 & chromatic# ((MycielskianSeq (CompleteSGraph 2)) . n) = n + 2 )

proof end;