math-comp
Expand the notation `{within _, _ _}`?
There is the notation {within i, continuous f} for an interval i and function f : R -> R where R : realType, but this notation {within i, ...} can used only for continuity.
There is a similar definition, the predicate derivable_oo_continuous_bnd, is used to express "continuous within a closed interval and derivable in the interior".
https://github.com/math-comp/analysis/blob/3b30884c4a9134f8c98cfab47c9cfa7f6fd4db0d/theories/realfun.v#L1169-L1171
This predicate is used mainly in FTC2. For example, the lemma continuous_FTC2:
https://github.com/math-comp/analysis/blob/3b30884c4a9134f8c98cfab47c9cfa7f6fd4db0d/theories/ftc.v#L545-L549
The assumptions in continuous_FTC2 will be "F is a C1 class function over [a, b]" but it separates into three in the statement, and continuous_FTC2 requires users to take derivative of F in advance.
I think this shows the one of needs of extension the within notation.
If it can be written as {within `[a, b], derivable F} as the existence of the derivative over [a, b], I wonder that continuous_FTC2 wouldn't requires a well-processed derivative and become more useful.
I also think that the extension would relate to defining the set of C^n class functions over an interval.
that notion seems to deserve a definition and a notation. what about generalizing it a bit as "continuous within X and derivable in the interior of X" for any set X in any topological space?
(though derivability needs more structure than just topology, so it will not actually be "any" topological space. manifolds?)