Homotopy Type Theory smooth function > history (Rev #2)

Contents

Definition

For a calculus field? FF and a subtype SFS \subseteq F, the type of smooth functions or infinitely differentiable functions between SS and FF is defined as the maximal subtype C (S,F)SFC^\infty(S, F) \subseteq S \to F such that the inverse image of C (S,F)C^\infty(S, F) under the Newton-Leibniz operator is equivalent to C (S,F)C^\infty(S, F) itself.

p:(C (S,F)SF)×(C (S,F) f:D 1(S,F) g:C (S,F)D˜(f)=g)p: (C^\infty(S, F) \subseteq S \to F) \times \left(C^\infty(S, F) \cong \sum_{f:D^1(S, F)} \Vert\sum_{g:C^\infty(S, F)} \tilde{D}(f) = g\Vert\right)
p: T:𝒰(TSF)×(T f:D 1(S,F) g:TD˜(f)=g)(TC (S,F))p: \prod_{T:\mathcal{U}} (T \subseteq S \to F) \times \left(T \cong \sum_{f:D^1(S, F)} \Vert\sum_{g:T} \tilde{D}(f) = g\Vert\right) \to (T \subseteq C^\infty(S, F))

See also

Revision on April 23, 2022 at 03:59:12 by Anonymous?. See the history of this page for a list of all contributions to it.