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

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

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

Contents

< uniformly continuous function

category: redirected to nlab

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:F→Ff:F \to F is uniformly continuous in FF if
isUniformlyContinuous(f)≔∏ ϵ:F +‖∑ δ:F +∏ x:F∏ y:F(|x−y|<δ)→(|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 19:41:28 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (to current)Previous revision (3 more)Current version of pageHide changesHistory (3 revisions)Rollback Source