Homotopy Type Theory antiderivative > history (Rev #4)

Contents

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 18:32:59 by Anonymous?. See the history of this page for a list of all contributions to it.