Homotopy Type Theory
smooth function > history (Rev #2)
Contents
Definition
For a calculus field? F F and a subtype S ⊆ F S \subseteq F , the type of smooth functions or infinitely differentiable functions between S S and F F is defined as the maximal subtype C ∞ ( S , F ) ⊆ S → F C^\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 ) ⊆ S → F ) × ( 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 : 𝒰 ( T ⊆ S → F ) × ( T ≅ ∑ f : D 1 ( S , F ) ‖ ∑ g : T D ˜ ( f ) = g ‖ ) → ( T ⊆ C ∞ ( 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.