#Contents# * table of contents {:toc} ## Definition ## ### Valued in fields ### Given a [[algebraic limit field]] $F$, a subtype $S \subseteq F$, a [[pointwise continuous function]] $f:C^0(S, F)$ is __differentiable__ if the [[difference quotient]] has a [[limit of a binary function approaching a diagonal|limit approaching the diagonal]] $$isDifferentiable(f) := hasLimitApproachingDiagonal\left(\frac{f(x) - f(y)}{x - y}\right)$$ Let us define the type of differentiable functions $D^1(S, F)$ on $S$ as the type of pointwise continuous functions that are differentiable. $$D^1(S, F) := \sum_{f:C^0(S, F)} isDifferentiable(f)$$ ## See also ## * [[pointwise continuous function]] * [[Newton-Leibniz operator]] * [[iterated differentiable function]] * [[smooth function]] * [[directionally differentiable function]]