:: Ramsey's Theorem
:: by Marco Riccardi
::
:: Received April 18, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ORDINAL1, FUNCT_1, SUBSET_1, EQREL_1, GROUP_10, TARSKI,
FINSET_1, XBOOLE_0, CARD_1, RELAT_1, FUNCT_2, ARYTM_1, ARYTM_3, XXREAL_0,
NAT_1, FINSEQ_1, CARD_3, RAMSEY_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, XCMPLX_0, XXREAL_0, RELAT_1,
RELSET_1, FUNCT_1, FINSEQ_1, CARD_1, ORDINAL1, NAT_1, NUMBERS, PARTFUN1,
EQREL_1, FINSET_1, FUNCT_2, FUNCT_3, GROUP_10, NEWTON, NAT_D;
constructors WELLORD2, GROUP_10, NEWTON, NAT_D, REAL_1, RVSUM_1, CARD_5,
RELSET_1, NUMBERS, EQREL_1, FUNCT_3;
registrations XBOOLE_0, SUBSET_1, XXREAL_0, XREAL_0, FINSEQ_1, RELAT_1,
ORDINAL1, EQREL_1, CARD_3, NAT_1, CARD_1, MEMBERED, FINSET_1, FUNCT_1,
FUNCT_2, RELSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities GROUP_10, ORDINAL1;
expansions TARSKI;
theorems TARSKI, XBOOLE_0, XBOOLE_1, EQREL_1, CARD_1, WELLORD2, FUNCT_1,
FUNCT_2, RELAT_1, GROUP_10, ZFMISC_1, CARD_2, NAT_1, XREAL_1, ORDINAL1,
XXREAL_0, STIRL2_1, WAYBEL12, CARD_FIL, FINSEQ_1, NEWTON, ENUMSET1,
NAT_D, XREAL_0, CARD_3, FUNCT_3;
schemes NAT_1, FUNCT_2, RECDEF_2;
begin :: Preliminaries
reserve n,m,k for Nat,
X,Y,Z for set,
f for Function of X,Y,
H for Subset of X;
definition
let X,Y,H;
let P be a_partition of the_subsets_of_card(Y,X);
pred H is_homogeneous_for P means
ex p being Element of P st the_subsets_of_card(Y,H) c= p;
end;
registration
let n;
let X be infinite set;
cluster the_subsets_of_card(n,X) -> non empty;
coherence
proof
not card X c= card n;
hence thesis by GROUP_10:1;
end;
end;
definition
let n,X,Y,f;
assume that
A1: f is one-to-one and
A2: card n c= card X & X is non empty and
A3: Y is non empty;
func f ||^ n -> Function of the_subsets_of_card(n,X),
the_subsets_of_card(n,Y) equals :Def2:
(.:f)|the_subsets_of_card(n,X);
::: for x being Element of the_subsets_of_card(n,X) holds it.x = f .: x;
coherence
proof
set IT = (.:f)|the_subsets_of_card(n,X);
set D = the_subsets_of_card(n,X);
reconsider D as non empty set by A2,GROUP_10:1;
a1: dom (.:f) = bool dom f by FUNCT_3:def 1;
a2: dom IT = dom (.:f) /\ the_subsets_of_card(n,X) by RELAT_1:61;
B1: dom f = X by A3,FUNCT_2:def 1; then
A4: dom IT = D by a1,a2,XBOOLE_1:28;
for y being object st y in rng IT holds y in the_subsets_of_card(n,Y)
proof
let y be object;
assume y in rng IT;
then consider x be object such that
A5: x in dom IT and
A6: y = IT.x by FUNCT_1:def 3;
A7: ex x9 be Subset of X st x=x9 & card x9 = n by A4,A5;
reconsider x as Element of D by B1,a1,a2,XBOOLE_1:28,A5;
Aa: x in the_subsets_of_card(n,X);
y = (.:f).x by A6,A4,FUNCT_1:47; then
A8: y = f .: x by Aa,B1,FUNCT_3:def 1;
f in Funcs(X, Y) by A3,FUNCT_2:8; then
A9: ex f9 be Function st f=f9 & dom f9=X & rng f9 c= Y by FUNCT_2:def 2;
f .: x c= rng f by RELAT_1:111;
then reconsider y9=y as Subset of Y by A8,A9,XBOOLE_1:1;
card y9 = n by A7,A8,CARD_1:5,A1,A9,CARD_1:33;
hence thesis;
end;
then rng IT c= the_subsets_of_card(n,Y);
hence thesis by A4,FUNCT_2:2;
end;
end;
Def2A:
f is one-to-one & card n c= card X & X is non empty &
Y is non empty implies
for x being Element of the_subsets_of_card(n,X) holds
(f ||^ n).x = f .: x
proof
assume
A1: f is one-to-one & card n c= card X & X is non empty &
Y is non empty;
let x be Element of the_subsets_of_card(n,X);
A0: dom f = X by FUNCT_2:def 1,A1;
A3: the_subsets_of_card(n,X) <> {} by A1,GROUP_10:1; then
A2: x in the_subsets_of_card(n,X);
(f ||^ n).x = ((.:f)|the_subsets_of_card(n,X)).x by A1,Def2
.= (.:f).x by A3,FUNCT_1:49
.= f .: x by A2,A0,FUNCT_3:def 1;
hence thesis;
end;
Lm1: X c= Y implies the_subsets_of_card(Z,X) c= the_subsets_of_card(Z,Y)
proof
assume
A1: X c= Y;
let x be object;
assume x in the_subsets_of_card(Z,X);
then consider x9 be Subset of X such that
A2: x9=x and
A3: card x9 = Z;
reconsider x99=x9 as Subset of Y by A1,XBOOLE_1:1;
x99=x by A2;
hence thesis by A3;
end;
theorem Th1:
f is one-to-one & card n c= card X & X is non empty & Y is non empty
implies
the_subsets_of_card(n,f .: H) = (f||^n) .: the_subsets_of_card(n,H)
proof
assume that
A1: f is one-to-one and
A2: card n c= card X and
A3: X is non empty and
A4: Y is non empty;
consider f1 be Function such that
A5: n c= f1 .: X by A2,CARD_1:66;
f in Funcs(X, Y) by A4,FUNCT_2:8;
then
A6: ex f9 be Function st f=f9 & dom f9=X & rng f9 c= Y by FUNCT_2:def 2;
then card X c= card Y by A1,CARD_1:10;
then consider f2 be Function such that
A7: X c= f2 .: Y by CARD_1:66;
f1 .: X c= f1 .:(f2 .: Y) by A7,RELAT_1:123;
then n c= f1 .:(f2 .: Y) by A5;
then n c= (f1*f2) .: Y by RELAT_1:126;
then card n c= card Y by CARD_1:66;
then the_subsets_of_card(n,Y) is non empty by A4,GROUP_10:1;
then f||^n in Funcs(the_subsets_of_card(n,X), the_subsets_of_card(n,Y)) by
FUNCT_2:8;
then
A8: ex fn be Function st f||^n=fn & dom fn= the_subsets_of_card(n,X) & rng
fn c= the_subsets_of_card(n,Y) by FUNCT_2:def 2;
for y being object holds y in the_subsets_of_card(n,f.:H) iff y in (f||^n)
.:the_subsets_of_card(n,H)
proof
let y be object;
hereby
A9: f.:H c= rng f by RELAT_1:111;
assume
A10: y in the_subsets_of_card(n,f.:H);
then
A11: ex X9 be Subset of f.:H st y=X9 & card X9 = n;
ex x being set st x in dom(f||^n) & x in the_subsets_of_card(n,H) &
y = (f||^n).x
proof
reconsider yy=y as set by TARSKI:1;
set x = f"yy;
take x;
A12: x c= dom f by RELAT_1:132;
A13: f.:x = y by A10,A9,FUNCT_1:77,XBOOLE_1:1;
then reconsider x9=x as Subset of H by A1,A10,A12,FUNCT_1:87;
A14: card x9 = n by A11,A13,CARD_1:5,A1,A12,CARD_1:33;
then
A15: x in the_subsets_of_card(n,H);
A16: the_subsets_of_card(n,H) c= the_subsets_of_card(n,X) by Lm1;
hence x in dom(f||^n) by A8,A15;
thus x in the_subsets_of_card(n,H) by A14;
thus y = f.:x by A10,A9,FUNCT_1:77,XBOOLE_1:1
.= (f||^n).x by A1,A2,A3,A4,A15,A16,Def2A;
end;
hence y in (f||^n).:the_subsets_of_card(n,H) by FUNCT_1:def 6;
end;
assume y in (f||^n).:the_subsets_of_card(n,H);
then consider x be object such that
A17: x in dom(f||^n) and
A18: x in the_subsets_of_card(n,H) and
A19: y = (f||^n).x by FUNCT_1:def 6;
reconsider x as Element of the_subsets_of_card(n,X) by A17;
A20: y = f .: x by A1,A2,A3,A4,A19,Def2A;
then reconsider X9=y as Subset of f.:H by A18,RELAT_1:123;
(ex x9 be Subset of H st x9=x & card x9 = n )& x, f.: x
are_equipotent by A1,A6,A18,CARD_1:33,XBOOLE_1:1;
then card X9 = n by A20,CARD_1:5;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
Lm2: the_subsets_of_card(0,X) = {0}
proof
for x being object holds x in the_subsets_of_card(0,X) iff x=0
proof
let x be object;
hereby
assume x in the_subsets_of_card(0,X);
then ex x9 be Subset of X st x9=x & card x9 = 0;
hence x=0;
end;
assume
A1: x=0;
then reconsider x9=x as Subset of X by XBOOLE_1:2;
card x9 = 0 by A1;
hence thesis;
end;
hence thesis by TARSKI:def 1;
end;
Lm3:
for X,Y being finite set st card Y = X holds the_subsets_of_card(X,Y) = {Y}
proof
let X,Y be finite set;
assume
A1: card Y = X;
for x being object holds x in the_subsets_of_card(X,Y) iff x = Y
proof
let x be object;
hereby
assume x in the_subsets_of_card(X,Y);
then consider X9 be Subset of Y such that
A2: X9=x and
A3: card X9 = X;
reconsider X9 as finite Subset of Y;
card(Y \ X9) = card Y - card X9 by CARD_2:44
.= 0 by A1,A3;
then Y \ X9 = {};
then Y c= X9 by XBOOLE_1:37;
hence x = Y by A2,XBOOLE_0:def 10;
end;
reconsider xx = x as set by TARSKI:1;
assume
A4: x = Y;
then xx c= Y;
then reconsider x9=x as Subset of Y;
x9 in the_subsets_of_card(X,Y) by A1,A4;
hence thesis;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th2:
X is infinite & X c= omega implies card X = omega
by WAYBEL12:2,CARD_1:5,CARD_1:47;
theorem Th3:
X is infinite implies X \/ Y is infinite
proof
card X c= card(X \/ Y) by CARD_1:11,XBOOLE_1:7;
hence thesis;
end;
theorem Th4:
X is infinite & Y is finite implies X \ Y is infinite
proof
X \/ Y = (X \ Y) \/ Y by XBOOLE_1:39;
hence thesis by Th3;
end;
registration
let X be infinite set;
let Y be set;
cluster X \/ Y -> infinite;
correctness by Th3;
end;
registration
let X be infinite set;
let Y be finite set;
cluster X \ Y -> infinite;
correctness by Th4;
end;
Lm4: for F being Function of (the_subsets_of_card(n,X)),k st card X = omega &
X c= omega & k<>0 holds ex H st H is infinite & F|the_subsets_of_card(n,H) is
constant
proof
defpred P[Nat] means for k being Nat, X being set, F
being Function of (the_subsets_of_card($1,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($1
,H) is constant;
A1: for n be Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume
A2: P[n];
now
let k be Nat;
let X be set;
let F be Function of (the_subsets_of_card(n+1,X)),k;
assume
A3: card X = omega;
X c= X;
then
A4: X in the_subsets_of_card(omega,X) by A3;
then reconsider A = the_subsets_of_card(omega,X) as non empty set;
reconsider X0=X as Element of A by A4;
defpred P1[set,set,set,set,set] means for x1,x2 being Element of A, y1,
y2 being Element of omega st $2=x1 & $3=y1 & $4=x2 & $5=y2 holds (y1 in x1
implies (ex F1 being Function of the_subsets_of_card(n,x1\{y1}),k, H1 being
Subset of x1\{y1} st H1 is infinite & F1|the_subsets_of_card(n,H1) is constant
& x2=H1 & y2 in H1 & y1 < y2 & (for x19 being Element of the_subsets_of_card(n,
x1\{y1}) holds F1.x19 = F.(x19 \/ {y1})) & for y29 being Element of omega st
y29>y1 & y29 in H1 holds y2<=y29)) & (not y1 in x1 implies x2=X & y2=0);
set Y0 = min* X;
assume
A5: X c= omega;
assume
A6: k<>0;
A7: for Y being set,a being Element of Y st card Y = omega & Y c= X ex
Fa being Function of the_subsets_of_card(n,Y\{a}),k, Ha being Subset of Y\{a}
st Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant & for Y9 being
Element of the_subsets_of_card(n,Y\{a}) holds Fa.Y9 = F.(Y9 \/ {a})
proof
let Y be set;
let a be Element of Y;
set Y1 = the_subsets_of_card(n,Y\{a});
assume
A8: card Y = omega;
then
A9: Y is infinite;
then reconsider Y1 as non empty set;
deffunc F1(Element of Y1)=F.($1 \/ {a});
assume
A10: Y c= X;
Y is non empty by A8; then
A11: {a} c= Y by ZFMISC_1:31;
A12: for x being Element of Y1 holds F1(x) in k
proof
let x be Element of Y1;
x in Y1;
then consider x9 be Subset of Y\{a} such that
A13: x=x9 and
A14: card x9=n;
x \/ {a} c= (Y\{a}) \/ {a} by A13,XBOOLE_1:9;
then x \/ {a} c= Y \/ {a} by XBOOLE_1:39;
then reconsider y=x \/ {a} as Subset of Y by A11,XBOOLE_1:12;
reconsider x99=x9 as finite set by A14;
not a in x99
proof
assume a in x99;
then not a in {a} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
then card y = n+1 by A13,A14,CARD_2:41;
then
A15: x \/ {a} in the_subsets_of_card(n+1,Y);
the_subsets_of_card(n+1,Y) c= the_subsets_of_card(n+1,X) by A10,Lm1;
hence thesis by A6,A15,FUNCT_2:5;
end;
consider Fa be Function of Y1,k such that
A16: for x being Element of Y1 holds Fa.x = F1(x) from FUNCT_2:sch
8(A12);
reconsider Fa as Function of the_subsets_of_card(n,Y\{a}),k;
A17: Y c= omega by A5,A10;
then card(Y\{a}) = omega by A9,Th2,XBOOLE_1:1;
then consider Ha be Subset of Y\{a} such that
A18: Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant by A2,A6,A17,
XBOOLE_1:1;
take Fa,Ha;
thus Ha is infinite & Fa|the_subsets_of_card(n,Ha) is constant by A18;
let Y9 be Element of the_subsets_of_card(n,Y\{a});
thus thesis by A16;
end;
A19: for a being Nat, x99 being Element of A, y99 being
Element of omega ex x199 being Element of A, y199 being Element of omega st P1[
a,x99,y99,x199,y199]
proof
let a be Nat;
let x99 be Element of A;
let y99 be Element of omega;
per cases;
suppose
A20: y99 in x99;
then reconsider a9=y99 as Element of x99;
A21: x99 in A;
then ex x999 be Subset of X st x999=x99 & card x999 = omega;
then consider
Fa be Function of the_subsets_of_card(n,x99\{a9}),k, Ha be
Subset of x99\{a9} such that
A22: Ha is infinite and
A23: Fa|the_subsets_of_card(n,Ha) is constant and
A24: for Y9 being Element of the_subsets_of_card(n,x99\{a9})
holds Fa.Y9 = F.(Y9 \/ {a9}) by A7;
Ha c= x99 by XBOOLE_1:1;
then
A25: Ha c= X by A21,XBOOLE_1:1;
then card Ha = omega by A5,A22,Th2,XBOOLE_1:1;
then Ha in A by A25;
then reconsider x199=Ha as Element of A;
set y199=min* {y29 where y29 is Element of omega: y29>y99 & y29 in
Ha};
take x199, y199;
A26: Ha c= omega by A5,A25;
now
let x1,x2 be Element of A;
let y1,y2 be Element of omega;
assume that
A27: x99=x1 and
A28: y99=y1;
assume that
A29: x199=x2 and
A30: y199=y2;
thus y1 in x1 implies ex F1 being Function of the_subsets_of_card(
n,x1\{y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|
the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x19
being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x19 = F.(x19 \/ {y1}))
& for y29 being Element of omega st y29>y1 & y29 in H1 holds y2<=y29
proof
reconsider H1=Ha as Subset of x1\{y1} by A27,A28;
set A9= {y29 where y29 is Element of omega: y29>y99 & y29 in Ha};
reconsider F1=Fa as Function of the_subsets_of_card(n,x1\{y1}),k
by A27,A28;
assume y1 in x1;
take F1, H1;
for x being object st x in A9 holds x in NAT
proof
let x be object;
assume x in A9;
then ex x9 be Element of omega st x9=x & x9>y99 & x9 in Ha;
hence thesis;
end;
then reconsider A9 as Subset of NAT by TARSKI:def 3;
thus H1 is infinite by A22;
thus F1|the_subsets_of_card(n,H1) is constant by A23;
thus x2=H1 by A29;
A9 <> {}
proof
set A99 = {y2999 where y2999 is Element of omega: y2999<=y99 &
y2999 in Ha};
A31: now
let x be object;
assume
A32: x in A9 \/ A99;
per cases by A32,XBOOLE_0:def 3;
suppose
x in A9;
then ex x9 be Element of omega st x=x9 & x9>y99 & x9 in Ha;
hence x in Ha;
end;
suppose
x in A99;
then
ex x9 be Element of omega st x=x9 & x9<=y99 & x9 in Ha;
hence x in Ha;
end;
end;
now
let x be object;
assume x in A99;
then consider x9 be Element of omega such that
A33: x=x9 and
A34: x9<=y99 and
x9 in Ha;
x9 < y99+1 by A34,NAT_1:13;
hence x in Segm(y99+1) by A33,NAT_1:44;
end;
then
A35: A99 c= Segm(y99+1);
A36: now
let x be object;
assume
A37: x in Ha;
then reconsider x9=x as Element of omega by A26;
per cases;
suppose
x9<=y99;
then x in A99 by A37;
hence x in A9 \/ A99 by XBOOLE_0:def 3;
end;
suppose
x9>y99;
then x in A9 by A37;
hence x in A9 \/ A99 by XBOOLE_0:def 3;
end;
end;
assume A9 = {};
hence contradiction by A22,A35,A31,A36,TARSKI:2;
end;
then y199 in A9 by NAT_1:def 1;
then
A38: ex y299 be Element of omega st y199=y299 & y299>y99 & y299 in Ha;
hence y2 in H1 by A30;
thus y1 < y2 by A28,A30,A38;
thus for x19 being Element of the_subsets_of_card(n,x1\{y1})
holds F1.x19 = F.(x19 \/ {y1}) by A24,A27,A28;
let y29 be Element of omega;
assume
A39: y29>y1;
assume y29 in H1;
then y29 in A9 by A28,A39;
hence thesis by A30,NAT_1:def 1;
end;
assume not y1 in x1;
hence thesis by A20,A27,A28;
end;
hence thesis;
end;
suppose
A40: not y99 in x99;
reconsider y199=0 as Element of omega;
reconsider x199=X as Element of A by A4;
take x199, y199;
thus thesis by A40;
end;
end;
consider S be sequence of A, a be sequence of omega such that
A41: S.0 = X0 & a.0 = Y0 & for i being Nat holds P1[i,S.i
,a.i,S.(i+1),a.(i+1)] from RECDEF_2:sch 3(A19);
defpred P2[Nat] means a.$1 in Segm(a.($1+1)) & S.($1+1) c= S.$1 & a
.$1 in S.$1 & a.($1+1) in S.($1+1) & not a.$1 in S.($1+1);
A42: P2[0]
proof
set i=0;
reconsider i as Element of NAT;
reconsider x1=S.i as Element of A;
reconsider x2=S.(i+1) as Element of A;
reconsider y1=a.i as Element of omega;
reconsider y2=a.(i+1) as Element of omega;
A43: y1 in x1 implies ex F1 being Function of the_subsets_of_card(n,x1
\{ y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|
the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x19
being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x19 = F.(x19 \/ {y1}))
& for y29 being Element of omega st y29>y1 & y29 in H1 holds y2<=y29 by A41;
hence a.0 in Segm(a.(0+1)) by A3,A5,A41,CARD_1:27,NAT_1:44,def 1;
thus S.(0+1) c= S.0 by A3,A5,A41,A43,CARD_1:27,NAT_1:def 1,XBOOLE_1:1;
thus a.0 in S.0 by A3,A5,A41,CARD_1:27,NAT_1:def 1;
thus a.(0+1) in S.(0+1) by A3,A5,A41,A43,CARD_1:27,NAT_1:def 1;
not y1 in x2
proof
assume y1 in x2;
then not y1 in {y1} by A3,A5,A41,A43,CARD_1:27,NAT_1:def 1
,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
hence thesis;
end;
defpred P4[object,object] means
for Y being set, i being Element of NAT, Fi
being Function of the_subsets_of_card(n,S.i\{a.i}),k st i=$1 & Y = {x where x
is Element of omega: ex j being Element of NAT st a.j=x & j>i} & (for Y9 being
Element of the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y9 = F.(Y9 \/ {a.i}))
holds ex l being Nat st l=$2 & l in k & rng(Fi|the_subsets_of_card(n
,Y)) = {l};
defpred P3[Nat] means for i,j being Nat st i>=j &
i=$1+j holds S.i c= S.j & (for ai,aj being Nat st i<>j & ai=a.i & aj
=a.j holds ai > aj);
A44: for i being Nat st P2[i] holds P2[i + 1]
proof
let i be Nat;
reconsider i9=i+1 as Element of NAT;
reconsider x1=S.i9 as Element of A;
reconsider x2=S.(i9+1) as Element of A;
reconsider y1=a.i9 as Element of omega;
reconsider y2=a.(i9+1) as Element of omega;
assume
A45: P2[i];
then
A46: ex F1 be Function of the_subsets_of_card(n,x1\{y1}),k, H1 be
Subset of x1\{y1} st H1 is infinite & F1|the_subsets_of_card(n,H1) is constant
& x2=H1 & y2 in H1 & y1 < y2 &( for x19 being Element of the_subsets_of_card(n,
x1\{y1}) holds F1. x19 = F.(x19 \/ {y1}))& for y29 being Element of omega st
y29>y1 & y29 in H1 holds y2<=y29 by A41;
not y1 in x2
proof
assume y1 in x2;
then not y1 in {y1} by A46,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
hence P2[i + 1] by A45,A46,NAT_1:44,XBOOLE_1:1;
end;
A47: for i being Nat holds P2[i] from NAT_1:sch 2(A42,A44);
A48: for l being Nat st P3[l] holds P3[l+1]
proof
let l be Nat;
assume
A49: P3[l];
thus P3[l+1]
proof
let i,j be Nat;
assume
A50: i>=j;
set j9=j+1;
assume
A51: i=l+1+j;
then
A52: i=l+j9;
A53: S.(j+1) c= S.j by A47;
i<>j
proof
assume i=j;
then 0=l+1 by A51;
hence contradiction;
end;
then i>j by A50,XXREAL_0:1;
then
A54: i>=j9 by NAT_1:13;
then S.i c= S.(j+1) by A49,A52;
hence S.i c= S.j by A53;
A55: for ai,aj9 being Nat st i<>j9 & ai=a.i & aj9=a.j9
holds ai > aj9 by A49,A54,A52;
thus for ai,aj being Nat st i<>j & ai=a.i & aj=a.j holds
ai > aj
proof
let ai,aj be Nat;
assume i<>j;
assume that
A56: ai=a.i and
A57: aj=a.j;
reconsider aj9=a.j9 as Nat;
aj in Segm aj9 by A47,A57;
then aj9 > aj by NAT_1:44;
hence thesis by A55,A56,XXREAL_0:2;
end;
end;
end;
A58: P3[0];
A59: for l being Nat holds P3[l] from NAT_1:sch 2(A58,A48);
A60: for i,j being Nat st i>=j holds S.i c= S.j & for ai,aj
being Nat st i<>j & ai=a.i & aj=a.j holds ai > aj
proof
let i,j be Nat;
assume
A61: i>=j;
then
A62: ex l be Nat st i = j + l by NAT_1:10;
hence S.i c= S.j by A59,A61;
thus thesis by A59,A61,A62;
end;
A63: for i being Element of NAT, Y being set, Fi being Function of
the_subsets_of_card(n,S.i\{a.i}),k st Y = {x where x is Element of omega: ex j
being Element of NAT st a.j=x & j>i} & (for Y9 being Element of
the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y9 = F.(Y9 \/ {a.i})) holds Y c= S.(i
+1) & Fi|the_subsets_of_card(n,Y) is constant
proof
let i be Element of NAT;
let Y be set;
let Fi be Function of the_subsets_of_card(n,S.i\{a.i}),k;
assume
A64: Y = {x where x is Element of omega: ex j being Element of
NAT st a.j=x & j>i};
consider x2 be Element of A, y2 be Element of omega such that
A65: S.(i+1)=x2 and
A66: a.(i+1)=y2;
consider x1 be Element of A, y1 be Element of omega such that
A67: S.i=x1 & a.i=y1;
y1 in x1 implies (ex F1 being Function of the_subsets_of_card(n,
x1\{y1}),k, H1 being Subset of x1\{y1} st H1 is infinite & F1|
the_subsets_of_card(n,H1) is constant & x2=H1 & y2 in H1 & y1 < y2 & (for x19
being Element of the_subsets_of_card(n,x1\{y1}) holds F1.x19 = F.(x19 \/ {y1}))
& for y29 being Element of omega st y29>y1 & y29 in H1 holds y2<=y29) & (not y1
in x1 implies x2=X & y2=0) by A41,A67,A65,A66;
then consider
F1 be Function of the_subsets_of_card(n,x1\{y1}),k, H1 be
Subset of x1\{y1} such that
H1 is infinite and
A68: F1|the_subsets_of_card(n,H1) is constant & x2=H1 and
A69: for x19 being Element of the_subsets_of_card(n,x1\{y1})
holds F1. x19 = F.(x19 \/ {y1}) and
for y29 being Element of omega st y29>y1 & y29 in H1 holds y2<=y29
by A47,A67;
reconsider F1 as Function of the_subsets_of_card(n,S.i\{a.i}),k by A67;
assume
A70: for Y9 being Element of the_subsets_of_card(n,S.i\{a.i})
holds Fi.Y9 = F.(Y9 \/ {a.i});
for x19 being Element of the_subsets_of_card(n,S.i\{a.i}) holds
F1.x19 = Fi.x19
proof
let x19 be Element of the_subsets_of_card(n,S.i\{a.i});
thus F1.x19 = F.(x19 \/ {a.i}) by A67,A69
.= Fi.x19 by A70;
end;
then
A71: Fi|the_subsets_of_card(n,S.(i+1)) is constant by A65,A68,FUNCT_2:63;
now
let x be object;
assume x in Y;
then ex x9 be Element of omega st x=x9 & ex j being Element of NAT
st a.j=x9 & j>i by A64;
then consider j be Element of NAT such that
A72: a.j=x and
A73: j>i;
j>=i+1 by A73,NAT_1:13; then
S.j c= S.(i+1) by A60;
hence x in S.(i+1) by A72,A47;
end;
hence Y c= S.(i+1);
then
A75: the_subsets_of_card(n,Y) c= the_subsets_of_card(n,S.(i+1)) by Lm1;
for x,y being object st x in dom(Fi|the_subsets_of_card(n,Y)) & y
in dom(Fi|the_subsets_of_card(n,Y)) holds Fi|the_subsets_of_card(n,Y).x = Fi|
the_subsets_of_card(n,Y).y
proof
let x,y be object;
assume
A76: x in dom(Fi|the_subsets_of_card(n,Y));
then
A77: x in the_subsets_of_card(n,Y);
x in dom Fi by A76,RELAT_1:57;
then
A78: x in dom(Fi|the_subsets_of_card(n,S.(i+1))) by A75,A76,RELAT_1:57;
assume
A79: y in dom(Fi|the_subsets_of_card(n,Y));
then
A80: y in the_subsets_of_card(n,Y);
y in dom Fi by A79,RELAT_1:57;
then
A81: y in dom(Fi|the_subsets_of_card(n,S.(i+1))) by A75,A80,RELAT_1:57;
thus Fi|the_subsets_of_card(n,Y).x = (Fi|the_subsets_of_card(n,S.(i+
1)))|the_subsets_of_card(n,Y).x by A75,FUNCT_1:51
.= Fi|the_subsets_of_card(n,S.(i+1)).x by A77,FUNCT_1:49
.= Fi|the_subsets_of_card(n,S.(i+1)).y by A71,A78,A81,
FUNCT_1:def 10
.= (Fi|the_subsets_of_card(n,S.(i+1)))|the_subsets_of_card(n,Y).
y by A80,FUNCT_1:49
.= Fi|the_subsets_of_card(n,Y).y by A75,FUNCT_1:51;
end;
hence thesis by FUNCT_1:def 10;
end;
for x1,x2 being object st x1 in dom a & x2 in dom a & a.x1 = a.x2
holds x1 = x2
proof
let x1,x2 be object;
assume x1 in dom a;
then reconsider i1=x1 as Element of NAT;
assume x2 in dom a;
then reconsider i2=x2 as Element of NAT;
reconsider ai2=a.i2 as Element of NAT;
reconsider ai1=a.i1 as Element of NAT;
assume
A82: a.x1 = a.x2;
assume
A83: x1 <> x2;
per cases by A83,XXREAL_0:1;
suppose
i1 < i2;
then ai1 < ai2 by A60;
hence contradiction by A82;
end;
suppose
i1 > i2;
then ai1 > ai2 by A60;
hence contradiction by A82;
end;
end;
then
A84: a is one-to-one by FUNCT_1:def 4;
A85: NAT = dom a by FUNCT_2:def 1;
A86: for i being Element of NAT holds card {x9 where x9 is Element of
omega: ex j being Element of NAT st a.j=x9 & j>i} = omega
proof
let i be Element of NAT;
set Z = {x9 where x9 is Element of omega: ex j being Element of NAT st
a.j=x9 & j>i};
now
let z be object;
assume z in Z;
then ex z9 be Element of omega st z=z9 & ex j being Element of NAT
st a.j=z9 & j>i;
hence z in NAT;
end;
then
A87: Z c= NAT;
A88: dom(a|(NAT \ Segm(i+1))) = dom a /\ (NAT \ Segm(i+1)) by RELAT_1:61
.= NAT /\ (NAT \ Segm(i+1)) by FUNCT_2:def 1
.= (NAT /\ NAT) \ Segm(i+1) by XBOOLE_1:49
.= NAT \ Segm(i+1);
for z being object holds z in Z iff z in rng(a|(NAT \ Segm(i+1)))
proof
let z be object;
hereby
assume z in Z;
then ex z9 be Element of omega st z=z9 & ex j being Element of NAT
st a.j=z9 & j>i;
then consider j be Element of NAT such that
A89: a.j=z and
A90: j>i;
j>=i+1 by A90,NAT_1:13;
then not j in Segm(i+1) by NAT_1:44;
then j in (NAT \ Segm(i+1)) by XBOOLE_0:def 5;
hence z in rng(a|(NAT \ Segm(i+1))) by A85,A89,FUNCT_1:50;
end;
assume z in rng(a|(NAT \ Segm(i+1)));
then consider j be object such that
A91: j in dom(a|(NAT \ Segm(i+1))) and
A92: z =(a|(NAT \ Segm(i+1))).j by FUNCT_1:def 3;
j in dom a by A91,RELAT_1:57;
then reconsider j as Element of NAT;
not j in Segm(i+1) by A91,XBOOLE_0:def 5;
then j>=i+1 by NAT_1:44;
then
A93: j>i by NAT_1:13;
a.j=z by A91,A92,FUNCT_1:47;
hence thesis by A93;
end;
then
A94: Z = rng(a|(NAT \ Segm(i+1))) by TARSKI:2;
a|(NAT \ Segm(i+1)) is one-to-one by A84,FUNCT_1:52;
hence thesis by A88,A94,A87,Th2,CARD_1:59;
end;
A95: for x being object st x in NAT
ex y being object st y in k & P4[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i9 = x as Element of NAT;
set Y9 = S.i9;
A96: not a.i9 in S.(i9+1) by A47;
reconsider a9 = a.i9 as Element of Y9 by A47;
set Z = {x9 where x9 is Element of omega: ex j being Element of NAT st
a.j=x9 & j>i9};
A97: S.(i9+1) c= S.i9 by A47;
Y9 in A;
then ex Y99 be Subset of X st Y99=Y9 & card Y99 = omega;
then consider
Fa be Function of the_subsets_of_card(n,Y9\{a9}),k, Ha be
Subset of Y9\{a9} such that
Ha is infinite and
Fa|the_subsets_of_card(n,Ha) is constant and
A98: for Y99 being Element of the_subsets_of_card(n,Y9\{a9})
holds Fa. Y99 = F.(Y99 \/ {a9}) by A7;
A99: Z c= S.(i9+1) by A63,A98;
now
let x be object;
assume x in Z;
then
A100: x in S.(i9+1) by A99;
then not x in {a.i9} by A96,TARSKI:def 1;
hence x in S.i9\{a.i9} by A97,A100,XBOOLE_0:def 5;
end;
then Z c= S.i9\{a.i9};
then the_subsets_of_card(n,Z) c= the_subsets_of_card(n,Y9\{a9}) by Lm1;
then
A101: Fa|the_subsets_of_card(n,Z) is Function of the_subsets_of_card(n
,Z),k by A6,FUNCT_2:32;
A102: not card Z c= card n by A86;
then Z is non empty;
then
A103: the_subsets_of_card(n,Z) is non empty by A102,GROUP_10:1;
Fa|the_subsets_of_card(n,Z) is constant by A63,A98;
then consider y be Element of k such that
A104: rng(Fa|the_subsets_of_card(n,Z)) = {y} by A6,A101,A103,FUNCT_2:111;
reconsider y as set;
take y;
thus y in k by A6;
for Y being set, i being Element of NAT, Fi being Function of
the_subsets_of_card(n,S.i\{a.i}),k st i=x & Y = {x9 where x9 is Element of
omega: ex j being Element of NAT st a.j=x9 & j>i} & (for Y9 being Element of
the_subsets_of_card(n,S.i\{a.i}) holds Fi.Y9 = F.(Y9 \/ {a.i})) holds ex l
being Nat st l=y & l in k & rng(Fi|the_subsets_of_card(n,Y)) = {l}
proof
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
let Y be set;
let i be Element of NAT;
let Fi be Function of the_subsets_of_card(n,S.i\{a.i}),k;
assume
A105: i=x;
k9 is Subset of NAT by STIRL2_1:8;
then reconsider l=y as Nat;
assume
A106: Y = {x9 where x9 is Element of omega: ex j being Element
of NAT st a.j=x9 & j>i};
assume
A107: for Y9 being Element of the_subsets_of_card(n,S.i\{a.i})
holds Fi.Y9 = F.(Y9 \/ {a.i});
take l;
thus l=y;
thus l in k by A6;
for x19 being Element of the_subsets_of_card(n,S.i\{a.i})
holds Fa.x19 = Fi.x19
proof
let x19 be Element of the_subsets_of_card(n,S.i\{a.i});
thus Fa.x19 = F.(x19 \/ {a.i}) by A98,A105
.= Fi.x19 by A107;
end;
hence thesis by A104,A105,A106,FUNCT_2:63;
end;
hence P4[x,y];
end;
consider g be sequence of k such that
A108: for x being object st x in NAT holds P4[x,g.x] from FUNCT_2:sch 1
(A95);
g in Funcs(NAT,k) by A6,FUNCT_2:8;
then ex g9 be Function st g=g9 & dom g9 = NAT & rng g9 c= k by
FUNCT_2:def 2;
then consider k9 be object such that
k9 in rng g and
A109: g"{k9} is infinite by CARD_2:101;
set H = a.:(g"{k9});
g"{k9} c= dom g by RELAT_1:132;
then g"{k9}, H are_equipotent by A84,A85,CARD_1:33,XBOOLE_1:1;
then
A110: card(g"{k9}) = card H by CARD_1:5;
now
let y be object;
assume y in H;
then consider x be object such that
A111: [x,y] in a and
x in g"{k9} by RELAT_1:def 13;
x in dom a by A111,FUNCT_1:1;
then reconsider i=x as Element of NAT;
y = a.x by A111,FUNCT_1:1;
then
A112: y in S.i by A47;
S.i in the_subsets_of_card(omega,X);
hence y in X by A112;
end;
then reconsider H as Subset of X by TARSKI:def 3;
take H;
thus H is infinite by A109,A110;
A113: for y being set st y in dom(F|the_subsets_of_card(n+1,H)) holds F|
the_subsets_of_card(n+1,H).y = k9
proof
let y be set;
assume y in dom(F|the_subsets_of_card(n+1,H));
then
A114: y in the_subsets_of_card(n+1,H) by RELAT_1:57;
then consider Y be Subset of H such that
A115: y=Y and
A116: card Y = n+1;
set y0 = min* Y;
set Y9 = y \ {y0};
Y c= X by XBOOLE_1:1;
then
A117: Y c= NAT by A5;
then
A118: y0 in Y by A116,CARD_1:27,NAT_1:def 1;
then consider x0 be object such that
x0 in dom a and
A119: x0 in g"{k9} and
A120: y0 = a.x0 by FUNCT_1:def 6;
consider y09 be object such that
y09 in rng g and
A121: [x0,y09] in g and
A122: y09 in {k9} by A119,RELAT_1:131;
A123: x0 in dom g by A121,FUNCT_1:1;
A124: g.x0 = y09 by A121,FUNCT_1:1;
reconsider x0 as Element of NAT by A123;
set Y0 = {x where x is Element of omega: ex j being Element of NAT st
a.j=x & j>x0};
{y0} c= y by A115,A118,ZFMISC_1:31;
then
A125: Y9 \/ {a.x0} = y by A120,XBOOLE_1:45;
reconsider a9 = a.x0 as Element of S.x0 by A47;
S.x0 in the_subsets_of_card(omega,X);
then ex S0 be Subset of X st S0=S.x0 & card S0 = omega;
then consider
F0 be Function of the_subsets_of_card(n,S.x0\{a9}),k, H0 be
Subset of S.x0\{a9} such that
H0 is infinite and
F0|the_subsets_of_card(n,H0) is constant and
A126: for Y9 being Element of the_subsets_of_card(n,S.x0\{a9})
holds F0. Y9 = F.(Y9 \/ {a9}) by A7;
reconsider y9=y as finite set by A115,A116;
card Y9 c= card y9 by CARD_1:11;
then reconsider Y99=Y9 as finite set;
A127: Y0 c= S.(x0+1) by A63,A126;
now
let x be object;
assume
A128: x in Y9;
then
A129: x in y;
then consider j be object such that
A130: j in dom a and
j in g"{k9} and
A131: x = a.j by A115,FUNCT_1:def 6;
reconsider x9=x as Element of omega by A115,A117,A129;
A132: not x in {y0} by A128,XBOOLE_0:def 5;
ex j being Element of NAT st a.j=x9 & j>x0
proof
reconsider j as Element of NAT by A130;
take j;
thus a.j=x9 by A131;
A133: y0 <= x9 by A115,A117,A128,NAT_1:def 1;
thus j>x0
proof
assume
A134: x0>=j;
x0<>j by A120,A132,A131,TARSKI:def 1;
hence contradiction by A60,A120,A131,A133,A134;
end;
end;
hence x in Y0;
end;
then
A135: Y9 is Subset of Y0 by TARSKI:def 3;
y0 in {y0} by TARSKI:def 1;
then not a.x0 in Y9 by A120,XBOOLE_0:def 5;
then card y9 = card Y99 + 1 by A125,CARD_2:41;
then
A136: Y9 in the_subsets_of_card(n,Y0) by A115,A116,A135;
ex l be Nat st l=g.x0 & l in k & rng(F0|
the_subsets_of_card(n,Y0)) = {l} by A108,A126;
then
A137: rng(F0|the_subsets_of_card(n,Y0)) = {k9} by A122,A124,TARSKI:def 1;
S.(x0+1) c= S.x0 by A47;
then Y0 c= S.x0 by A127;
then
A138: Y0\{a.x0} c= S.x0\{a.x0} by XBOOLE_1:33;
not a.x0 in Y0 by A47,A127;
then Y0 c= S.x0\{a.x0} by A138,ZFMISC_1:57;
then
A139: the_subsets_of_card(n,Y0) c= the_subsets_of_card(n,S.x0\{a.x0}) by Lm1;
then
A140: Y9 in the_subsets_of_card(n,S.x0\{a.x0}) by A136;
reconsider Y9 as Element of the_subsets_of_card(n,S.x0\{a.x0}) by A139
,A136;
Y9 in dom F0 by A6,A140,FUNCT_2:def 1;
then Y9 in dom(F0|the_subsets_of_card(n,Y0)) by A136,RELAT_1:57;
then F0|the_subsets_of_card(n,Y0).Y9 in rng(F0|the_subsets_of_card(n,
Y0)) by FUNCT_1:3;
then F0|the_subsets_of_card(n,Y0).Y9 = k9 by A137,TARSKI:def 1;
then
A141: F0.Y9 = k9 by A136,FUNCT_1:49;
F0.Y9 = F.(Y9 \/ {a.x0}) by A126;
hence thesis by A114,A125,A141,FUNCT_1:49;
end;
for x,y being object st x in dom(F|the_subsets_of_card(n+1,H)) & y in
dom(F|the_subsets_of_card(n+1,H)) holds F|the_subsets_of_card(n+1,H).x = F|
the_subsets_of_card(n+1,H).y
proof
let x,y be object;
assume x in dom(F|the_subsets_of_card(n+1,H));
then
A142: F|the_subsets_of_card(n+1,H).x = k9 by A113;
assume y in dom(F|the_subsets_of_card(n+1,H));
hence thesis by A113,A142;
end;
hence F|the_subsets_of_card(n+1,H) is constant by FUNCT_1:def 10;
end;
hence thesis;
end;
A143: P[0]
proof
let k be Nat;
let X be set;
set H = X;
H c= X;
then reconsider H as Subset of X;
let F be Function of (the_subsets_of_card(0,X)),k;
assume
A144: card X = omega;
assume X c= omega;
assume k<>0;
take H;
thus H is infinite by A144;
for x,y being object holds x in dom(F|the_subsets_of_card(0,H)) & y in
dom(F|the_subsets_of_card(0,H)) implies F|the_subsets_of_card(0,H).x=F|
the_subsets_of_card(0,H).y
proof
let x,y be object;
assume
A145: x in dom(F|the_subsets_of_card(0,H));
A146: dom(F|the_subsets_of_card(0,H)) = dom(F|{0}) by Lm2
.= dom F /\ {0} by RELAT_1:61;
assume y in dom(F|the_subsets_of_card(0,H));
then y in {0} by A146,XBOOLE_0:def 4;
then
A147: y=0 by TARSKI:def 1;
x in {0} by A146,A145,XBOOLE_0:def 4;
hence thesis by A147,TARSKI:def 1;
end;
hence thesis by FUNCT_1:def 10;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A143,A1);
hence thesis;
end;
theorem
the_subsets_of_card(0,X) = {0} by Lm2;
theorem Th6:
for X being finite set st card X < n holds the_subsets_of_card(n, X) is empty
proof
let X be finite set;
assume
A1: card X < n;
A2: card Seg n = n by FINSEQ_1:57;
assume the_subsets_of_card(n, X) is not empty;
then consider x be object such that
A3: x in the_subsets_of_card(n, X) by XBOOLE_0:def 1;
ex X9 be Subset of X st x=X9 & card X9 = n by A3;
then Segm card Seg n c= Segm card X by A2,CARD_1:11;
then card Seg n <= card X by NAT_1:39;
hence contradiction by A1,FINSEQ_1:57;
end;
theorem
X c= Y implies the_subsets_of_card(Z,X) c= the_subsets_of_card(Z,Y) by Lm1;
theorem
X is finite & Y is finite & card Y = X implies the_subsets_of_card(X,Y) = {Y}
by Lm3;
theorem
X is non empty & Y is non empty implies
(f is constant iff ex y being Element of Y st rng f = {y}) by FUNCT_2:111;
theorem Th10:
for X being finite set st k <= card X ex Y being Subset of X st card Y = k
proof
let X be finite set;
assume k <= card X;
then Segm card k c= Segm card X by NAT_1:39;
then consider Y be set such that
A1: Y c= X and
A2: card Y = card k by CARD_FIL:36;
reconsider Y as Subset of X by A1;
take Y;
thus thesis by A2;
end;
theorem Th11:
m >= 1 implies n+1 <= (n+m) choose m
proof
defpred Q[Nat] means for n being Element of NAT st $1>=1 holds n+1 <= (n+$1)
choose $1;
A1: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
set k9=k+1;
reconsider k9 as Element of NAT;
assume
A2: Q[k];
for n being Element of NAT st k9>=1 holds n+1 <= (n+k9) choose k9
proof
let n be Element of NAT;
assume
A3: k9>=1;
per cases by A3,NAT_1:8;
suppose
A4: k+1=1;
n+1 >= 0+1 by XREAL_1:6;
hence thesis by A4,NEWTON:23;
end;
suppose
A5: k>=1;
(n+k9) choose k9 = (n+k+1) choose (k+1)
.= (n+k) choose (k+1) + (n+k) choose k by NEWTON:22; then
A7: (n+1) + (n+k) choose (k+1) <= (n+k9) choose k9 by XREAL_1:6,A2,A5;
0+(n+1) <= (n+k) choose (k+1) + (n+1) by XREAL_1:6;
hence thesis by A7,XXREAL_0:2;
end;
end;
hence thesis;
end;
reconsider n9=n,m9=m as Element of NAT by ORDINAL1:def 12;
assume
A8: m >= 1;
A9: Q[0];
for k being Nat holds Q[k] from NAT_1:sch 2(A9,A1);
then n9+1 <= (n9+m9) choose m9 by A8;
hence thesis;
end;
theorem Th12:
m >= 1 & n >= 1 implies m+1 <= (n+m) choose m
proof
defpred Q[Nat] means for n being Element of NAT st $1>=1 & n>=1 holds $1+1
<= (n+$1) choose $1;
assume
A1: m >= 1 & n >= 1;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
reconsider m9=m as Element of NAT by ORDINAL1:def 12;
A2: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
set k9=k+1;
reconsider k9 as Element of NAT;
assume
A3: Q[k];
for n being Element of NAT st k9>=1 & n>=1 holds k9+1 <= (n+k9) choose k9
proof
let n be Element of NAT;
assume
A4: k9>=1;
assume
A5: n>=1;
per cases by A4,NAT_1:8;
suppose
A6: k+1=1;
n+1 >= 0+1 & n+1 >= 1+1 by A5,XREAL_1:6;
hence thesis by A6,NEWTON:23;
end;
suppose
A7: k>=1;
set k99=k+1;
A8: (n+k9) choose k9 = (n+k+1) choose (k+1)
.= (n+k) choose (k+1) + (n+k) choose k by NEWTON:22;
k+1>=0+1 by XREAL_1:6;
then
A9: (n-'1) +1 <= (n-'1+k99) choose k99 by Th11;
n-1 >= 1-1 by A5,XREAL_1:9;
then n -' 1 = n - 1 by XREAL_0:def 2;
then 1 <= (n+k) choose (k+1) by A5,A9,XXREAL_0:2;
then
A10: 1+(k+1) <= (n+k) choose (k+1) + (k+1) by XREAL_1:6;
(k+1) + (n+k) choose (k+1) <= (n+k9) choose k9
by A3,A5,A7,A8,XREAL_1:6;
hence thesis by A10,XXREAL_0:2;
end;
end;
hence thesis;
end;
A11: Q[0];
for k being Nat holds Q[k] from NAT_1:sch 2(A11,A2);
then m9+1 <= (n9+m9) choose m9 by A1;
hence thesis;
end;
theorem Th13:
for X being non empty set, p1,p2 being Element of X
for P being a_partition of X, A being Element of P
st p1 in A & (proj P).p1 = (proj P).p2
holds p2 in A
proof
let X be non empty set;
let p1,p2 be Element of X;
let P be a_partition of X;
let A be Element of P;
assume
A1: p1 in A;
assume (proj P).p1=(proj P).p2;
then
A2: (proj P).p2 = A by A1,EQREL_1:65;
assume
A3: not p2 in A;
union P = X by EQREL_1:def 4;
then consider B be set such that
A4: p2 in B and
A5: B in P by TARSKI:def 4;
reconsider B as Element of P by A5;
A6: (proj P).p2 = B by A4,EQREL_1:65;
per cases by EQREL_1:def 4;
suppose
A=B;
hence contradiction by A3,A4;
end;
suppose
A misses B;
hence contradiction by A2,A6;
end;
end;
begin :: Infinite Ramsey Theorem
theorem Th14:
for F being Function of the_subsets_of_card(n,X),k st k<>0 & X is infinite
ex H st H is infinite & F|the_subsets_of_card(n,H) is constant
proof
let F be Function of the_subsets_of_card(n,X),k;
assume that
A1: k<>0 and
A2: X is infinite;
F in Funcs(the_subsets_of_card(n,X),k) by A1,FUNCT_2:8;
then
A3: ex g1 be Function st F=g1 & dom g1=the_subsets_of_card(n,X) & rng g1 c=
k by FUNCT_2:def 2;
consider Y be set such that
A4: Y c= X and
A5: card Y = omega by A2,CARD_3:87;
reconsider Y as non empty set by A5;
Y,omega are_equipotent by A5,CARD_1:5,47;
then consider f be Function such that
A6: f is one-to-one and
A7: dom f = omega and
A8: rng f = Y by WELLORD2:def 4;
reconsider f as Function of omega,Y by A7,A8,FUNCT_2:1;
not card Y c= card n by A5;
then the_subsets_of_card(n,Y) is non empty by GROUP_10:1;
then f||^n in Funcs(the_subsets_of_card(n,omega), the_subsets_of_card(n,Y))
by FUNCT_2:8;
then
A9: ex g2 be Function st f||^n=g2 & dom g2= the_subsets_of_card(n,omega) &
rng g2 c= the_subsets_of_card(n,Y) by FUNCT_2:def 2;
set F9 = F * (f||^n);
the_subsets_of_card(n,Y) c= the_subsets_of_card(n,X) by A4,Lm1;
then
A10: dom F9 = the_subsets_of_card(n,omega) by A3,A9,RELAT_1:27,XBOOLE_1:1;
A11: rng F9 c= rng F by RELAT_1:26;
then
A12: rng F9 c= k by A3;
reconsider F9 as Function of the_subsets_of_card(n,omega),k by A3,A10,A11,
FUNCT_2:2,XBOOLE_1:1;
consider H9 be Subset of omega such that
A13: H9 is infinite and
A14: F9|the_subsets_of_card(n,H9) is constant by A1,Lm4,CARD_1:47;
A15: rng(F9|the_subsets_of_card(n,H9)) c= rng F9 by RELAT_1:70;
set H = f .: H9;
f .: H9 c= rng f by RELAT_1:111;
then reconsider H as Subset of X by A4,A8,XBOOLE_1:1;
take H;
H9,f.:H9 are_equipotent by A6,A7,CARD_1:33;
hence H is infinite by A13,CARD_1:38;
dom(F9|the_subsets_of_card(n,H9)) = the_subsets_of_card(n,H9) by A10,Lm1,
RELAT_1:62;
then
F9|the_subsets_of_card(n,H9) is Function of the_subsets_of_card(n,H9),k
by A12,A15,FUNCT_2:2,XBOOLE_1:1;
then consider y be Element of k such that
A16: rng(F9|the_subsets_of_card(n,H9)) = {y} by A1,A13,A14,FUNCT_2:111;
A17: not card omega c= card n;
A18: ex y being Element of k st rng(F|the_subsets_of_card(n,H)) = {y}
proof
take y;
thus rng(F|the_subsets_of_card(n,H)) = F.:the_subsets_of_card(n,H) by
RELAT_1:115
.= F.:((f||^n) .: the_subsets_of_card(n,H9)) by A6,A17,Th1
.= F9 .: the_subsets_of_card(n,H9) by RELAT_1:126
.= {y} by A16,RELAT_1:115;
end;
thus thesis by A18;
end;
:: theorem 9.1 Set Theory T.Jech
::$N Ramsey's Theorem
::$L https://en.wikipedia.org/wiki/Ramsey's_theorem Ramsey's Theorem
theorem
for X being infinite set, P being a_partition of the_subsets_of_card(n,X)
st card P = k
ex H being Subset of X st H is infinite & H is_homogeneous_for P
proof
let X be infinite set;
let P be a_partition of the_subsets_of_card(n,X);
assume
A1: card P = k;
then P,k are_equipotent by CARD_1:def 2;
then consider F1 be Function such that
A2: F1 is one-to-one and
A3: dom F1 = P and
A4: rng F1 = k by WELLORD2:def 4;
reconsider F1 as Function of P,k by A3,A4,FUNCT_2:1;
set F=F1*proj P;
reconsider F as Function of the_subsets_of_card(n,X),k;
consider H be Subset of X such that
A5: H is infinite and
A6: F|the_subsets_of_card(n,H) is constant by A1,Th14;
take H;
thus H is infinite by A5;
set h = the Element of the_subsets_of_card(n,H);
a7: the_subsets_of_card(n,H) is non empty by A5;
A8: the_subsets_of_card(n,H) c= the_subsets_of_card(n,X) by Lm1;
then reconsider h as Element of the_subsets_of_card(n,X) by a7;
set E = EqClass(h,P);
reconsider E as Element of P by EQREL_1:def 6;
for x being object holds x in the_subsets_of_card(n,H) implies x in E
proof
let x be object;
assume
A9: x in the_subsets_of_card(n,H);
then reconsider x9=x as Element of the_subsets_of_card(n,X) by A8;
A10: dom F = the_subsets_of_card(n,X) by A1,FUNCT_2:def 1;
then h in dom F /\ the_subsets_of_card(n,H) by A5,XBOOLE_0:def 4;
then
A11: h in dom(F|the_subsets_of_card(n,H)) by RELAT_1:61;
x9 in dom F /\ the_subsets_of_card(n,H) by A9,A10,XBOOLE_0:def 4;
then
A12: x9 in dom(F|the_subsets_of_card(n,H)) by RELAT_1:61;
F.x9 = F|the_subsets_of_card(n,H).x9 by A9,FUNCT_1:49
.= F|the_subsets_of_card(n,H).h by A6,A12,A11,FUNCT_1:def 10
.= F.h by A5,FUNCT_1:49;
then F1.((proj P).x9) = (F1*proj P).h by A10,FUNCT_1:12
.= F1.((proj P).h) by A10,FUNCT_1:12;
then h in E & (proj P).h = (proj P).x9 by A2,A3,EQREL_1:def 6,FUNCT_1:def 4
;
hence thesis by Th13;
end;
then the_subsets_of_card(n,H) c= E;
hence thesis;
end;
begin :: Ramsey's Theorem
scheme
BinInd2 { P[Nat,Nat] } : P[m,n]
provided
A1: P[0,n] & P[n,0] and
A2: P[m+1,n] & P[m,n+1] implies P[m+1,n+1]
proof
defpred Q[Nat] means for m,n being Nat st m+n=$1 holds P[m,n];
A3: for k being Nat st Q[k] holds Q[k+1]
proof
let k be Nat;
assume
A4: Q[k];
for m,n being Nat st m+n=k+1 holds P[m,n]
proof
let m,n be Nat;
assume
A5: m+n=k+1;
per cases;
suppose
m=0 or n=0;
hence thesis by A1;
end;
suppose
A6: m<>0 & n<>0;
then reconsider m9=m-1 as Element of NAT by NAT_1:20;
reconsider n9=n-1 as Element of NAT by A6,NAT_1:20;
m9+n=k by A5;
then
A7: P[m9,n9+1] by A4;
m+n9=k by A5;
then P[m9+1,n9] by A4;
hence thesis by A2,A7;
end;
end;
hence thesis;
end;
let m,n;
set k=m+n;
reconsider k as Element of NAT by ORDINAL1:def 12;
A8: Q[0]
proof
let m,n be Nat;
assume m+n=0;
then m=0;
hence thesis by A1;
end;
for k being Nat holds Q[k] from NAT_1:sch 2(A8,A3);
then Q[k];
hence thesis;
end;
:: Chapter 35 proof from THE BOOK Aigner-Ziegler
theorem Th16:
m >= 2 & n >= 2 implies ex r being Nat st r <= (m + n -' 2) choose (m -' 1) &
r >= 2 & for X being finite set,
F being Function of the_subsets_of_card(2,X), Seg 2 st card X >= r
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
defpred P[Nat,Nat] means $1 >= 2 & $2 >= 2 implies ex
r being Nat st r <= ($1 + $2 -' 2) choose ($1 -' 1) & r >= 2 & for X
being finite set, 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 >= $1 & rng(F|the_subsets_of_card(
2,S)) = {1}) or (card S >= $2 & rng(F|the_subsets_of_card(2,S)) = {2});
A1: for n,m being Nat st P[m+1,n] & P[m,n+1] holds P[m+1,n+1]
proof
let n,m be Nat;
assume
A2: P[m+1,n];
assume
A3: P[m,n+1];
assume that
A4: m+1 >= 2 and
A5: n+1 >= 2;
per cases by XXREAL_0:1;
suppose
m+1<2 or n+1<2;
hence thesis by A4,A5;
end;
suppose
A6: m+1=2;
set r=n+1;
take r;
(m+1)+(n+1) >= 2+2 by A4,A5,XREAL_1:7;
then (m+1)+(n+1)-2 >= 4-2 by XREAL_1:9;
then
A7: m+n = (m+1) + (n+1) -' 2 by XREAL_0:def 2;
(m+1) -' 1 = m & m+1-1 >= 2-1 by A4,NAT_D:34,XREAL_1:9;
hence r <= ((m+1) + (n+1) -' 2) choose ((m+1) -' 1) by A7,Th11;
thus r >= 2 by A5;
let X be finite set;
let F be Function of the_subsets_of_card(2,X), Seg 2;
assume
A8: card X >= r;
F in Funcs(the_subsets_of_card(2,X), Seg 2) by FUNCT_2:8;
then
A9: ex f be Function st F = f & dom f = the_subsets_of_card( 2,X) & rng
f c= Seg 2 by FUNCT_2:def 2;
per cases;
suppose
A10: not 1 in rng F;
consider S be Subset of X such that
A11: card S = r by A8,Th10;
card 2 <= card S by A5,A11;
then Segm card 2 c= Segm card S by NAT_1:39;
then the_subsets_of_card(2,S) is non empty by A11,CARD_1:27,GROUP_10:1;
then
A12: ex x be object st x in the_subsets_of_card(2,S) by XBOOLE_0:def 1;
take S;
A13: rng(F|the_subsets_of_card(2,S)) c= rng F by RELAT_1:70;
then
A14: rng(F|the_subsets_of_card(2,S)) c= {1,2} by A9,FINSEQ_1:2;
the_subsets_of_card(2,S) c= the_subsets_of_card(2,X) by Lm1;
then
A15: F|the_subsets_of_card(2,S) <> {} by A9,A12;
now
let x be object;
A16: rng(F|the_subsets_of_card(2,S)) = {} or rng(F|
the_subsets_of_card(2,S)) = {1} or rng(F|the_subsets_of_card(2,S)) = {2} or rng
(F|the_subsets_of_card(2,S)) = {1,2} by A14,ZFMISC_1:36;
hereby
assume
A17: x in rng(F|the_subsets_of_card(2,S));
then x=1 or x=2 by A14,TARSKI:def 2;
hence x=2 by A10,A13,A17;
end;
assume
A18: x=2;
A19: not 1 in rng(F|the_subsets_of_card(2,S)) by A10,A13;
assume not x in rng(F|the_subsets_of_card(2,S));
hence contradiction by A15,A18,A19,A16,TARSKI:def 1,def 2;
end;
hence thesis by A11,TARSKI:def 1;
end;
suppose
1 in rng F;
then consider S be object such that
A20: S in dom F and
A21: 1 = F.S by FUNCT_1:def 3;
S in {X9 where X9 is Subset of X: card X9 = 2} by A20;
then
A22: ex X9 be Subset of X st S=X9 & card X9 = 2;
then reconsider S as Subset of X;
the_subsets_of_card(2,S) = {S} by A22,Lm3;
then S in the_subsets_of_card(2,S) by TARSKI:def 1;
then
A23: F|the_subsets_of_card(2,S).S = 1 by A21,FUNCT_1:49;
take S;
A24: {S} c= dom F by A20,ZFMISC_1:31;
dom(F|the_subsets_of_card(2,S)) = dom F /\ the_subsets_of_card(2,
S) by RELAT_1:61
.= dom F /\ {S} by A22,Lm3
.= {S} by A24,XBOOLE_1:28;
hence thesis by A6,A22,A23,FUNCT_1:4;
end;
end;
suppose
A25: n+1=2;
set r=m+1;
take r;
A26: n+1-1 >= 2-1 by A5,XREAL_1:9;
(m+1)+(n+1) >= 2+2 by A4,A5,XREAL_1:7;
then (m+1)+(n+1)-2 >= 4-2 by XREAL_1:9;
then
A27: m+n = (m+1) + (n+1) -' 2 by XREAL_0:def 2;
(m+1) -' 1 = m & m+1-1 >= 2-1 by A4,NAT_D:34,XREAL_1:9;
hence r <= ((m+1) + (n+1) -' 2) choose ((m+1) -' 1) by A27,A26,Th12;
thus r >= 2 by A4;
let X be finite set;
let F be Function of the_subsets_of_card(2,X), Seg 2;
assume
A28: card X >= r;
F in Funcs(the_subsets_of_card(2,X), Seg 2) by FUNCT_2:8;
then
A29: ex f be Function st F = f & dom f = the_subsets_of_card( 2,X) & rng
f c= Seg 2 by FUNCT_2:def 2;
per cases;
suppose
A30: not 2 in rng F;
consider S be Subset of X such that
A31: card S = r by A28,Th10;
card 2 <= card S by A4,A31;
then Segm card 2 c= Segm card S by NAT_1:39;
then the_subsets_of_card(2,S) is non empty by A31,CARD_1:27,GROUP_10:1;
then
A32: ex x be object st x in the_subsets_of_card(2,S) by XBOOLE_0:def 1;
take S;
A33: rng(F|the_subsets_of_card(2,S)) c= rng F by RELAT_1:70;
then
A34: rng(F|the_subsets_of_card(2,S)) c= {1,2} by A29,FINSEQ_1:2;
the_subsets_of_card(2,S) c= the_subsets_of_card(2,X) by Lm1;
then
A35: F|the_subsets_of_card(2,S) <> {} by A29,A32;
now
let x be object;
A36: rng(F|the_subsets_of_card(2,S)) = {} or rng(F|
the_subsets_of_card(2,S)) = {1} or rng(F|the_subsets_of_card(2,S)) = {2} or rng
(F|the_subsets_of_card(2,S)) = {1,2} by A34,ZFMISC_1:36;
hereby
assume
A37: x in rng(F|the_subsets_of_card(2,S));
then x=1 or x=2 by A34,TARSKI:def 2;
hence x=1 by A30,A33,A37;
end;
assume
A38: x=1;
A39: not 2 in rng(F|the_subsets_of_card(2,S)) by A30,A33;
assume not x in rng(F|the_subsets_of_card(2,S));
hence contradiction by A35,A38,A39,A36,TARSKI:def 1,def 2;
end;
hence thesis by A31,TARSKI:def 1;
end;
suppose
2 in rng F;
then consider S be object such that
A40: S in dom F and
A41: 2 = F.S by FUNCT_1:def 3;
S in {X9 where X9 is Subset of X: card X9 = 2} by A40;
then
A42: ex X9 be Subset of X st S=X9 & card X9 = 2;
then reconsider S as Subset of X;
the_subsets_of_card(2,S) = {S} by A42,Lm3;
then S in the_subsets_of_card(2,S) by TARSKI:def 1;
then
A43: F|the_subsets_of_card(2,S).S = 2 by A41,FUNCT_1:49;
take S;
A44: {S} c= dom F by A40,ZFMISC_1:31;
dom(F|the_subsets_of_card(2,S)) = dom F /\ the_subsets_of_card(2,
S) by RELAT_1:61
.= dom F /\ {S} by A42,Lm3
.= {S} by A44,XBOOLE_1:28;
hence thesis by A25,A42,A43,FUNCT_1:4;
end;
end;
suppose
A45: m+1>2 & n+1>2;
set t = m + n -' 1;
set s = m -' 1;
m + 1 - 2 >= 2 - 2 by A4,XREAL_1:9;
then m -' 1 = m - 1 by XREAL_0:def 2;
then
A46: (m+1) -' 1 = s + 1 by NAT_D:34;
(m+1) + (n+1) >= 2+2 by A4,A5,XREAL_1:7;
then
A47: m+n+2-3 >= 4-3 by XREAL_1:9;
then
A48: m + n -' 1 = m + n - 1 by XREAL_0:def 2;
A49: m + n + 1 -' 2 = m + n + 1 - 2 by A47,XREAL_0:def 2;
m + n >= 0;
then
A50: (m+1) + (n+1) -' 2 = (m+1) + (n+1) - 2 by XREAL_0:def 2
.= t + 1 by A48;
consider r2 be Nat such that
A51: r2 <= (m + (n+1) -' 2) choose (m -' 1) and
r2 >= 2 and
A52: for X being finite set, F being Function of the_subsets_of_card
(2,X), Seg 2 st card X >= r2 holds ex S being Subset of X st card S >= m & rng(
F|the_subsets_of_card(2,S)) = {1} or card S >= n+1 & rng(F|the_subsets_of_card(
2,S)) = {2} by A3,A45,NAT_1:13;
consider r1 be Nat such that
A53: r1 <= ((m+1) + n -' 2) choose ((m+1) -' 1) and
A54: r1 >= 2 and
A55: for X being finite set, F being Function of the_subsets_of_card
(2,X), Seg 2 st card X >= r1 holds ex S being Subset of X st card S >= m+1 &
rng(F|the_subsets_of_card(2,S)) = {1} or card S >= n & rng(F|
the_subsets_of_card(2,S)) = {2} by A2,A45,NAT_1:13;
set r = r1+r2;
take r;
r1+r2 <= ((m+1) + n -' 2) choose ((m+1) -' 1) + (m + (n+1) -' 2)
choose (m -' 1) by A53,A51,XREAL_1:7;
hence r <= ((m+1) + (n+1) -' 2) choose ((m+1) -' 1) by A48,A49,A50,A46,
NEWTON:22;
r1 + r2 >= 0 + 2 by A54,XREAL_1:7;
hence r >= 2;
let X be finite set;
let F be Function of (the_subsets_of_card(2,X)), Seg 2;
assume card X >= r;
then consider S be Subset of X such that
A56: card S = r by Th10;
consider s be object such that
A57: s in S by A54,A56,CARD_1:27,XBOOLE_0:def 1;
set B = {s9 where s9 is Element of S: F.{s,s9} = 2 & {s,s9} in dom F};
set A = {s9 where s9 is Element of S: F.{s,s9} = 1 & {s,s9} in dom F};
F in Funcs(the_subsets_of_card(2,X), Seg 2) by FUNCT_2:8;
then
A58: ex f be Function st F = f & dom f = the_subsets_of_card( 2,X) & rng
f c= Seg 2 by FUNCT_2:def 2;
A59: for x being object holds x in A \/ B iff x in S \ {s}
proof
let x be object;
hereby
assume
A60: x in A \/ B;
per cases by A60,XBOOLE_0:def 3;
suppose
x in A;
then consider s9 be Element of S such that
A61: x = s9 and
F.{s,s9} = 1 and
A62: {s,s9} in dom F;
now
assume x in {s};
then
A63: x = s by TARSKI:def 1;
{s,s9} = {s} \/ {s9} by ENUMSET1:1
.= {s} by A61,A63;
then {s} in the_subsets_of_card(2,X) by A62;
then ex X9 be Subset of X st X9={s} & card X9 = 2;
hence contradiction by CARD_1:30;
end;
hence x in S \ {s} by A54,A56,A61,CARD_1:27,XBOOLE_0:def 5;
end;
suppose
x in B;
then consider s9 be Element of S such that
A64: x = s9 and
F.{s,s9} = 2 and
A65: {s,s9} in dom F;
now
assume x in {s};
then
A66: x = s by TARSKI:def 1;
{s,s9} = {s} \/ {s9} by ENUMSET1:1
.= {s} by A64,A66;
then {s} in the_subsets_of_card(2,X) by A65;
then ex X9 be Subset of X st X9={s} & card X9 = 2;
hence contradiction by CARD_1:30;
end;
hence x in S \ {s} by A54,A56,A64,CARD_1:27,XBOOLE_0:def 5;
end;
end;
assume
A67: x in S \ {s};
then reconsider s9=x as Element of S by XBOOLE_0:def 5;
not s9 in {s} by A67,XBOOLE_0:def 5;
then s<>s9 by TARSKI:def 1;
then
A68: card {s,s9} = 2 by CARD_2:57;
{s,s9} c= S by A57,ZFMISC_1:32;
then {s,s9} is Subset of X by XBOOLE_1:1;
then
A69: {s,s9} in dom F by A58,A68;
then
A70: F.{s,s9} in rng F by FUNCT_1:3;
per cases by A58,A70,FINSEQ_1:2,TARSKI:def 2;
suppose
F.{s,s9} = 1;
then x in A by A69;
hence thesis by XBOOLE_0:def 3;
end;
suppose
F.{s,s9} = 2;
then x in B by A69;
hence thesis by XBOOLE_0:def 3;
end;
end;
A71: now
assume A /\ B <> {};
then consider x be object such that
A72: x in A /\ B by XBOOLE_0:def 1;
x in B by A72,XBOOLE_0:def 4;
then
A73: ex s2 be Element of S st x = s2 & F.{s,s2} = 2 & {s,s2} in dom F;
x in A by A72,XBOOLE_0:def 4;
then ex s1 be Element of S st x = s1 & F.{s,s1} = 1 & {s,s1} in dom F;
hence contradiction by A73;
end;
S \ {s} c= S by XBOOLE_1:36;
then
A74: A \/ B c= S by A59;
{s} c= S by A57,ZFMISC_1:31;
then
A75: card(S \ {s}) = card S - card {s} by CARD_2:44
.= r1 + r2 - 1 by A56,CARD_1:30;
reconsider B as finite Subset of S by A74,XBOOLE_1:11;
reconsider A as finite Subset of S by A74,XBOOLE_1:11;
card (A \/ B) = card A + card B - card {} by A71,CARD_2:45
.= card A + card B;
then
A76: card A + card B = r1 + r2 - 1 by A59,A75,TARSKI:2;
A77: card A >= r2 or card B >= r1
proof
assume card A < r2;
then
A78: card A + 1 <= r2 by NAT_1:13;
assume card B < r1;
then card A + 1 + card B < r2 + r1 by A78,XREAL_1:8;
hence contradiction by A76;
end;
per cases by A77;
suppose
A79: card A >= r2;
set F9 = F|the_subsets_of_card(2,A);
A c= X by XBOOLE_1:1;
then the_subsets_of_card(2,X) /\ the_subsets_of_card(2,A) =
the_subsets_of_card(2,A) by Lm1,XBOOLE_1:28;
then
A80: dom(F|the_subsets_of_card(2,A)) = the_subsets_of_card(2,A) by A58,
RELAT_1:61;
rng(F|the_subsets_of_card(2,A)) c= rng F by RELAT_1:70;
then reconsider
F9 as Function of the_subsets_of_card(2,A), Seg 2 by A58,A80,FUNCT_2:2
,XBOOLE_1:1;
consider S9 be Subset of A such that
A81: card S9 >= m & rng(F9|the_subsets_of_card(2,S9)) = {1} or
card S9 >= n+1 & rng(F9|the_subsets_of_card(2,S9)) = {2} by A52,A79;
A82: F9|the_subsets_of_card(2,S9) = F|the_subsets_of_card(2,S9) by Lm1,
RELAT_1:74;
A c= X by XBOOLE_1:1;
then reconsider S9 as Subset of X by XBOOLE_1:1;
per cases by A81;
suppose
A83: card S9 >= n+1 & rng(F9|the_subsets_of_card(2,S9)) = {2};
take S9;
thus thesis by A83,Lm1,RELAT_1:74;
end;
suppose
A84: card S9 >= m & rng(F9|the_subsets_of_card(2,S9)) = {1};
set S99 = S9 \/ {s};
{s} c= X by A57,ZFMISC_1:31;
then reconsider S99 as Subset of X by XBOOLE_1:8;
A85: the_subsets_of_card(2,S9) c= the_subsets_of_card(2,S99) by Lm1,
XBOOLE_1:7;
A86: rng(F|the_subsets_of_card(2,S9)) = {1} by A84,Lm1,RELAT_1:74;
A87: for y being object holds y in rng(F|the_subsets_of_card(2,S99))
iff y = 1
proof
let y be object;
F|the_subsets_of_card(2,S9) c= F|the_subsets_of_card(2,S99)
by A85,RELAT_1:75;
then
A88: rng(F|the_subsets_of_card(2,S9)) c= rng(F|
the_subsets_of_card(2,S99)) by RELAT_1:11;
hereby
assume y in rng(F|the_subsets_of_card(2,S99));
then consider x be object such that
A89: x in dom(F|the_subsets_of_card(2,S99)) and
A90: y = (F|the_subsets_of_card(2,S99)).x by FUNCT_1:def 3;
A91: x in the_subsets_of_card(2,S99) by A89,RELAT_1:57;
A92: x in dom F by A89,RELAT_1:57;
x in {S999 where S999 is Subset of S99: card S999 = 2} by A89,
RELAT_1:57;
then consider S999 be Subset of S99 such that
A93: x=S999 and
A94: card S999 = 2;
consider s1,s2 be object such that
A95: s1 <> s2 and
A96: S999 = {s1,s2} by A94,CARD_2:60;
A97: s1 in S999 by A96,TARSKI:def 2;
A98: s2 in S999 by A96,TARSKI:def 2;
per cases by A97,XBOOLE_0:def 3;
suppose
A99: s1 in S9;
per cases by A98,XBOOLE_0:def 3;
suppose
s2 in S9;
then reconsider x as Subset of S9 by A93,A96,A99,ZFMISC_1:32;
x in the_subsets_of_card(2,S9) by A93,A94;
then
A100: x in dom(F|the_subsets_of_card(2,S9)) by A92,RELAT_1:57;
then
A101: x in dom(F|the_subsets_of_card(2,S99)|
the_subsets_of_card(2,S9)) by A85,RELAT_1:74;
(F|the_subsets_of_card(2,S9)).x = (F|
the_subsets_of_card(2,S99)|the_subsets_of_card(2,S9)).x by A85,RELAT_1:74
.= (F|the_subsets_of_card(2,S99)).x by A101,FUNCT_1:47;
then y in rng(F|the_subsets_of_card(2,S9)) by A90,A100,
FUNCT_1:3;
hence y = 1 by A82,A84,TARSKI:def 1;
end;
suppose
A102: s2 in {s};
s1 in A by A99;
then
A103: ex s99 be Element of S st s1=s99 & F.{s,s99} = 1 & {s,
s99} in dom F;
x = {s1,s} by A93,A96,A102,TARSKI:def 1;
hence y = 1 by A90,A91,A103,FUNCT_1:49;
end;
end;
suppose
A104: s1 in {s};
then
A105: s <> s2 by A95,TARSKI:def 1;
per cases by A98,XBOOLE_0:def 3;
suppose
s2 in S9;
then s2 in A;
then ex s99 be Element of S st s2=s99 & F.{s,s99} = 1 & {s,
s99} in dom F;
then F.x = 1 by A93,A96,A104,TARSKI:def 1;
hence y = 1 by A90,A91,FUNCT_1:49;
end;
suppose
s2 in {s};
hence y=1 by A105,TARSKI:def 1;
end;
end;
end;
assume y = 1;
then y in rng(F|the_subsets_of_card(2,S9)) by A86,TARSKI:def 1;
hence thesis by A88;
end;
take S99;
A106: not s in S9
proof
assume s in S9;
then s in A;
then
A107: ex s9 be Element of S st s=s9 & F.{s,s9} = 1 & {s,s9} in dom F;
{s,s} = {s} \/ {s} by ENUMSET1:1
.= {s};
then {s} in the_subsets_of_card(2,X) by A107;
then ex X9 be Subset of X st X9={s} & card X9 = 2;
hence contradiction by CARD_1:30;
end;
card S9 + 1 >= m + 1 by A84,XREAL_1:6;
hence thesis by A87,A106,CARD_2:41,TARSKI:def 1;
end;
end;
suppose
A108: card B >= r1;
set F9 = F|the_subsets_of_card(2,B);
B c= X by XBOOLE_1:1;
then the_subsets_of_card(2,X) /\ the_subsets_of_card(2,B) =
the_subsets_of_card(2,B) by Lm1,XBOOLE_1:28;
then
A109: dom(F|the_subsets_of_card(2,B)) = the_subsets_of_card(2,B) by A58,
RELAT_1:61;
rng(F|the_subsets_of_card(2,B)) c= rng F by RELAT_1:70;
then reconsider
F9 as Function of the_subsets_of_card(2,B), Seg 2 by A58,A109,FUNCT_2:2
,XBOOLE_1:1;
consider S9 be Subset of B such that
A110: card S9 >= m+1 & rng(F9|the_subsets_of_card(2,S9)) = {1} or
card S9 >= n & rng(F9|the_subsets_of_card(2,S9)) = {2} by A55,A108;
A111: F9|the_subsets_of_card(2,S9) = F|the_subsets_of_card(2,S9) by Lm1,
RELAT_1:74;
B c= X by XBOOLE_1:1;
then reconsider S9 as Subset of X by XBOOLE_1:1;
per cases by A110;
suppose
A112: card S9 >= m+1 & rng(F9|the_subsets_of_card(2,S9)) = {1};
take S9;
thus thesis by A112,Lm1,RELAT_1:74;
end;
suppose
A113: card S9 >= n & rng(F9|the_subsets_of_card(2,S9)) = {2};
set S99 = S9 \/ {s};
{s} c= X by A57,ZFMISC_1:31;
then reconsider S99 as Subset of X by XBOOLE_1:8;
A114: the_subsets_of_card(2,S9) c= the_subsets_of_card(2,S99) by Lm1,
XBOOLE_1:7;
A115: rng(F|the_subsets_of_card(2,S9)) = {2} by A113,Lm1,RELAT_1:74;
A116: for y being object holds y in rng(F|the_subsets_of_card(2,S99))
iff y = 2
proof
let y be object;
F|the_subsets_of_card(2,S9) c= F|the_subsets_of_card(2,S99)
by A114,RELAT_1:75;
then
A117: rng(F|the_subsets_of_card(2,S9)) c= rng(F|
the_subsets_of_card(2,S99)) by RELAT_1:11;
hereby
assume y in rng(F|the_subsets_of_card(2,S99));
then consider x be object such that
A118: x in dom(F|the_subsets_of_card(2,S99)) and
A119: y = (F|the_subsets_of_card(2,S99)).x by FUNCT_1:def 3;
A120: x in the_subsets_of_card(2,S99) by A118,RELAT_1:57;
A121: x in dom F by A118,RELAT_1:57;
x in {S999 where S999 is Subset of S99: card S999 = 2} by A118,
RELAT_1:57;
then consider S999 be Subset of S99 such that
A122: x=S999 and
A123: card S999 = 2;
consider s1,s2 be object such that
A124: s1 <> s2 and
A125: S999 = {s1,s2} by A123,CARD_2:60;
A126: s1 in S999 by A125,TARSKI:def 2;
A127: s2 in S999 by A125,TARSKI:def 2;
per cases by A126,XBOOLE_0:def 3;
suppose
A128: s1 in S9;
per cases by A127,XBOOLE_0:def 3;
suppose
s2 in S9;
then reconsider x as Subset of S9 by A122,A125,A128,
ZFMISC_1:32;
x in the_subsets_of_card(2,S9) by A122,A123;
then
A129: x in dom(F|the_subsets_of_card(2,S9)) by A121,RELAT_1:57;
then
A130: x in dom(F|the_subsets_of_card(2,S99)|
the_subsets_of_card(2,S9)) by A114,RELAT_1:74;
(F|the_subsets_of_card(2,S9)).x = (F|
the_subsets_of_card(2,S99)|the_subsets_of_card(2,S9)).x by A114,RELAT_1:74
.= (F|the_subsets_of_card(2,S99)).x by A130,FUNCT_1:47;
then y in rng(F|the_subsets_of_card(2,S9)) by A119,A129,
FUNCT_1:3;
hence y = 2 by A111,A113,TARSKI:def 1;
end;
suppose
A131: s2 in {s};
s1 in B by A128;
then
A132: ex s99 be Element of S st s1=s99 & F.{s,s99} = 2 & {s,
s99} in dom F;
x = {s1,s} by A122,A125,A131,TARSKI:def 1;
hence y = 2 by A119,A120,A132,FUNCT_1:49;
end;
end;
suppose
A133: s1 in {s};
then
A134: s <> s2 by A124,TARSKI:def 1;
per cases by A127,XBOOLE_0:def 3;
suppose
s2 in S9;
then s2 in B;
then ex s99 be Element of S st s2=s99 & F.{s,s99} = 2 & {s,
s99} in dom F;
then F.x = 2 by A122,A125,A133,TARSKI:def 1;
hence y = 2 by A119,A120,FUNCT_1:49;
end;
suppose
s2 in {s};
hence y = 2 by A134,TARSKI:def 1;
end;
end;
end;
assume y = 2;
then y in rng(F|the_subsets_of_card(2,S9)) by A115,TARSKI:def 1;
hence thesis by A117;
end;
take S99;
A135: not s in S9
proof
assume s in S9;
then s in B;
then
A136: ex s9 be Element of S st s=s9 & F.{s,s9} = 2 & {s,s9} in dom F;
{s,s} = {s} \/ {s} by ENUMSET1:1
.= {s};
then {s} in the_subsets_of_card(2,X) by A136;
then ex X9 be Subset of X st X9={s} & card X9 = 2;
hence contradiction by CARD_1:30;
end;
card S9 + 1 >= n + 1 by A113,XREAL_1:6;
hence thesis by A116,A135,CARD_2:41,TARSKI:def 1;
end;
end;
end;
end;
A137: for n being Nat holds P[0,n] & P[n,0];
for n,m being Nat holds P[m,n] from BinInd2(A137,A1);
hence thesis;
end;
::$N Ramsey's Theorem (finite case)
theorem
for m being Nat holds
ex r being Nat st
for X being finite set, 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
let m be Nat;
per cases;
suppose
A1: m<2;
set r=1;
take r;
let X be finite set;
let P be a_partition of the_subsets_of_card(2,X);
assume card X >= r;
then consider x be object such that
A2: x in X by CARD_1:27,XBOOLE_0:def 1;
reconsider S = {x} as Subset of X by A2,ZFMISC_1:31;
assume card P = 2;
take S;
m<1+1 by A1;
then m<=1 by NAT_1:13;
hence card S >= m by CARD_1:30;
A3: card S = 1 by CARD_1:30;
ex p being Element of P st the_subsets_of_card(2,S) c= p
proof
take p = the Element of P;
thus thesis by A3,Th6;
end;
hence thesis;
end;
suppose
m>=2;
then consider r be Nat such that
r <= (m + m -' 2) choose (m -' 1) and
A4: r >= 2 and
A5: for X being finite set, 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 >= m & rng(F|the_subsets_of_card(2,S)
) = {2} by Th16;
take r;
let X be finite set;
let P be a_partition of the_subsets_of_card(2,X);
assume that
A6: card X >= r and
A7: card P = 2;
2 <= card X by A4,A6,XXREAL_0:2;
then card Seg 2 <= card X by FINSEQ_1:57;
then Segm card Seg 2 c= Segm card X by NAT_1:39;
then card 2 c= card X by FINSEQ_1:55;
then reconsider X9 = the_subsets_of_card(2,X) as non empty set by A4,A6,
CARD_1:27,GROUP_10:1;
reconsider P9=P as a_partition of X9;
card P9 = card Seg 2 by A7,FINSEQ_1:57;
then P9, Seg 2 are_equipotent by CARD_1:5;
then consider F1 be Function such that
A8: F1 is one-to-one and
A9: dom F1 = P9 and
A10: rng F1 = Seg 2 by WELLORD2:def 4;
reconsider F1 as Function of P9,Seg 2 by A9,A10,FUNCT_2:1;
set F=F1*(proj P9);
reconsider F as Function of the_subsets_of_card(2,X),Seg 2;
consider S be Subset of X such that
A11: card S >= m & rng(F|the_subsets_of_card(2,S)) = {1} or card S >=
m & rng(F|the_subsets_of_card(2,S)) = {2} by A5,A6;
take S;
thus card S >= m by A11;
set h = the Element of the_subsets_of_card(2,S);
A12: the_subsets_of_card(2,S) is non empty by A11;
then
A13: h in the_subsets_of_card(2,S);
A14: the_subsets_of_card(2,S) c= the_subsets_of_card(2,X) by Lm1;
then reconsider h as Element of X9 by A13;
set E = EqClass(h,P9);
reconsider E as Element of P by EQREL_1:def 6;
A15: F|the_subsets_of_card(2,S) is constant by A11;
for x being object holds x in the_subsets_of_card(2,S) implies x in E
proof
let x be object;
assume
A16: x in the_subsets_of_card(2,S);
then reconsider x9=x as Element of the_subsets_of_card(2,X) by A14;
reconsider x99=x as Element of X9 by A14,A16;
A17: dom F = the_subsets_of_card(2,X) by FUNCT_2:def 1;
then h in dom F /\ the_subsets_of_card(2,S) by A12,XBOOLE_0:def 4;
then
A18: h in dom(F|the_subsets_of_card(2,S)) by RELAT_1:61;
x9 in dom F /\ the_subsets_of_card(2,S) by A16,A17,XBOOLE_0:def 4;
then
A19: x9 in dom(F|the_subsets_of_card(2,S)) by RELAT_1:61;
F.x9 = F|the_subsets_of_card(2,S).x9 by A16,FUNCT_1:49
.= F|the_subsets_of_card(2,S).h by A15,A19,A18,FUNCT_1:def 10
.= F.h by A12,FUNCT_1:49;
then
A20: F1.((proj P9).x9) = (F1*proj P9).h by A17,FUNCT_1:12
.= F1.((proj P9).h) by A17,FUNCT_1:12;
(proj P9).x99 in P9;
then h in E & (proj P9).h = (proj P9).x9 by A8,A9,A20,EQREL_1:def 6
,FUNCT_1:def 4;
hence thesis by Th13;
end;
then the_subsets_of_card(2,S) c= E;
hence thesis;
end;
end;