Re: A question

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

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.