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

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

Contents

Definition

Given an a algebraic sequentially limit Cauchy complete Archimedean ordered field F F \mathbb{R} , and a functionsubtypef:f:\mathbb{R} \to \mathbb{R} , the type of antiderivatives of S fF S f \subseteq F , and is a the functionf: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)=f antiderivatives(f) \coloneqq \sum_{g:D^1(S, \sum_{g:D^1(\mathbb{R}, F)} \mathbb{R})} \tilde{D}(g) = f

An antiderivative is a term of the above type.

See also

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