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

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Definition
- In ~~homotopy~~ Archimedean ~~type~~ ordered ~~theory~~ fieldsIn Archimedean ordered fields
  In premetric spaces
See also

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

Definition

~~In homotopy type theory~~

In Archimedean ordered fields

Let $F$ be an Archimedean ordered field and let

F_{+} \coloneqq \sum_{a:F} 0 \lt a

be the positive elements in $F$ . A function $f:F \to F$ is uniformly continuous in $F$ if

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

~~In premetric spaces~~
~~Let $S$ be a premetric space and let~~
~~$F_{+} \coloneqq \sum_{a:S} 0 \lt a$~~
~~be the positive elements in $S$ . A function $f:S \to S$ $f$ is uniformly continuous in $S$ if~~
~~$isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{\delta:\mathbb{Q}_{+}} \prod_{x:S} \prod_{y:S} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert$~~

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

Contents

Definition

In homotopy type theory

In Archimedean ordered fields

In premetric spaces

See also