:: Ramsey's Theorem
::  by Marco Riccardi
::
:: Received April 18, 2008
:: Copyright (c) 2008-2021 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, ZFMISC_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_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, FUNCT_3, GROUP_10, NEWTON, NAT_D;
 constructors WELLORD2, GROUP_10, NEWTON, NAT_D, REAL_1, RVSUM_1, CARD_5,
      RELSET_1, NUMBERS, EQREL_1, FUNCT_3;
 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) equals
:: RAMSEY_1:def 2
  (.:f)|the_subsets_of_card(n,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;