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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
