[isabelle-dev] Reorganising Analysis

[Lawrence Paulson]

With a little help from Fabian, I managed to prove the inverse function theorem and therefore to reduce somewhat the theories involved in building Complex_Transcendental, which can now be combined with Complex_Analysis_Basics. There are still 25 ancestor theories. Arguably this material should be moved to its own directory, Complex_Analysis. This development would include quite a bit of basic topology but no integration or measure theory.

If we do this as the first step, the next step should become clearer. I already think it might be based on integration. Any thoughts or reactions?




Larry

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/69684029/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Screenshot 2019-11-04 at 11.25.42.png
Type: image/png
Size: 600354 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/69684029/attachment-0001.png>