Re: A question

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

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.

Josef Urban


On Thu, 31 May 2001, Piotr Rudnicki wrote:

> Hi:
> 
> 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
> 
> To my surprise I cannot find such a theorem or a scheme in MML.
> Maybe I am looking for a wrong thing?
> 
> 	
> -- 
> 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.
>