Homotopy Type Theory antiderivative > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

< antiderivative

Definition

Given a sequentially Cauchy complete Archimedean ordered field \mathbb{R} and a function f:f:\mathbb{R} \to \mathbb{R}, the type of antiderivatives of ff is the fiber of the Newton-Leibniz operator at ff:

antiderivatives(f) g:D 1(,)D˜(g)=fantiderivatives(f) \coloneqq \sum_{g:D^1(\mathbb{R}, \mathbb{R})} \tilde{D}(g) = f

An antiderivative is a term of the above type.

See also

Revision on June 10, 2022 at 15:20:45 by Anonymous?. See the history of this page for a list of all contributions to it.