Homotopy Type Theory pointwise continuous function > history (Rev #20, changes)

Showing changes from revision #19 to #20: Added | Removed | Changed

Contents

Definition

In Archimedean ordered fields

Let FF be an Archimedean ordered field and let

Let FF be an Archimedean ordered field and let

F + a:F0<aF_{+} \coloneqq \sum_{a:F} 0 \lt a
F + a:F0<aF_{+} \coloneqq \sum_{a:F} 0 \lt a

be the positive elements in FF. A function f:FFf:F \to F is pointwise continuous in FF if

be the positive elements in FF. A function f:FFf:F \to F is pointwise continuous in FF if

isPointwiseContinuous(f) x:F ϵ:F + y:F δ:F +(|xy|<δ)(|f(x)f(y)|<ϵ)isPointwiseContinuous(f) \coloneqq \prod_{x:F} \prod_{\epsilon:F_{+}} \prod_{y:F} \Vert \sum_{\delta:F_{+}} (\vert x - y \vert \lt \delta) \to (\vert f(x) - f(y) \vert \lt \epsilon) \Vert
isPointwiseContinuous(f) x:F ϵ:F + y:F δ:F +(|xy|<δ)(|f(x)f(y)|<ϵ)isPointwiseContinuous(f) \coloneqq \prod_{x:F} \prod_{\epsilon:F_{+}} \prod_{y:F} \Vert \sum_{\delta:F_{+}} (\vert x - y \vert \lt \delta) \to (\vert f(x) - f(y) \vert \lt \epsilon) \Vert

See also

Revision on June 10, 2022 at 14:15:22 by Anonymous?. See the history of this page for a list of all contributions to it.