Re: [Isarmathlib-devel] A contribution

[daniel]

I did some more work. From now on, the web page you should check for my
files is just:

https://belenus.unirioja.es/~daconcep/

The real numbers are not so easy to work with, the metric spaces need some rewriting.

In the case of the partitions, I tried to work with the existing definition, but my skills
with this kind of functions is very limited. I'm used to HOL.

By the way, in the context real0 and real1 there is mistake (copy-paste, I guess). The "minus" for reals and integers have the same name for their definition rule (rminus_def). I guess on the integers was supposed to be
"iminus_def".

Daniel

>Is there any particular topology that may be useful to include for future work?

Metric spaces would be interesting. Historically, the equivalence of Heine and Cauchy definitions of convergence was one of first things that were noticed (by Sierpinski) to be dependent on the Axiom of Choice. But I think it's best to write about things that interest you, or the background for them if that is too far off.

Slawekk

---

From: daniel <address@hidden>
To: address@hidden
Sent: Thursday, September 6, 2012 4:18 PM
Subject: Re: [Isarmathlib-devel] A contribution

I'll write more informal text and try to change the style. I'll keep the html document updated.
Is there any particular topology that may be useful to include for future work?

Daniel

_______________________________________________
Isarmathlib-devel mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/isarmathlib-devel