Homotopy Type Theory directional derivative > history (Rev #2)

Definition
See also

Definition

Given a calculus field? $F$ of scalars, let $V$ be a $F$ -calculus vector space? $V$ , and let $f:V \to F$ be a directionally differentiable function valued in scalars. Given a vector $w:V$ , the directional derivative $\Del_{w}$ is pointwise defined as

\Del_{w}(f)(v) \coloneqq \lim_{(x, y) \to (x, x)} \frac{f(v + x w) - f(v + y w)}{x - y}

Homotopy Type Theory directional derivative > history (Rev #2)

Contents

Definition

See also