:: 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);

end;
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;

ex p being Element of P st the_subsets_of_card (Y,H) c= p;

:: 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 );

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
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 ;

(.: f) | (the_subsets_of_card (n,X)) is Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y))

end;
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));

(.: f) | (the_subsets_of_card (n,X)) is Function of (the_subsets_of_card (n,X)),(the_subsets_of_card (n,Y))

proof 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));

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))

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;

registration
end;

registration
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: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;

the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) by Lm1;

theorem :: RAMSEY_1:8

theorem :: RAMSEY_1:9

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

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 )

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 :: 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 )

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;

:: 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} ) ) ) )

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;

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 )

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;

:: Ramsey's Theorem