Homotopy Type Theory antiderivative > history (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

Last revised on June 10, 2022 at 19:20:45. See the history of this page for a list of all contributions to it.