begin
:: deftheorem Def1 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 );
definition
let n be
natural number ;
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) means :
Def2:
for
x being
Element of
the_subsets_of_card n,
X holds
it . x = f .: x;
existence
ex b1 being Function of (the_subsets_of_card n,X),(the_subsets_of_card n,Y) st
for x being Element of the_subsets_of_card n,X holds b1 . x = f .: x
uniqueness
for b1, b2 being Function of (the_subsets_of_card n,X),(the_subsets_of_card n,Y) st ( for x being Element of the_subsets_of_card n,X holds b1 . x = f .: x ) & ( for x being Element of the_subsets_of_card n,X holds b2 . x = f .: x ) holds
b1 = b2
end;
:: deftheorem Def2 defines ||^ RAMSEY_1:def 2 :
for n being natural number
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 b5 being Function of (the_subsets_of_card n,X),(the_subsets_of_card n,Y) holds
( b5 = f ||^ n iff for x being Element of the_subsets_of_card n,X holds b5 . x = f .: x );
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
theorem Th1:
Lm2:
for X being set holds the_subsets_of_card 0 ,X = {0 }
Lm3:
for X, Y being finite set st card Y = X holds
the_subsets_of_card X,Y = {Y}
theorem Th2:
theorem Th3:
theorem Th4:
Lm4:
for n, k being natural number
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
( not H is finite & F | (the_subsets_of_card n,H) is constant )
theorem
theorem Th6:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
begin
theorem Th14:
theorem
begin
theorem Th16:
theorem