:: Ramsey's Theorem
:: by Marco Riccardi
::
:: Copyright (c) 2008-2021 Association of Mizar Users

definition
let X, Y be set ;
let H be Subset of X;
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;

:: deftheorem defines is_homogeneous_for RAMSEY_1:def 1 :
for X, Y being set
for H being Subset of X
for P being a_partition of the_subsets_of_card (Y,X) holds
( H is_homogeneous_for P iff ex p being Element of P st the_subsets_of_card (Y,H) c= p );

registration
let n be Nat;
let X be infinite set ;
cluster the_subsets_of_card (n,X) -> non empty ;
coherence
not the_subsets_of_card (n,X) is empty
proof end;
end;

definition
let n be Nat;
let X, Y be set ;
let f be Function of X,Y;
assume that
A1: f is one-to-one and
A2: ( card n c= card X & not X is empty ) and
A3: not Y is empty ;
func f ||^ n -> Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y)) equals :Def2: :: RAMSEY_1:def 2
(.: f) | (the_subsets_of_card (n,X));
coherence
(.: f) | (the_subsets_of_card (n,X)) is Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y))
proof end;
end;

:: deftheorem Def2 defines ||^ RAMSEY_1:def 2 :
for n being Nat
for X, Y being set
for f being Function of X,Y st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
f ||^ n = (.: f) | (the_subsets_of_card (n,X));

Def2A: for n being Nat
for X, Y being set
for f being Function of X,Y st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
for x being Element of the_subsets_of_card (n,X) holds (f ||^ n) . x = f .: x

proof end;

Lm1: for X, Y, Z being set st X c= Y holds
the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y)

proof end;

theorem Th1: :: RAMSEY_1:1
for n being Nat
for X, Y being set
for f being Function of X,Y
for H being Subset of X st f is one-to-one & card n c= card X & not X is empty & not Y is empty holds
the_subsets_of_card (n,(f .: H)) = (f ||^ n) .: (the_subsets_of_card (n,H))
proof end;

Lm2: for X being set holds the_subsets_of_card (0,X) =
proof end;

Lm3: for X, Y being finite set st card Y = X holds
the_subsets_of_card (X,Y) = {Y}

proof end;

theorem Th2: :: RAMSEY_1:2
for X being set st X is infinite & X c= omega holds
card X = omega by ;

theorem Th3: :: RAMSEY_1:3
for X, Y being set st X is infinite holds
X \/ Y is infinite
proof end;

theorem Th4: :: RAMSEY_1:4
for X, Y being set st X is infinite & Y is finite holds
X \ Y is infinite
proof end;

registration
let X be infinite set ;
let Y be set ;
cluster X \/ Y -> infinite ;
correctness
coherence
not X \/ Y is finite
;
by Th3;
end;

registration
let X be infinite set ;
let Y be finite set ;
cluster X \ Y -> infinite ;
correctness
coherence
not X \ Y is finite
;
by Th4;
end;

Lm4: for n, k being Nat
for X being set
for F being Function of (the_subsets_of_card (n,X)),k st card X = omega & X c= omega & k <> 0 holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (n,H)) is constant )

proof end;

theorem :: RAMSEY_1:5
for X being set holds the_subsets_of_card (0,X) = by Lm2;

theorem Th6: :: RAMSEY_1:6
for n being Nat
for X being finite set st card X < n holds
the_subsets_of_card (n,X) is empty
proof end;

theorem :: RAMSEY_1:7
for X, Y, Z being set st X c= Y holds
the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) by Lm1;

theorem :: RAMSEY_1:8
for X, Y being set st X is finite & Y is finite & card Y = X holds
the_subsets_of_card (X,Y) = {Y} by Lm3;

theorem :: RAMSEY_1:9
for X, Y being set
for f being Function of X,Y st not X is empty & not Y is empty holds
( f is constant iff ex y being Element of Y st rng f = {y} ) by FUNCT_2:111;

theorem Th10: :: RAMSEY_1:10
for k being Nat
for X being finite set st k <= card X holds
ex Y being Subset of X st card Y = k
proof end;

theorem Th11: :: RAMSEY_1:11
for n, m being Nat st m >= 1 holds
n + 1 <= (n + m) choose m
proof end;

theorem Th12: :: RAMSEY_1:12
for n, m being Nat st m >= 1 & n >= 1 holds
m + 1 <= (n + m) choose m
proof end;

theorem Th13: :: RAMSEY_1:13
for X being non empty set
for p1, p2 being Element of X
for P being a_partition of X
for A being Element of P st p1 in A & (proj P) . p1 = (proj P) . p2 holds
p2 in A
proof end;

theorem Th14: :: RAMSEY_1:14
for n, k being Nat
for X being set
for F being Function of (the_subsets_of_card (n,X)),k st k <> 0 & X is infinite holds
ex H being Subset of X st
( H is infinite & F | (the_subsets_of_card (n,H)) is constant )
proof end;

:: theorem 9.1 Set Theory T.Jech
:: Ramsey's Theorem
theorem :: RAMSEY_1:15
for n, k being Nat
for X being infinite set
for 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 )
proof end;

scheme :: RAMSEY_1:sch 1
BinInd2{ P1[ Nat, Nat] } :
for n, m being Nat holds P1[m,n]
provided
A1: for n being Nat holds
( P1[ 0 ,n] & P1[n, 0 ] ) and
A2: for n, m being Nat st P1[m + 1,n] & P1[m,n + 1] holds
P1[m + 1,n + 1]
proof end;

:: Chapter 35 proof from THE BOOK Aigner-Ziegler
theorem Th16: :: RAMSEY_1:16
for n, m being Nat st m >= 2 & n >= 2 holds
ex r being Nat st
( r <= ((m + n) -' 2) choose (m -' 1) & r >= 2 & ( for X being finite set
for 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} ) ) ) )
proof end;

:: Ramsey's Theorem (finite case)
theorem :: RAMSEY_1:17
for m being Nat ex r being Nat st
for X being finite set
for 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 )
proof end;