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