:: Ramsey's Theorem
:: by Marco Riccardi
::
:: Received April 18, 2008
:: 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) = {0}

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 WAYBEL12:2, CARD_1:5, CARD_1:47;

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) = {0} 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{ P₁[ Nat, Nat] } :

for n, m being Nat holds P₁[m,n]

provided

A1: for n being Nat holds
( P₁[ 0 ,n] & P₁[n, 0 ] ) and
A2: for n, m being Nat st P₁[m + 1,n] & P₁[m,n + 1] holds
P₁[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;