:: Ramsey's Theorem
:: by Marco Riccardi
::
:: Received April 18, 2008
:: Copyright (c) 2008-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 NUMBERS, ORDINAL1, FUNCT_1, SUBSET_1, EQREL_1, GROUP_10, TARSKI,
FINSET_1, XBOOLE_0, CARD_1, RELAT_1, FUNCT_2, ARYTM_1, ARYTM_3, XXREAL_0,
NAT_1, FINSEQ_1, CARD_3, RAMSEY_1;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, RELAT_1, RELSET_1,
FUNCT_1, FINSEQ_1, CARD_1, ORDINAL1, NAT_1, NUMBERS, PARTFUN1, EQREL_1,
FINSET_1, FUNCT_2, GROUP_10, NEWTON, NAT_D;
constructors WELLORD2, GROUP_10, NEWTON, NAT_D, REAL_1, RVSUM_1, CARD_5,
RELSET_1, NUMBERS, EQREL_1;
registrations XBOOLE_0, SUBSET_1, XXREAL_0, XREAL_0, FINSEQ_1, RELAT_1,
ORDINAL1, EQREL_1, CARD_3, NAT_1, CARD_1, MEMBERED, FINSET_1, FUNCT_1,
FUNCT_2, RELSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve n,m,k for Nat,
X,Y,Z for set,
f for Function of X,Y,
H for Subset of X;
definition
let X,Y,H;
let P be a_partition of the_subsets_of_card(Y,X);
pred H is_homogeneous_for P means
:: RAMSEY_1:def 1
ex p being Element of P st the_subsets_of_card(Y,H) c= p;
end;
registration
let n;
let X be infinite set;
cluster the_subsets_of_card(n,X) -> non empty;
end;
definition
let n,X,Y,f;
assume that
f is one-to-one and
card n c= card X & X is non empty and
Y is non empty;
func f ||^ n -> Function of the_subsets_of_card(n,X), the_subsets_of_card(n,
Y) means
:: RAMSEY_1:def 2
for x being Element of the_subsets_of_card(n,X) holds it.x = f .: x;
end;
theorem :: RAMSEY_1:1
f is one-to-one & card n c= card X & X is non empty & Y is non
empty implies the_subsets_of_card(n,f .: H) = (f||^n) .: the_subsets_of_card(n,
H);
theorem :: RAMSEY_1:2
X is infinite & X c= omega implies card X = omega;
theorem :: RAMSEY_1:3
X is infinite implies X \/ Y is infinite;
theorem :: RAMSEY_1:4
X is infinite & Y is finite implies X \ Y is infinite;
registration
let X be infinite set;
let Y be set;
cluster X \/ Y -> infinite;
end;
registration
let X be infinite set;
let Y be finite set;
cluster X \ Y -> infinite;
end;
theorem :: RAMSEY_1:5
the_subsets_of_card(0,X) = {0};
theorem :: RAMSEY_1:6
for X being finite set st card X < n holds the_subsets_of_card(n, X) is empty
;
theorem :: RAMSEY_1:7
X c= Y implies the_subsets_of_card(Z,X) c= the_subsets_of_card(Z,Y);
theorem :: RAMSEY_1:8
X is finite & Y is finite & card Y = X implies the_subsets_of_card(X,Y
) = {Y};
theorem :: RAMSEY_1:9
X is non empty & Y is non empty implies (f is constant iff ex y being
Element of Y st rng f = {y});
theorem :: RAMSEY_1:10
for X being finite set st k <= card X holds ex Y being Subset of
X st card Y = k;
theorem :: RAMSEY_1:11
m>=1 implies n+1 <= (n+m) choose m;
theorem :: RAMSEY_1:12
m>=1 & n>=1 implies m+1 <= (n+m) choose m;
theorem :: RAMSEY_1:13
for X being non empty set, p1,p2 being Element of X, P being
a_partition of X, A being Element of P st p1 in A & (proj P).p1=(proj P).p2
holds p2 in A;
begin :: Infinite Ramsey Theorem
theorem :: RAMSEY_1:14
for F being Function of the_subsets_of_card(n,X),k st k<>0 & X
is infinite holds ex H st H is infinite & F|the_subsets_of_card(n,H) is
constant;
:: theorem 9.1 Set Theory T.Jech
::$N Ramsey's Theorem
theorem :: RAMSEY_1:15
for X being infinite set, P being a_partition of the_subsets_of_card(n
,X) st card P = k holds ex H being Subset of X st H is infinite & H
is_homogeneous_for P;
begin :: Ramsey's Theorem
scheme :: RAMSEY_1:sch 1
BinInd2 { P[Nat,Nat] } : P[m,n]
provided
P[0,n] & P[n,0] and
P[m+1,n] & P[m,n+1] implies P[m+1,n+1];
:: Chapter 35 proof from THE BOOK Aigner-Ziegler
theorem :: RAMSEY_1:16
m >= 2 & n >= 2 implies ex r being Nat st r <= (m + n
-' 2) choose (m -' 1) & r >= 2 & for X being finite set, F being Function of
the_subsets_of_card(2,X), Seg 2 st card X >= r holds ex S being Subset of X st
card S >= m & rng(F|the_subsets_of_card(2,S)) = {1} or card S >= n & rng(F|
the_subsets_of_card(2,S)) = {2};
::$N Ramsey's Theorem (finite case)
theorem :: RAMSEY_1:17
for m being Nat holds ex r being Nat st for X
being finite set, P being a_partition of the_subsets_of_card(2,X) st card X >=
r & card P = 2 holds ex S being Subset of X st card S >= m & S
is_homogeneous_for P;