Homotopy Type Theory uniformly continuous function > history (changes)

Showing changes from revision #3 to #4: Added | Removed | Changed


< uniformly continuous function

Whenever editing is allowed on the nLab again, this article should be ported over there.


In Archimedean ordered fields

Let FF be an Archimedean ordered field and let

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 uniformly continuous in FF if

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

See also

Last revised on June 10, 2022 at 19:41:28. See the history of this page for a list of all contributions to it.