I'm extremely hesitant to suggest changes to the main database, having flunked out of school now twice, but working on what I call "cmpcvxhmph" and "cmpcvxhmph0" (i.e., that any complex convex shape is homeomorphic to the unit ball), I'm finding myself very often relying on the property expressed in fnconstg, and I'm wondering whether it might be better expressed as an fnconst, or even fnconstd, as since I've started on this project ovexd, fvexd, and fzfid have been introduced.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cd6c5c92-0f64-47db-9600-920b2b37f64bn%40googlegroups.com.
