# [isabelle] property of infinite cardinals

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'"
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.*