[isabelle-dev] Reorganising Analysis
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
Much of it belongs conceptually to Convex_Euclidean_Space (which is part
of Multivariate_Analysis) and several AFP-entries depend on material
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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev