[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