Homotopy Type Theory uniformly continuous function > history (Rev #4, changes)

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

Contents

< uniformly continuous function

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

Definition

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

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