:: Ramsey's Theorem :: by Marco Riccardi :: :: Received April 18, 2008 :: Copyright (c) 2008-2018 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;