let n, k be Nat; :: thesis: 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 )
let X be infinite set ; :: thesis: 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 )
let P be a_partition of the_subsets_of_card (n,X); :: thesis: ( card P = k implies ex H being Subset of X st
( H is infinite & H is_homogeneous_for P ) )
assume A1: card P = k ; :: thesis: ex H being Subset of X st
( H is infinite & H is_homogeneous_for P )
then P,k are_equipotent by CARD_1:def 2;
then consider F1 being 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 = F1 as Function of P,k by A3, A4, FUNCT_2:1;
set F = F1 * (proj P);
reconsider F = F1 * (proj P) as Function of (the_subsets_of_card (n,X)),k ;
consider H being 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 ; :: thesis: ( H is infinite & H is_homogeneous_for P )
thus H is infinite by A5; :: thesis: H is_homogeneous_for P
set h = the Element of the_subsets_of_card (n,H);
a7: not the_subsets_of_card (n,H) is empty by A5;
A8: the_subsets_of_card (n,H) c= the_subsets_of_card (n,X) by Lm1;
then reconsider h = the Element of the_subsets_of_card (n,H) as Element of the_subsets_of_card (n,X) by a7;
set E = EqClass (h,P);
reconsider E = EqClass (h,P) as Element of P by EQREL_1:def 6;
for x being object st x in the_subsets_of_card (n,H) holds
x in E then the_subsets_of_card (n,H) c= E ;
hence H is_homogeneous_for P ; :: thesis: verum