Hi Piotr's problem has been sorted out. What I am asking for is somehow relating. See the attachment. Regards - Antoni Urban ----- Original Message ----- From: Piotr Rudnicki <piotr@cs.ualberta.ca> To: <mizar-forum@mizar.uwb.edu.pl> Sent: Friday, June 01, 2001 7:11 AM Subject: Re: A question > Thanks. Silly me was looking only for NAT. > > Still it is a bit surprising that I could not find the theorem > in the shape I wanted. I am mizaring now the Dickson lemma and need to > use it many times. > > PR > > On Fri, Jun 01, 2001 at 09:39:12AM +0900, Grzegorz Bancerek wrote: > > > > I am looking for a fact like this: > > > > > > > > for X being infinite set > > > > ex f being Function of NAT, X st f is one-to-one > > > > Piotr Rudnicki > > > > Josef Urban wrote: > > > > > > A bit of grepping through CARDs gave this: > > > > > > theorem :: CARD_1:26 > > > Card X <=` Card Y iff ex f st f is one-to-one & dom f = X & rng f c= Y; > > > > > > theorem :: CARD_4:2 > > > X is finite iff Card X <` alef 0; > > > > > > maybe there is shorter way. > > > > Together with CARD_1:26 you may use also > > > > theorem :: CARD_1:83 > > alef 0 = omega; > > > > theorem :: CARD_4:1 > > X is finite iff Card X is finite; > > > > theorem :: CARD_4:11 > > not M is finite iff alef 0 c= M; > > > > The predicate <=` is a synonym of c= > > NAT is a synomym of omega, > > and infinite is an antonym of finite. > > > > Grzegorz > > -- > Piotr Rudnicki CompSci, Univerity of Alberta, Edmonton, Canada > email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr > > I am a fundamentalist: always fun before mental. >
Attachment:
Cardinal.gif
Description: GIF image
