Re: [isabelle] property of infinite cardinals



Andrei Popescu wrote:
> (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?

Yes. See Library/Zorn.thy

> Is there any theory of ordinals developed in Isabelle/HOL?)

Yes. See http://afp.sourceforge.net/entries/Ordinal.shtml

Tobias

> Thank you in advance, 
>    Andrei Popescu 
> 
> 
> 
>       






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