Re: A question

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

> > 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