Re: [isabelle] property of infinite cardinals



Andrei Popescu wrote:
> Hello, 
> 
> I was wondering if one [has proved]/[can prove] in Isabelle/HOL that any infinite type 'a has an injection from 'a * 'a to 'a.  Namely:
> 
> definition 
>   injective :: "('a => 'b) => bool"
> where 
>   "injective f == ALL x x'. f x = f x' --> x = x'"

A grep for "injective" will quickly show you that it already exists
under the name "inj" (and the related "inj_on").

Regards
Tobias


> lemma 
> "~ finite(UNIV::'a set) ==> EX (f :: ('a * 'a) => 'a). injective f"
> 
> (At least for well-ordered 'a should be provable.  Related question: can one prove (similarly to the case of ZF+Choice) that any type can be well-ordered?  Is there any theory of ordinals developed in Isabelle/HOL?)
> 
> Thank you in advance, 
>    Andrei Popescu 
> 
> 
> 
>       






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.