Re: [isabelle] proving finite universe



Chris,

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.

Best,
Stephan

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,
Chris
begin:vcard
fn:Stephan Merz
n:Merz;Stephan
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
x-mozilla-html:FALSE
url:http://www.loria.fr/~merz/
version:2.1
end:vcard



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