Contents

Definition

Given a Heyting field $F$ and a subtype $S \subseteq F$, let us define the subtype $\Delta_{\#}(S) \subseteq S \times S$ of pairs of elements apart from the diagonal as

Given a function $f:S \to F$, the difference quotient $q:\Delta_{\#}(S) \to F$ is the partial binary function

See also

• differential function?

• Newton-Leibniz operator