:: Ramsey's Theorem
:: by Marco Riccardi
::
:: Received April 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
:: deftheorem Def1 defines is_homogeneous_for RAMSEY_1:def 1 :
definition
let n be
natural number ;
let X,
Y be
set ;
let f be
Function of
X,
Y;
assume A1:
(
f is
one-to-one &
card n c= card X & not
X is
empty & not
Y is
empty )
;
func f ||^ n -> Function of
the_subsets_of_card n,
X,
the_subsets_of_card n,
Y means :
Def2:
:: RAMSEY_1:def 2
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 :
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: :: RAMSEY_1:1
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: :: RAMSEY_1:2
theorem Th3: :: RAMSEY_1:3
theorem Th4: :: RAMSEY_1:4
Lm5:
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 :: RAMSEY_1:5
theorem Th6: :: RAMSEY_1:6
theorem :: RAMSEY_1:7
theorem :: RAMSEY_1:8
theorem :: RAMSEY_1:9
theorem Th10: :: RAMSEY_1:10
theorem Th11: :: RAMSEY_1:11
theorem Th12: :: RAMSEY_1:12
theorem Th13: :: RAMSEY_1:13
theorem Th14: :: RAMSEY_1:14
theorem :: RAMSEY_1:15
theorem Th16: :: RAMSEY_1:16
theorem :: RAMSEY_1:17