#Contents# * table of contents {:toc} ## Definition ## Let $T$ be a function limit space with a tight apartness relation $\#$ and let $S \subseteq T$ be a subtype of $T$. Let us define the subtype $\Delta_{\#}(S) \subseteq S \times S$ of pairs of elements apart from the [[diagonal]] as $$\Delta_{\#}(S) \coloneqq \sum_{(x,y):S \times S} x \# y$$ Given a [[partial function|partial]] binary function $q:\Delta_{\#}(S) \to T$, the currying of $q$ results in the dependent functions $$x:S \vdash q(x): \left(\sum_{y:S} x \# y\right) \to T$$ A function $g:S \to T$ is a __limit of $q$ approaching the diagonal__ if for all $x:S$ the limit of the dependent function $q(x)$ approaching $x$ is $g(x)$. We can define a predicate that the $q$ has a limit approaching the diagonal as $$hasLimitApproachingDiagonal(q) \coloneqq \left[\sum_{g:S \to F} \prod_{x:S} \lim_{y \to x} q(x)(y) = g(x)\right]$$ The type of all functions in $\Delta_{\#}(S) \to F$ that have a limit approaching the diagonal is defined as $$DiagonalLimitFunc(S, T) \coloneqq \sum_{q:\Delta_{\#}(S) \to T} hasLimitApproachingDiagonal(q)$$ As a result, there exists a function $$\lim_{(x, y) \to (x, x)} (-)(x, y): DiagonalLimitFunc(S, T) \to (S \to F)$$ which returns the limit of a partial binary function $q:DiagonalLimitFunc(S, T) \subseteq (\Delta_{\#}(S) \to T)$ approaching the diagonal. ## See also ## * [[limit of a function]] * [[differentiable function]] * [[difference quotient]] * [[Newton-Leibniz operator]]