#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In set theory ### #### In Archimedean ordered fields #### Let $F$ be an [[Archimedean ordered field]] and let $$F_{+} \coloneqq \{a \in F \vert 0 \lt a$$ be the positive elements in $F$. $f$ is __uniformly continuous__ in $F$ if $$isUniformlyContinuous(f) \coloneqq \forall \epsilon \in F_{+}. \exists \delta \in F_{+}. \forall x \in F. \forall y \in F. (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y))$$ #### In premetric spaces #### ### 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$$ ## See also ## * [[Archimedean ordered field]] * [[premetric space]] * [[uniformly differentiable function]] * [[pointwise continuous function]]