#Contents# * table of contents {:toc} ## Definition ## For a [[calculus field]] $F$ and a subtype $S \subseteq F$, the types of functions $S \to F$, [[pointwise continuous function]]s $C^0(S, F)$, and [[differentiable function]]s $D^1(S, F)$ between $S$ and $F$ are subtypes of the type of functions $S \to F$. For the [[Newton-Leibniz operator]] $\tilde{D}: D^1(S, F) \to (S \to F)$, the type of __$n$-fold iterated differentiable functions__ between $S$ and $F$ is the $n$-fold [[iterated inverse image]] of $S \to F$ under the Newton-Leibniz operator: $$D^0(S, F) := \tilde{D}^{-0}(S \to F) := S \to F$$ $$n:\mathbb{N} \vdash D^{n+1}(S, F) := \tilde{D}^{-(n+1)}(S \to F) := \sum_{f:D^1(S, F)} \Vert\sum_{g:D^{n}(S, F)} \tilde{D}(f) = g\Vert$$ and the type of __pointwise continuously $n$-fold iterated differentiable functions__ between $S$ and $F$ is the $n$-fold [[iterated inverse image]]s of $C^0(S, F)$ under the Newton-Leibniz operator: $$C^0(S, F) := \tilde{D}^{-0}(C^0(S, F)) := C^0(S, F)$$ $$n:\mathbb{N} \vdash C^{n+1}(S, F) := \tilde{D}^{-(n+1)}(C^0(S, F)) := \sum_{f:D^1(S, F)} \Vert\sum_{g:C^{n}(S, F)} \tilde{D}(f) = g\Vert$$ ## See also ## * [[pointwise continuous function]] * [[differentiable function]] * [[smooth function]] * [[iterated inverse image]]