:: Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received February 8, 2012
:: Copyright (c) 2012-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies MATROID0, NAT_1, FINSET_1, CARD_1, ARYTM_3, SUBSET_1, XXREAL_0,
CLASSES1, SGRAPH1, SIMPLEX0, TARSKI, GRAPH_1, GLIB_000, PBOOLE, XBOOLE_0,
ZFMISC_1, NUMBERS, FUNCT_1, RELAT_1, COMBGRAS, MYCIELSK, DILWORTH,
CIRCUIT2, AOFA_000, EQREL_1, PEPIN, CIRCUIT1, FUNCT_2, ARYTM_1, PROB_1,
BSPACE, STRUCT_0, NEWTON, STIRL2_1, UPROOTS, FINSEQ_1, CARD_3, FINSEQ_2,
PROB_2, GROUP_10, RAMSEY_1, SCMYCIEL;
notations TARSKI, XBOOLE_0, ORDINAL1, RELAT_1, FUNCT_1, FUNCT_2, MATROID0,
XCMPLX_0, NAT_1, FINSET_1, ENUMSET1, FINSEQ_1, FINSEQ_2, CARD_1,
SUBSET_1, XXREAL_0, ZFMISC_1, NUMBERS, NEWTON, UPROOTS, RVSUM_1, PROB_2,
FUNCOP_1, CLASSES1, AOFA_000, EQREL_1, BSPACE, STIRL2_1, PBOOLE,
CARD_LAR, MYCIELSK, GROUP_10, RAMSEY_1, CARD_3;
constructors MATROID0, LEXBFS, UPROOTS, CARD_LAR, RVSUM_1, BSPACE, STIRL2_1,
BINOP_2, PROB_2, DOMAIN_1, CLASSES1, MYCIELSK, RAMSEY_1, RELSET_1,
COHSP_1;
registrations FINSET_1, XXREAL_0, ORDINAL1, SETFAM_1, RELSET_1, XREAL_0,
NAT_1, SUBSET_1, EQREL_1, CARD_1, NEWTON, VALUED_0, XBOOLE_0, PARTFUN1,
FUNCT_2, SIMPLEX0, MYCIELSK, ZFMISC_1, FINSEQ_1, COHSP_1, STIRL2_1;
requirements SUBSET, NUMERALS, REAL, ARITHM, BOOLE;
begin :: Preliminaries
:: Could not find in MML
theorem :: SCMYCIEL:1
for x being object, X being set holds not [x,X] in X;
theorem :: SCMYCIEL:2
for x, X being object holds [x,X] <> X;
theorem :: SCMYCIEL:3
for x, X being object holds [x,X] <> x;
theorem :: SCMYCIEL:4
for x1,y1,x2,y2 being object, X being set
st x1 in X & x2 in X & {x1,[y1,X]} = {x2,[y2,X]}
holds x1 = x2 & y1 = y2;
theorem :: SCMYCIEL:5 :: belongs to PENCIL_1
for X being set, v being object st 3 c= card X
ex v1, v2 being object st v1 in X & v2 in X & v1<>v & v2<>v & v1<>v2;
theorem :: SCMYCIEL:6
for x being set holds singletons {x} = { {x} };
registration
cluster finite-yielding for FinSequence;
end;
theorem :: SCMYCIEL:7
for X being non empty finite set, P being a_partition of X
st card P < card X
ex p being set, x, y being object st p in P & x in p & y in p & x <> y;
registration
cluster union {{}} -> empty;
end;
theorem :: SCMYCIEL:8
for x being set holds union { {}, {x} } = {x};
theorem :: SCMYCIEL:9 :: variant of SUBSET_1:46 or CARD_1:65
for X being set, s being Subset of X
st s is 1-element
ex x being set st x in X & s = {x};
theorem :: SCMYCIEL:10
for X being set holds
card { {X,[x,X]} where x is Element of X : x in X } = card X;
definition
let G be set;
func PairsOf G -> Subset of G means
:: SCMYCIEL:def 1
for e being set holds e in it iff e in G & card e = 2;
end;
theorem :: SCMYCIEL:11
for X being set, e being set
st e in PairsOf X
ex x, y being set st x <> y & x in union X & y in union X & e = {x, y};
theorem :: SCMYCIEL:12
for X being set, x, y being object st x <> y & {x, y} in X
holds {x, y} in PairsOf X;
theorem :: SCMYCIEL:13
for X being set, x, y being object
st {x, y} in PairsOf X holds x <> y & x in union X & y in union X;
theorem :: SCMYCIEL:14
for G, H being set st G c= H holds PairsOf G c= PairsOf H;
theorem :: 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;
theorem :: SCMYCIEL:16 :: ordunordpairs:
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;
registration
let X be finite set;
cluster PairsOf X -> finite;
end;
definition
let X be set;
attr X is void means
:: SCMYCIEL:def 2
X = {{}};
end;
registration
cluster void for set;
end;
registration
cluster void -> finite for set;
end;
registration
let G be void set;
cluster union G -> empty;
end;
theorem :: SCMYCIEL:17
for X being set st X is void holds PairsOf X = {};
theorem :: SCMYCIEL:18
for X being set st union X = {} holds X = {} or X = {{}};
definition
let X be set;
attr X is pairfree means
:: SCMYCIEL:def 3
PairsOf X is empty;
end;
theorem :: SCMYCIEL:19
for X, x being set st card union X = 1 holds X is pairfree;
registration
cluster finite-membered non empty for set;
end;
registration
let X be finite-membered set, Y be set;
cluster X /\ Y -> finite-membered;
cluster X \ Y -> finite-membered;
end;
begin :: Simple graphs as simplicial complexes
definition
let n be Nat;
let X be set;
attr X is n-at_most_dimensional means
:: SCMYCIEL:def 4
for x being set st x in X holds card x c= n+1;
end;
registration
let n be Nat;
cluster n-at_most_dimensional -> finite-membered for set;
end;
registration
let n be Nat;
cluster n-at_most_dimensional subset-closed non empty for set;
end;
theorem :: SCMYCIEL:20
for G being subset-closed non empty set holds {} in G;
theorem :: SCMYCIEL:21
for n being Nat, X being n-at_most_dimensional set,
x being Element of X
st x in X holds card x <= n+1;
registration
let n be Nat;
let X, Y be n-at_most_dimensional set;
cluster X \/ Y -> n-at_most_dimensional;
end;
registration
let n be Nat;
let X be n-at_most_dimensional set, Y be set;
cluster X /\ Y -> n-at_most_dimensional;
cluster X \ Y -> n-at_most_dimensional;
end;
registration
let n be Nat, X be n-at_most_dimensional set;
cluster -> n-at_most_dimensional for Subset of X;
end;
definition
let s be set;
attr s is SimpleGraph-like means
:: SCMYCIEL:def 5
s is 1-at_most_dimensional subset-closed non empty;
end;
registration
cluster SimpleGraph-like ->
1-at_most_dimensional subset-closed non empty for set;
cluster 1-at_most_dimensional subset-closed non empty
-> SimpleGraph-like for set;
end;
theorem :: SCMYCIEL:22
{{}} is SimpleGraph-like;
registration
cluster {{}} -> SimpleGraph-like;
end;
registration
cluster SimpleGraph-like for set;
end;
definition
mode SimpleGraph is SimpleGraph-like set;
end;
registration
cluster void for SimpleGraph;
cluster finite for SimpleGraph;
end;
notation :: meant for graphs
let G be set;
synonym Vertices G for union G;
synonym Edges G for PairsOf G;
end;
notation
let X be set;
synonym X is edgeless for X is pairfree;
end;
theorem :: SCMYCIEL:23
for G being SimpleGraph st Vertices G is finite holds G is finite;
theorem :: SCMYCIEL:24
for G being SimpleGraph, x being object holds x in Vertices G iff {x} in G;
theorem :: SCMYCIEL:25
for x being set holds { {}, {x} } is SimpleGraph;
definition :: meant for graphs
let X be finite finite-membered set;
func order X -> Nat equals
:: SCMYCIEL:def 6
card union X;
end;
definition :: meant for graphs
let X be finite set;
func size X -> Nat equals
:: SCMYCIEL:def 7
card PairsOf X;
end;
theorem :: SCMYCIEL:26
for G being finite SimpleGraph holds order G <= card G;
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 :: SCMYCIEL:27
for G being SimpleGraph holds G = { {} } \/ singletons Vertices G \/ Edges G;
theorem :: SCMYCIEL:28
for G being SimpleGraph st Vertices G = {} holds G is void;
theorem :: SCMYCIEL:29
for G being SimpleGraph, x being set
st x in G & x <> {}
holds (ex y being set st x = {y} & y in Vertices G) or x in Edges G;
theorem :: SCMYCIEL:30 :: Gsingle:
for G being SimpleGraph, x being set st Vertices G = {x} holds G = { {}, {x} };
theorem :: SCMYCIEL:31
for X being set ex G being SimpleGraph st G is edgeless & Vertices G = X;
definition
let G be SimpleGraph, v be Element of Vertices G;
func Adjacent v -> Subset of Vertices G means
:: SCMYCIEL:def 8
for x being Element of Vertices G holds x in it iff {v, x} in Edges G;
end;
definition
let X be set;
mode SimpleGraph of X -> SimpleGraph means
:: SCMYCIEL:def 9
Vertices it = X;
end;
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};
end;
theorem :: 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;
registration
let X be finite set;
cluster CompleteSGraph X -> finite;
end;
theorem :: SCMYCIEL:33
for X being set, x being set st x in X holds {x} in CompleteSGraph X;
theorem :: SCMYCIEL:34
for X being set, x, y being set st x in X & y in X
holds {x,y} in CompleteSGraph X;
theorem :: SCMYCIEL:35
CompleteSGraph {} = {{}};
theorem :: SCMYCIEL:36
for x being set holds CompleteSGraph {x} = {{},{x}};
theorem :: SCMYCIEL:37
for x, y being set holds CompleteSGraph {x,y} = {{},{x},{y},{x,y}};
theorem :: SCMYCIEL:38
for X, Y being set st X c= Y holds CompleteSGraph X c= CompleteSGraph Y;
theorem :: SCMYCIEL:39
for G being SimpleGraph, x being set st x in Vertices G
holds CompleteSGraph {x} c= G;
registration
let G be SimpleGraph;
cluster SimpleGraph-like for Subset of G;
end;
definition
let G be SimpleGraph;
mode Subgraph of G is SimpleGraph-like Subset of G;
end;
definition
let G be SimpleGraph;
func Complement G -> SimpleGraph equals
:: SCMYCIEL:def 11
(CompleteSGraph Vertices G) \ Edges G;
involutiveness;
end;
theorem :: SCMYCIEL:40 :: Compl1:
for G being SimpleGraph holds Vertices G = Vertices Complement G;
theorem :: SCMYCIEL:41 :: Compl1a:
for G being SimpleGraph, 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;
begin :: Induced Subgraphs
definition
let G be SimpleGraph, L be set;
func G SubgraphInducedBy L -> Subset of G equals
:: SCMYCIEL:def 12
G /\ bool L;
end;
registration
let G be SimpleGraph, L be set;
cluster G SubgraphInducedBy L -> SimpleGraph-like;
end;
theorem :: SCMYCIEL:42 :: Sub3b:
for G being SimpleGraph holds G = G SubgraphInducedBy Vertices G;
theorem :: SCMYCIEL:43
for G being SimpleGraph, L being set
holds G SubgraphInducedBy L = G SubgraphInducedBy (L /\ Vertices G);
registration
let G be finite SimpleGraph, L be set;
cluster G SubgraphInducedBy L -> finite;
end;
registration
let G be SimpleGraph, L be finite set;
cluster G SubgraphInducedBy L -> finite;
end;
theorem :: SCMYCIEL:44
for G, H being SimpleGraph
st G c= H holds G c= H SubgraphInducedBy Vertices G;
theorem :: SCMYCIEL:45
for G being SimpleGraph, L being set
holds Vertices (G SubgraphInducedBy L) = (Vertices G) /\ L;
theorem :: SCMYCIEL:46
for G being SimpleGraph, x being set
st x in Vertices G holds G SubgraphInducedBy {x} = { {}, {x} };
begin :: Clique, clique number, clique cover
definition
let G be SimpleGraph;
attr G is clique means
:: SCMYCIEL:def 13
G = CompleteSGraph Vertices G;
end;
theorem :: 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;
theorem :: SCMYCIEL:48
{{}} is clique;
registration
cluster clique for SimpleGraph;
let G be SimpleGraph;
cluster clique for Subgraph of G;
end;
definition
let G be SimpleGraph;
mode Clique of G is clique Subgraph of G;
end;
theorem :: SCMYCIEL:49
for X being set holds (CompleteSGraph X) is clique;
registration
let X be set;
cluster CompleteSGraph X -> clique;
end;
theorem :: SCMYCIEL:50
for G being SimpleGraph, x being set st x in Vertices G
holds { {}, {x} } is Clique of G;
theorem :: SCMYCIEL:51
for G being SimpleGraph, 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;
registration
let G be SimpleGraph;
cluster finite for Clique of G;
end;
theorem :: SCMYCIEL:52
for G being SimpleGraph, x being set st x in union G
ex C being finite Clique of G st Vertices C = {x};
theorem :: SCMYCIEL:53
for C being clique SimpleGraph, u, v being set
st u in Vertices C & v in Vertices C holds {u, v} in C;
definition
let G be SimpleGraph;
attr G is with_finite_clique# means
:: SCMYCIEL:def 14
ex C being finite Clique of G
st for D being finite Clique of G holds order D <= order C;
end;
registration
cluster with_finite_clique# for SimpleGraph;
end;
registration
cluster finite -> with_finite_clique# for SimpleGraph;
end;
definition
let G be with_finite_clique# SimpleGraph;
func clique# G -> Nat means
:: 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;
end;
theorem :: SCMYCIEL:54
for G being with_finite_clique# SimpleGraph
st clique# G = 0 holds Vertices G = {};
theorem :: SCMYCIEL:55
for G being void SimpleGraph holds clique# G = 0;
theorem :: SCMYCIEL:56
for G being SimpleGraph, x, y being set
st {x,y} in G holds G SubgraphInducedBy {x,y} is Clique of G;
theorem :: SCMYCIEL:57
for G being with_finite_clique# SimpleGraph
st Edges G <> {} holds clique# G >= 2;
theorem :: SCMYCIEL:58 :: CliqueSubno0:
for G, H being with_finite_clique# SimpleGraph
st G c= H holds clique# G <= clique# H;
theorem :: SCMYCIEL:59
for X being finite set holds clique# CompleteSGraph X = card X;
definition
let G be SimpleGraph, P be a_partition of Vertices G;
attr P is Clique-wise means
:: SCMYCIEL:def 16
for x being set st x in P holds G SubgraphInducedBy x is Clique of G;
end;
registration
let G be SimpleGraph;
cluster Clique-wise for a_partition of Vertices G;
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;
end;
definition
let G be SimpleGraph;
attr G is with_finite_cliquecover# means
:: SCMYCIEL:def 17
ex C being Clique-partition of G st C is finite;
end;
registration
cluster finite -> with_finite_cliquecover# for SimpleGraph;
end;
registration
let G be with_finite_cliquecover# SimpleGraph;
cluster finite for Clique-partition of G;
end;
registration
let G be with_finite_cliquecover# SimpleGraph, S be Subset of Vertices G;
cluster G SubgraphInducedBy S -> with_finite_cliquecover#;
end;
definition
let G be with_finite_cliquecover# SimpleGraph;
func cliquecover# G -> Nat means
:: 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;
end;
begin :: Stable set, coloring
definition
let G be SimpleGraph, S be Subset of Vertices G;
attr S is stable means
:: SCMYCIEL:def 19
for x, y being set st x <> y & x in S & y in S holds {x,y} nin G;
end;
theorem :: SCMYCIEL:60
for G being SimpleGraph holds {}(Vertices G) is stable;
theorem :: SCMYCIEL:61
for G being SimpleGraph, S being Subset of Vertices G, v being object
st S = {v} holds S is stable;
registration
let G be SimpleGraph;
cluster trivial -> stable for Subset of Vertices G;
end;
registration
let G be SimpleGraph;
cluster stable for Subset of Vertices G;
end;
definition
let G be SimpleGraph;
mode StableSet of G is stable Subset of Vertices G;
:: other possible names: AntiChain of R, IndependentSet of R
end;
theorem :: SCMYCIEL:62
for G being SimpleGraph, x, y being set
st x in Vertices G & y in Vertices G & {x,y} nin G
holds {x, y} is StableSet of G;
theorem :: SCMYCIEL:63 :: Height4:
for G being with_finite_clique# SimpleGraph st clique# G = 1
holds Vertices G is StableSet of G;
registration
let G be SimpleGraph;
cluster finite for StableSet of G;
end;
theorem :: SCMYCIEL:64 :: AChain0:
for G being SimpleGraph, A being StableSet of G, B being Subset of A
holds B is StableSet of G;
definition
let G be SimpleGraph, P be a_partition of Vertices G;
attr P is StableSet-wise means
:: SCMYCIEL:def 20
for x being set st x in P holds x is StableSet of G;
end;
theorem :: SCMYCIEL:65
for G being SimpleGraph holds SmallestPartition Vertices G is StableSet-wise;
registration
let G be SimpleGraph;
cluster StableSet-wise for a_partition of Vertices G;
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
:: SCMYCIEL:def 21
ex C being Coloring of G st C is finite;
end;
registration
cluster finitely_colorable for SimpleGraph;
end;
registration
cluster finite -> finitely_colorable for SimpleGraph;
end;
registration
let G be finitely_colorable SimpleGraph;
cluster finite for Coloring of G;
end;
theorem :: SCMYCIEL:66
for G being SimpleGraph, S being Clique of G, L being set
st L c= Vertices S holds G SubgraphInducedBy L is Clique of G;
theorem :: SCMYCIEL:67
for G being SimpleGraph, C being Coloring of G, S being Subset of Vertices G
holds C | S is Coloring of (G SubgraphInducedBy S);
registration
let G be finitely_colorable SimpleGraph, S be set;
cluster G SubgraphInducedBy S -> finitely_colorable;
end;
definition
let G be finitely_colorable SimpleGraph;
func chromatic# G -> Nat means
:: 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;
end;
theorem :: SCMYCIEL:68
for G, H being finitely_colorable SimpleGraph
st G c= H holds chromatic# G <= chromatic# H;
theorem :: SCMYCIEL:69
for X being finite set holds chromatic# CompleteSGraph X = card X;
theorem :: SCMYCIEL:70
for G being finitely_colorable SimpleGraph,
C being finite Coloring of G, c being set
st c in C & card C = chromatic# G
ex v being Element of Vertices G st v in c &
for d being Element of C st d <> c
ex w being Element of Vertices G st w in Adjacent(v) & w in d;
definition
let G be SimpleGraph;
attr G is with_finite_stability# means
:: SCMYCIEL:def 23
ex A being finite StableSet of G
st for B being finite StableSet of G holds card B <= card A;
end;
registration
cluster finite -> with_finite_stability# for SimpleGraph;
end;
registration
let G be with_finite_stability# SimpleGraph;
cluster -> finite for StableSet of G;
end;
registration
cluster with_finite_stability# non void for SimpleGraph;
end;
definition
let G be with_finite_stability# SimpleGraph;
func stability# G -> Nat means
:: 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;
end;
registration
let G be with_finite_stability# non void SimpleGraph;
cluster stability# G -> positive;
end;
theorem :: SCMYCIEL:71 :: Width4:
for G being with_finite_stability# SimpleGraph
st stability# G = 1 holds G is clique;
registration :: see analoguous in DILWORTH
:: I have done it through Ramsey. How else to prove it?
:: For posets one gets it directly from Dilworth.
cluster with_finite_clique# with_finite_stability# -> finite for SimpleGraph;
end;
theorem :: SCMYCIEL:72
for G being SimpleGraph, C being Clique of G
holds Vertices C is StableSet of Complement G;
theorem :: SCMYCIEL:73
for G being SimpleGraph, C being Clique of Complement G
holds Vertices C is StableSet of G;
theorem :: SCMYCIEL:74
for G being SimpleGraph, C being StableSet of G
holds (Complement G) SubgraphInducedBy C is Clique of Complement G;
theorem :: SCMYCIEL:75
for G being SimpleGraph, C being StableSet of Complement G
holds G SubgraphInducedBy C is Clique of G;
registration
let G be with_finite_clique# SimpleGraph;
cluster Complement G -> with_finite_stability#;
end;
registration
let G be with_finite_stability# SimpleGraph;
cluster Complement G -> with_finite_clique#;
end;
theorem :: SCMYCIEL:76
for G being with_finite_clique# SimpleGraph
holds clique# G = stability# Complement G;
theorem :: SCMYCIEL:77 :: staRcliCR:
for G being with_finite_stability# SimpleGraph
holds stability# G = clique# Complement G;
theorem :: SCMYCIEL:78
for G being SimpleGraph, C being Clique-partition of Complement G
holds C is Coloring of G;
theorem :: SCMYCIEL:79
for G being SimpleGraph, C being Clique-partition of G
holds C is Coloring of Complement G;
theorem :: SCMYCIEL:80
for G being SimpleGraph, C being Coloring of G
holds C is Clique-partition of Complement G;
theorem :: SCMYCIEL:81 :: ChrComplClico:
for G being SimpleGraph, C being Coloring of Complement G
holds C is Clique-partition of G;
registration
let G be finitely_colorable SimpleGraph;
cluster Complement G -> with_finite_cliquecover#;
end;
registration
let G be with_finite_cliquecover# SimpleGraph;
cluster Complement G -> finitely_colorable;
end;
theorem :: SCMYCIEL:82
for G being finitely_colorable SimpleGraph
holds chromatic# G = cliquecover# Complement G;
theorem :: SCMYCIEL:83 :: covRchrCR:
for G being with_finite_cliquecover# SimpleGraph
holds cliquecover# G = chromatic# Complement G;
begin :: Mycielskian of a graph
definition
let G be SimpleGraph;
func Mycielskian G -> SimpleGraph equals
:: SCMYCIEL:def 25
{ {} } \/
(the set of all {x}
where x is Element of (union G) \/ [:union G,{union G}:] \/ {union G})
\/
(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 };
end;
theorem :: SCMYCIEL:84 :: Mycielskian0:
for G being SimpleGraph holds G c= Mycielskian G;
theorem :: SCMYCIEL:85
for G being SimpleGraph, 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;
theorem :: SCMYCIEL:86
for G being SimpleGraph
holds Vertices Mycielskian G = union G \/ [:union G,{union G}:] \/ {union G};
theorem :: SCMYCIEL:87
for G being SimpleGraph holds union G in union Mycielskian G;
theorem :: SCMYCIEL:88
for G being void SimpleGraph holds Mycielskian G = {{},{union G}};
registration
let G be finite SimpleGraph;
cluster Mycielskian G -> finite;
end;
theorem :: SCMYCIEL:89
for G being finite SimpleGraph holds order Mycielskian G = 2*(order G) + 1;
theorem :: SCMYCIEL:90
for G being SimpleGraph, 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);
theorem :: 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 };
theorem :: SCMYCIEL:92
for G being finite SimpleGraph holds size Mycielskian G = 3*(size G) + order G;
theorem :: SCMYCIEL:93
for G being SimpleGraph, s, t being object
st {s, t} in Edges Mycielskian G
holds {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]);
theorem :: SCMYCIEL:94
for G being SimpleGraph, u being object
st { union G, u } in Edges Mycielskian G
ex x being object st x in union G & u = [x, union G];
theorem :: SCMYCIEL:95
for G being SimpleGraph, u being object
st u in Vertices G holds { [u, union G] } in Mycielskian G;
theorem :: SCMYCIEL:96
for G being SimpleGraph, u being set
st u in Vertices G holds { [u, union G], union G} in Mycielskian G;
theorem :: SCMYCIEL:97
for G being SimpleGraph, x, y being object
holds not {[x,union G],[y,union G]} in Edges Mycielskian G;
theorem :: SCMYCIEL:98
for G being SimpleGraph, x, y being object
st x <> y holds not {[x,union G],[y,union G]} in Mycielskian G;
theorem :: SCMYCIEL:99
for G being SimpleGraph, 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);
theorem :: SCMYCIEL:100
for G being SimpleGraph, x, y being set
st {[x,union G], y} in Mycielskian G holds x <> y;
theorem :: SCMYCIEL:101
for G being SimpleGraph, x, y being set
st y in union G & {[x,union G], y} in Mycielskian G holds {x, y} in G;
theorem :: SCMYCIEL:102
for G being SimpleGraph, x, y being set
st {x, y} in Edges G holds {[x,union G], y} in Mycielskian G;
theorem :: SCMYCIEL:103
for G being SimpleGraph, x, y being set
st x in Vertices G & y in Vertices G & {x, y} in Mycielskian G
holds {x, y} in G;
theorem :: SCMYCIEL:104
for G being SimpleGraph holds G = (Mycielskian G) SubgraphInducedBy Vertices G;
theorem :: SCMYCIEL:105
for G being SimpleGraph, C being finite Clique of Mycielskian G
st 3 <= order C for v being Vertex of C holds v <> union G;
theorem :: SCMYCIEL:106 :: MClique0
for G being with_finite_clique# SimpleGraph st clique# G = 0
for D being finite Clique of Mycielskian G holds order D <= 1;
theorem :: SCMYCIEL:107 :: MGsingle:
for G being SimpleGraph, x being set st Vertices G = {x}
holds Mycielskian G = {{},{x},{[x,union G]}, {union G}, {[x,union G],union G}};
theorem :: SCMYCIEL:108 :: MClique1
for G being with_finite_clique# SimpleGraph st clique# G = 1
for D being finite Clique of Mycielskian G holds order D <= 2;
theorem :: SCMYCIEL:109 :: MClique2
for G being with_finite_clique# SimpleGraph st 2 <= clique# G
for D being finite Clique of Mycielskian G holds order D <= clique# G;
registration
let G be with_finite_clique# SimpleGraph;
cluster Mycielskian G -> with_finite_clique#;
end;
theorem :: SCMYCIEL:110 :: MClique
for G being with_finite_clique# SimpleGraph
st 2 <= clique# G holds clique# Mycielskian G = clique# G;
theorem :: SCMYCIEL:111
for G being finitely_colorable SimpleGraph
ex E being Coloring of Mycielskian G st card E = 1 + chromatic# G;
registration
let G be finitely_colorable SimpleGraph;
cluster Mycielskian G -> finitely_colorable;
end;
theorem :: SCMYCIEL:112
for G being finitely_colorable SimpleGraph
holds chromatic# Mycielskian G = 1 + chromatic# G;
definition
let G be SimpleGraph;
func MycielskianSeq G -> ManySortedSet of NAT means
:: SCMYCIEL:def 26
ex myc being Function
st it = myc & myc.0 = G &
for k being Nat, G being SimpleGraph
st G = myc.k holds myc.(k+1) = Mycielskian G;
end;
theorem :: SCMYCIEL:113
for G being SimpleGraph holds (MycielskianSeq G).0 = G;
theorem :: SCMYCIEL:114
for G being SimpleGraph, n be Nat holds (MycielskianSeq G).n is SimpleGraph;
registration
let G be SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> SimpleGraph-like;
end;
theorem :: SCMYCIEL:115
for G, H being SimpleGraph, n be Nat
holds (MycielskianSeq G).(n+1) = Mycielskian (MycielskianSeq G).n;
registration
let G be with_finite_clique# SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> with_finite_clique#;
end;
registration
let G be finitely_colorable SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> finitely_colorable;
end;
registration
let G be finite SimpleGraph, n be Nat;
cluster (MycielskianSeq G).n -> finite;
end;
theorem :: SCMYCIEL:116
for G being finite SimpleGraph, n being Nat
holds order ((MycielskianSeq G).n) = 2|^n*(order G) + 2|^n - 1;
theorem :: SCMYCIEL:117 :: MSnsize:
for G being finite SimpleGraph, n being Nat
holds size (MycielskianSeq G).n
= 3|^n*(size G) + (3|^n - 2|^n)*(order G) + (n+1) block 3;
theorem :: SCMYCIEL:118
for n being Nat
holds clique# ((MycielskianSeq CompleteSGraph 2).n) = 2 &
chromatic# ((MycielskianSeq CompleteSGraph 2).n) = n+2;
theorem :: SCMYCIEL:119
for n being Nat
ex G being finite SimpleGraph st clique# G = 2 & chromatic# G > n;
theorem :: SCMYCIEL:120
for n being Nat
ex G being finite SimpleGraph st stability# G = 2 & cliquecover# G > n;