:: The {M}ycielskian of a Graph
:: by Piotr Rudnicki and Lorna Stewart
::
:: Received July 2, 2010
:: Copyright (c) 2010-2016 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 MYCIELSK, FINSET_1, DILWORTH, CARD_1, ARYTM_3, ARYTM_1, FUNCT_1,
RELAT_1, RELAT_2, YELLOW_0, TARSKI, EQREL_1, CIRCUIT2, SUBSET_1,
COMBGRAS, NECKLACE, NEWTON, XXREAL_0, NAT_1, XBOOLE_0, ORDERS_2,
STRUCT_0, ZFMISC_1, FUNCT_2, NUMBERS, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, FINSET_1, SUBSET_1, STRUCT_0, ORDINAL1,
CARD_1, ORDERS_2, XCMPLX_0, XXREAL_0, XREAL_0, NAT_D, RELAT_1, RELSET_1,
RELAT_2, EQREL_1, FUNCT_1, FUNCT_2, NEWTON, YELLOW_0, NECKLACE, DILWORTH,
NUMBERS;
constructors NECKLACE, RELSET_1, NAT_1, NAT_D, NEWTON, YELLOW_0, DILWORTH,
DOMAIN_1;
registrations SUBSET_1, XBOOLE_0, STRUCT_0, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, CARD_1, RELSET_1, ORDINAL1, EQREL_1, NECKLA_3, FUNCT_2, FINSET_1,
DILWORTH, NEWTON, ORDERS_2;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
begin :: MML Remarks
:: Note: PUA2MSS1:11 can be now proven without non empty for X
:: See func P | S below
begin
theorem :: MYCIELSK:1 :: TimesM:
for x, y, z being Real st 0 <= x holds x*(y-'z) = x*y -' x*z;
theorem :: MYCIELSK:2 :: Nat0:
for x, y, z being Nat holds x in Segm y \ Segm z iff z <= x & x < y;
theorem :: MYCIELSK:3 :: U5s:
for A, B, C, D, E, X being set
st X c= A or X c= B or X c= C or X c= D or X c= E
holds X c= A \/ B \/ C \/ D \/ E;
theorem :: MYCIELSK:4 :: U5:
for A, B, C, D, E, x being set holds
x in A \/ B \/ C \/ D \/ E iff x in A or x in B or x in C or x in D or x in E;
theorem :: MYCIELSK:5 :: Sym0a:
for R being symmetric RelStr, x, y being set
st x in the carrier of R & y in the carrier of R &
[x,y] in the InternalRel of R
holds [y,x] in the InternalRel of R;
theorem :: MYCIELSK:6 :: Sym0:
for R being symmetric RelStr, x, y being Element of R st x <= y holds y <= x;
begin :: Partitions
theorem :: MYCIELSK:7 :: Partcard:
for X being set, P being a_partition of X holds card P c= card X;
definition
let X be set, P be a_partition of X, S be Subset of X;
func P | S -> a_partition of S equals
:: MYCIELSK:def 1
{x /\ S where x is Element of P: x meets S};
end;
registration
let X be set;
cluster finite for a_partition of X;
end;
registration
let X be set, P be finite a_partition of X, S be Subset of X;
cluster P | S -> finite;
end;
theorem :: MYCIELSK:8 :: Tpart0:
for X being set, P being finite a_partition of X, S being Subset of X
holds card (P | S) <= card P;
theorem :: MYCIELSK:9 :: Tpart1:
for X being set, P being finite a_partition of X, S being Subset of X
holds (for p being set st p in P holds p meets S)
iff card (P | S) = card P;
theorem :: MYCIELSK:10 :: Tsr0:
for R being RelStr, C being Coloring of R, S being Subset of R
holds C | S is Coloring of subrelstr S;
begin :: Chromatic number and clique cover number
:: This section could be moved to DILWORTH or better yet to some
:: article with preliminaries where RelStr represents a graph.
:: But then some stuff from NECKLACE would have to be moved.
:: I decided not to move stuff around until there is much more
:: material and then a bigger reorganisation would be in place
:: 2009.08.06
definition
let R be RelStr; :: finitely_colorable sounds better
attr R is with_finite_chromatic# means
:: MYCIELSK:def 2
ex C being Coloring of R st C is finite;
end;
registration
cluster with_finite_chromatic# for RelStr;
end;
registration
cluster finite -> with_finite_chromatic# for RelStr;
end;
registration
let R be with_finite_chromatic# RelStr;
cluster finite for Coloring of R;
end;
registration
let R be with_finite_chromatic# RelStr, S be Subset of R;
cluster subrelstr S -> with_finite_chromatic#;
end;
definition
let R be with_finite_chromatic# RelStr;
func chromatic# R -> Nat means
:: MYCIELSK:def 3
(ex C being finite Coloring of R st card C = it)
& for C being finite Coloring of R holds it <= card C;
end;
registration
let R be empty RelStr;
cluster chromatic# R -> empty;
end;
registration
let R be non empty with_finite_chromatic# RelStr;
cluster chromatic# R -> positive;
end;
definition
let R be RelStr;
attr R is with_finite_cliquecover# means
:: MYCIELSK:def 4
ex C being Clique-partition of R st C is finite;
end;
registration
cluster with_finite_cliquecover# for RelStr;
end;
registration
cluster finite -> with_finite_cliquecover# for RelStr;
end;
registration
let R be with_finite_cliquecover# RelStr;
cluster finite for Clique-partition of R;
end;
registration
let R be with_finite_cliquecover# RelStr, S be Subset of R;
cluster subrelstr S -> with_finite_cliquecover#;
end;
definition
let R be with_finite_cliquecover# RelStr;
func cliquecover# R -> Nat means
:: MYCIELSK:def 5
(ex C being finite Clique-partition of R st card C = it)
& for C being finite Clique-partition of R holds it <= card C;
end;
registration
let R be empty RelStr;
cluster cliquecover# R -> empty;
end;
registration
let R be non empty with_finite_cliquecover# RelStr;
cluster cliquecover# R -> positive;
end;
:: Note: for empty RelStr clique# = 0, stability# = 0, chromatic# = 0,
:: cliquecover# = 0 follows from clusters.
theorem :: MYCIELSK:11 :: Maxclique:
for R being finite RelStr holds clique# R <= card the carrier of R;
theorem :: MYCIELSK:12 :: Maxstability:
for R being finite RelStr holds stability# R <= card the carrier of R;
theorem :: MYCIELSK:13 :: Maxchromatic:
for R being finite RelStr holds chromatic# R <= card the carrier of R;
theorem :: MYCIELSK:14 :: Maxclicover:
for R being finite RelStr holds cliquecover# R <= card the carrier of R;
theorem :: MYCIELSK:15 :: CliChr:
:: more general than DILWORTH:50 for finite RelStr
for R being with_finite_clique# with_finite_chromatic# RelStr
holds clique# R <= chromatic# R;
theorem :: MYCIELSK:16 :: StaCov:
:: more general than DILWORTH:46 for finite RelStr
for R being with_finite_stability# with_finite_cliquecover# RelStr
holds stability# R <= cliquecover# R;
begin :: Complement
theorem :: MYCIELSK:17 :: DCompl:
for R being RelStr, x, y being Element of R,
a, b being Element of ComplRelStr R
st x = a & y = b & x <= y holds not a <= b;
theorem :: MYCIELSK:18 :: DCompl1:
for R being RelStr, x, y being Element of R,
a, b being Element of ComplRelStr R
st x = a & y = b & x <> y & x in the carrier of R & not a <= b holds x <= y;
registration
let R be finite RelStr;
cluster ComplRelStr R -> finite;
end;
theorem :: MYCIELSK:19 :: CliStaCompl:
for R being symmetric RelStr, C being Clique of R
holds C is StableSet of ComplRelStr R;
theorem :: MYCIELSK:20 :: CliComplSta:
for R being symmetric RelStr, C being Clique of ComplRelStr R
holds C is StableSet of R;
theorem :: MYCIELSK:21 :: StaCliCompl:
for R being RelStr, C being StableSet of R holds C is Clique of ComplRelStr R;
theorem :: MYCIELSK:22 :: StaComplCli:
for R being RelStr, C being StableSet of ComplRelStr R holds C is Clique of R;
registration
let R be with_finite_clique# RelStr;
cluster ComplRelStr R -> with_finite_stability#;
end;
registration
let R be with_finite_stability# symmetric RelStr;
cluster ComplRelStr R -> with_finite_clique#;
end;
theorem :: MYCIELSK:23 :: cliRstaCR:
for R being with_finite_clique# symmetric RelStr
holds clique# R = stability# ComplRelStr R;
theorem :: MYCIELSK:24 :: staRcliCR:
for R being with_finite_stability# symmetric RelStr
holds stability# R = clique# ComplRelStr R;
theorem :: MYCIELSK:25 :: ChrClicoCompl:
for R being RelStr, C being Coloring of R
holds C is Clique-partition of ComplRelStr R;
theorem :: MYCIELSK:26 :: ClicoComplChr:
for R being symmetric RelStr, C being Clique-partition of ComplRelStr R
holds C is Coloring of R;
theorem :: MYCIELSK:27 :: ClicoChrCompl:
for R being symmetric RelStr, C being Clique-partition of R
holds C is Coloring of ComplRelStr R;
theorem :: MYCIELSK:28 :: ChrComplClico:
for R being RelStr, C being Coloring of ComplRelStr R
holds C is Clique-partition of R;
registration
let R be with_finite_chromatic# RelStr;
cluster ComplRelStr R -> with_finite_cliquecover#;
end;
registration
let R be with_finite_cliquecover# symmetric RelStr;
cluster ComplRelStr R -> with_finite_chromatic#;
end;
theorem :: MYCIELSK:29 :: chrRcovCR:
for R being with_finite_chromatic# symmetric RelStr
holds chromatic# R = cliquecover# ComplRelStr R;
theorem :: MYCIELSK:30 :: covRchrCR:
for R being with_finite_cliquecover# symmetric RelStr
holds cliquecover# R = chromatic# ComplRelStr R;
begin :: Adjacent set
definition
let R be RelStr, v be Element of R;
func Adjacent v -> Subset of R means
:: MYCIELSK:def 6
for x being Element of R holds x in it iff x < v or v < x;
end;
theorem :: MYCIELSK:31 :: AdjCol:
for R being with_finite_chromatic# RelStr,
C being finite Coloring of R, c being set
st c in C & card C = chromatic# R
ex v being Element of R st v in c &
for d being Element of C st d <> c
ex w being Element of R st w in Adjacent(v) & w in d;
begin :: Natural numbers as vertices
definition
let n be Nat;
mode NatRelStr of n -> strict RelStr means
:: MYCIELSK:def 7
the carrier of it = n;
end;
registration
cluster -> empty for NatRelStr of 0;
end;
registration
let n be non zero Nat;
cluster -> non empty for NatRelStr of n;
end;
registration
let n be Nat;
cluster -> finite for NatRelStr of n;
cluster irreflexive for NatRelStr of n;
end;
definition
let n be Nat;
func CompleteRelStr n -> NatRelStr of n means
:: MYCIELSK:def 8
the InternalRel of it = [: n, n :] \ id n;
end;
theorem :: MYCIELSK:32 :: CRS:
for n being Nat, x,y being set
st x in n & y in n
holds [x,y] in the InternalRel of CompleteRelStr n iff x <> y;
registration
let n be Nat;
cluster CompleteRelStr n -> irreflexive symmetric;
end;
registration
let n be Nat;
cluster [#]CompleteRelStr n -> clique;
end;
theorem :: MYCIELSK:33 :: CompleteCli:
for n being Nat holds clique# CompleteRelStr n = n;
theorem :: MYCIELSK:34 :: CompleteSta:
for n being non zero Nat holds stability# CompleteRelStr n = 1;
theorem :: MYCIELSK:35 :: CompleteChr:
for n being Nat holds chromatic# CompleteRelStr n = n;
theorem :: MYCIELSK:36 :: CompleteClico
for n being non zero Nat holds cliquecover# CompleteRelStr n = 1;
begin :: Mycielskian of a graph
definition
let n be Nat, R be NatRelStr of n;
:: Note: no assumptions about R
func Mycielskian R -> NatRelStr of 2*n+1 means
:: MYCIELSK:def 9
the InternalRel of it =
(the InternalRel of R)
\/ { [x,y+n] where x, y is Element of NAT : [x,y] in the InternalRel of R }
\/ { [x+n,y] where x, y is Element of NAT : [x,y] in the InternalRel of R }
\/ [: {2*n}, 2*n \ n :]
\/ [: 2*n \ n, {2*n} :];
end;
theorem :: MYCIELSK:37 :: cMR0:
for n being Nat, R being NatRelStr of n
holds the carrier of R c= the carrier of Mycielskian R;
theorem :: MYCIELSK:38 :: iMR0:
for n being Nat, R being NatRelStr of n, x, y being Nat
st [x,y] in the InternalRel of Mycielskian R
holds x < n & y < n or x < n & n <= y & y < 2*n or n <= x & x < 2*n & y < n
or x = 2*n & n <= y & y < 2*n or n <= x & x < 2*n & y = 2*n;
theorem :: MYCIELSK:39 :: iMR1ba:
for n being Nat, R being NatRelStr of n
holds the InternalRel of R c= the InternalRel of Mycielskian R;
theorem :: MYCIELSK:40 :: iMR1b:
for n being Nat, R being NatRelStr of n, x, y being set
st x in Segm n & y in Segm n &
[x,y] in the InternalRel of Mycielskian R
holds [x,y] in the InternalRel of R;
theorem :: MYCIELSK:41 :: iMR1a:
for n being Nat, R being NatRelStr of n, x, y being Nat
st [x,y] in the InternalRel of R holds
[x,y+n] in the InternalRel of Mycielskian R
& [x+n,y] in the InternalRel of Mycielskian R;
theorem :: MYCIELSK:42 :: iMR1c:
for n being Nat, R being NatRelStr of n, x, y being Nat
st x in Segm n & [x,y+n] in the InternalRel of Mycielskian R
holds [x,y] in the InternalRel of R;
theorem :: MYCIELSK:43 :: iMR1d:
for n being Nat, R being NatRelStr of n, x, y being Nat
st y in Segm n & [x+n,y] in the InternalRel of Mycielskian R
holds [x,y] in the InternalRel of R;
theorem :: MYCIELSK:44 :: iMR1e:
for n being Nat, R being NatRelStr of n, m being Nat
st n <= m & m < 2*n
holds [m,2*n] in the InternalRel of Mycielskian R
& [2*n,m] in the InternalRel of Mycielskian R;
theorem :: MYCIELSK:45 :: Msubrel:
for n being Nat, R being NatRelStr of n, S being Subset of Mycielskian R
st S = n holds R = subrelstr S;
theorem :: MYCIELSK:46 :: MClique:
for n being Nat, R being irreflexive NatRelStr of n
st 2 <= clique# R holds clique# R = clique# Mycielskian R;
theorem :: MYCIELSK:47 :: Tchro0:
for R being with_finite_chromatic# RelStr, S being Subset of R
holds chromatic# R >= chromatic# subrelstr S;
theorem :: MYCIELSK:48
:: :: Mchromatic: :: even when n = 0 or n = 1 and then
:: Mycielskian n = 2 is compl(P_3) (Thanks Lorna)
:: and if we continue we have disconnected graphs.
for n being Nat, R being irreflexive NatRelStr of n
holds chromatic# Mycielskian R = 1 + chromatic# R;
definition
let n be Nat;
func Mycielskian n -> NatRelStr of 3*2|^n-'1 means
:: MYCIELSK:def 10
ex myc being Function
st it = myc.n & dom myc = NAT & myc.0 = CompleteRelStr 2 &
:: can start with empty RelStr, numbers will change
:: and the M_2 ... will not be connected
for k being Nat, R being NatRelStr of 3*2|^k-'1
st R = myc.k holds myc.(k+1) = Mycielskian R;
end;
theorem :: MYCIELSK:49 :: Mycn1:
Mycielskian 0 = CompleteRelStr 2 &
for k being Nat holds Mycielskian (k+1) = Mycielskian Mycielskian k;
registration
let n be Nat;
cluster Mycielskian n -> irreflexive;
end;
registration
let n be Nat;
cluster Mycielskian n -> symmetric;
end;
theorem :: MYCIELSK:50 :: Mycth:
for n being Nat
holds clique# Mycielskian n = 2 & chromatic# Mycielskian n = n+2;
theorem :: MYCIELSK:51
for n being Nat
ex R being finite RelStr st clique# R = 2 & chromatic# R > n;
theorem :: MYCIELSK:52
for n being Nat
ex R being finite RelStr st stability# R = 2 & cliquecover# R > n;