Fix boundary conditions with subspace

[zstone1]

Fixes #408 (except in realfun.v. We should open another ticket for that, as it's a bit more work).

This

1. introduces a notation {within A, continuous f}, to indicate continuity on the subspace. This is hacky, and needs fixing (see {in A, continuous f} has bad boundary conditions #408) for further discussion
2. A bunch of additional lemmas about subspaces, their continuity, and closed sets
3. Fixes boundary conditions for
   a. continuous image of connected is connected
   b. continuous image of compact is compact
   c. EVT, and it's friends, including Rolle's theorem, and MVT.
   d. interval_connectedP, and IVT, including a dramatic simplification of that proof.

Note that I use some scaffolding code for realfun.v to change the {in I, continuous f} to {within I, continuous f}. It's not much, but rewriting the whole thing is a lot of lines changed, and requires a couple tougher lemmas (such as letting us convert between fmap f (nbhs {subspace A} x) and nbhs {subspace (f@A)} f awhen f is a homeomorphism). Specifically, this comes up insegment_can_ge, where the subspace swaps from [a,b]to[-b, -a]`.

I think the scaffolding in realfun.v is fine, and can be handled in a separate diff. The notation should be fixed, at least.

[zstone1]

Merges are all resolved here. Build is broken, but that seems to be affecting more than just this change. Can we get this into the next release?

[affeldt-aist]

I proof-read the changes and only found minor improvements. It is ok to merge with me.