{in A, continuous f} has bad boundary conditions

[zstone1]

Phrases like {in [a, b], continuous f} appear in various places in the repo (such as MVT). This phrasing is a little too strong. In MVT, it requires f be continuous from the left at a, but we shouldn't have to care about values f takes outside of [a,b]. This mixes particularly poorly with restrict, and other piecewise definitions. I've got two approaches, and I don't like either.

a) We can define {within A, continuous f} notation that somehow replaces filters with within A versions. Even if you could define such a notation, the downside is existing continuity results won't apply directly.
b) We can use Tietze Extension Theorem-style alterations on f, but this is awkward as well. And it may not be possible for sets that are neither open or closed.

Is there an elegant way to fix this statement to mean the right thing?

[CohenCyril]

Yes you are right, I stumbled on the same issue some time ago, I have a solution based on having an alias to point out the subset topology relatively to a set A, which could be named e.g. {within A}, the filter would indeed be the within A F of original filtersF. Continuity in such a space could then be expressed as: continuous (f : {within A} -> T), and we could have a notation {within A, forall x, P x} = forall x : {within A}, P x which would work in particular for continuous but also anything. One could then combine it with for: {for x, {within A, continuous f}}.

[zstone1]

Well, I can't get the notations described above to work. I'd like to define

Context {T: topologicalType}.
Definition prop_within1 (A : set T) P & (phantom Prop (forall (x : (subspace A)), P x : Prop)) := 
  {in (A : set (subspace A)), forall (x: subspace A), P x}.
Notation "'{within' A , P }" := (@prop_within1 A _ (Phantom Prop P)).
Lemma withinATest {U: topologicalType} (A : set T) (f : T -> U) : 
  {in A, continuous (f : subspace A -> U)} =
  {within A, continuous f}.

This all typechecks, but it's seems like a deadend approach. Using {within A, forall x, f @ x --> f x}. fails just the same, but highlights the real issue: The order of inferring implicits is all wrong. I think the following is happening, but one of you may be a better idea

1. It first typechecks continuous f
2. It fills the hole of the filteredType of x as a T.
3. Then it needs to typecheck the phantom. It observes that subspace A and T are unifiable, so it succeds.
4. The P that is extracted is a forall x, (subspace A),...), but, the filteredType under the @ is still T.

I do not know how to resolve this. Can we change the order of evaluation here?

[CohenCyril]

I do not know how to resolve this. Can we change the order of evaluation here?

I think you are right about the unification order. I do not know yet how to do things properly. I'll let it sink in during my Christmas holidays.