Expand the notation `{within _, _ _}`?

[IshiguroYoshihiro]

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".

analysis/theories/realfun.v

Lines 1169 to 1171 in 3b30884

	Definition derivable_oo_continuous_bnd (f : R -> V) (x y : R) :=
	[/\ {in `]x, y[, forall x, derivable f x 1},
	f @ x^'+ --> f x & f @ y^'- --> f y].

This predicate is used mainly in FTC2. For example, the lemma continuous_FTC2:

analysis/theories/ftc.v

Lines 545 to 549 in 3b30884

	Corollary continuous_FTC2 f F a b : (a < b)%R ->
	{within `[a, b], continuous f} ->
	derivable_oo_continuous_bnd F a b ->
	{in `]a, b[, F^`() =1 f} ->
	(\int[mu]_(x in `[a, b]) (f x)%:E = (F b)%:E - (F a)%:E)%E.

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.

[t6s]

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?

[t6s]

(though derivability needs more structure than just topology, so it will not actually be "any" topological space. manifolds?)