#Contents# * table of contents {:toc} ## Definition ## For a [[calculus field]] $F$ and a subtype $S \subseteq F$, the type of __smooth functions__ or __infinitely differentiable functions__ between $S$ and $F$ is defined as the maximal subtype $C^\infty(S, F) \subseteq S \to F$ such that the [[inverse image]] of $C^\infty(S, F)$ under the [[Newton-Leibniz operator]] is equivalent to $C^\infty(S, F)$ itself. $$p: (C^\infty(S, F) \subseteq S \to F) \times \left(C^\infty(S, F) \cong \sum_{f:D^1(S, F)} \Vert\sum_{g:C^\infty(S, F)} \tilde{D}(f) = g\Vert\right)$$ $$p: \prod_{T:\mathcal{U}} (T \subseteq S \to F) \times \left(T \cong \sum_{f:D^1(S, F)} \Vert\sum_{g:T} \tilde{D}(f) = g\Vert\right) \to (T \subseteq C^\infty(S, F))$$ ## See also ## * [[pointwise continuous function]] * [[differentiable function]] * [[iterated differentiable function]] * [[infinitely iterated inverse image]]