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

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

# Contents

## Definition

Given~~ an~~ a~~ algebraic~~ sequentially~~ limit~~ Cauchy complete Archimedean ordered field $\mathrm{F\mathbb{R}}$~~ F~~ \mathbb{R}~~ ,~~ and a function~~subtype~~$f:\mathbb{R} \to \mathbb{R}$ , the type of antiderivatives of$\mathrm{Sf}\subseteq F$~~ S~~ f~~ \subseteq~~~~ F~~~~ ,~~ ~~ and~~ is~~ a~~ the~~ function~~~~$f:S \to F$~~~~, the type of antiderivatives of ~~~~$f$~~~~ is the ~~fiber of the Newton-Leibniz operator at $f$:

$$\mathrm{antiderivatives}(f)\u2254\sum _{g:{D}^{1}(\mathrm{S\mathbb{R}},\mathrm{F\mathbb{R}})}\tilde{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 14:32:59 by
Anonymous?.
See the history of this page for a list of all contributions to it.