Re: [isabelle] proving finite universe
the theory HOL/Library/Infinite_Set contains several lemmas that can be
useful here. In particular, it proves that a set if infinite iff it
contains a countable subset (lemma infinite_iff_countable_subset), which
should help you to prove your goal.
Chris Osborn wrote:
Does anyone know how I can prove the following:
"not (finite (UNIV::string set))"
I have been unable to find applicable lemmas.
Thanks in advance,
org:INRIA Nancy & LORIA
adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France
email;internet:Stephan.Merz at loria.fr
tel;work:(+33) 354 95 84 78
tel;fax:(+33) 383 41 30 79
This archive was generated by a fusion of
Pipermail (Mailman edition) and