[isabelle-dev] Reorganising Analysis
Fabian Immler
immler at in.tum.de
Tue Nov 5 04:13:00 CET 2019
On 11/4/2019 1:41 PM, Fabian Immler wrote:
> I just checked: it is easy to remove Path_Connected and Starlike from
> the imports of Ordered_Euclidean_Space:
But for now (b212ee44f87c), I kept Starlike as one import of
Multivariate_Analysis:
Much of it belongs conceptually to Convex_Euclidean_Space (which is part
of Multivariate_Analysis) and several AFP-entries depend on material
from Starlike.
Starlike is a huge (8000loc) conglomeration and it may well be that we
don't need all of it in a "Basic Analysis" session.
In a first attempt to get a better overview what is in there and why, I
split off a theory about line segments (c2465b429e6e).
Then there is a lot (>2000loc) of material about relative
interior/frontiers, which is a concept defined for convex sets, so
perhaps it fits better in Convex_Euclidean_Space or (given the size) a
seperate theory.
For the rest of the theory I could not identify clear topics anymore -
the part on affine dimension might be worth separating from the rest.
I only know that "Starlike" is a misnomer: there is just one definition
and three lemmas about starlike sets in this huge theory.
Fabian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20191104/bf0c08a9/attachment.bin>
More information about the isabelle-dev
mailing list