Homotopy Type Theory antiderivative > history (Rev #2)

Contents

Definition

Given a calculus field? FF, a subtype SFS \subseteq F, and a function f:SFf:S \to F, the type of antiderivatives of ff is the fiber of the Newton-Leibniz operator at ff:

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

An antiderivative is a term of the above type.

See also

Revision on April 16, 2022 at 15:31:50 by Anonymous?. See the history of this page for a list of all contributions to it.