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

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

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

Definition

In set homotopy type theory

In Archimedean ordered fields

Let FF be an Archimedean ordered field and let

F +{ a:FaF|0<a F_{+} \coloneqq \{a \sum_{a:F} \in F \vert 0 \lt a

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

isUniformlyContinuous(f) ϵ:F +ϵ δ:F +F + x:F. y:FδF +.xF.yF.(|x δy|<δ)(|f(x) ϵf(y)|<ϵ) isUniformlyContinuous(f) \coloneqq \forall \prod_{\epsilon:F_{+}} \epsilon \Vert \in \sum_{\delta:F_{+}} F_{+}. \prod_{x:F} \exists \prod_{y:F} \delta (\vert \in F_{+}. \forall x \in - F. \forall y \in \vert F. \lt (x \delta) \sim_\delta y) \to (f(x) (\vert \sim_\epsilon f(x) f(y)) - f(y) \vert \lt \epsilon) \Vert

In premetric spaces

In homotopy type theory

Let SS be a premetric space and let

In Archimedean ordered fields

F + a:S0<aF_{+} \coloneqq \sum_{a:S} 0 \lt a

Let be the positive elements in F S F S . be A an functionArchimedean ordered fieldf:SSf:S \to S and letff is uniformly continuous in SS if

F +isUniformlyContinuous(f) a ϵ:F +0< δ: +a x:S y:S(x δy)(f(x) ϵf(y)) F_{+} isUniformlyContinuous(f) \coloneqq \sum_{a:F} \prod_{\epsilon:\mathbb{Q}_{+}} 0 \Vert \lt \sum_{\delta:\mathbb{Q}_{+}} a \prod_{x:S} \prod_{y:S} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert

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

In premetric spaces

Let SS be a premetric space and let

F + a:S0<aF_{+} \coloneqq \sum_{a:S} 0 \lt a

be the positive elements in SS. A function f:SSf:S \to S ff is uniformly continuous in SS if

isUniformlyContinuous(f) ϵ: + δ: + x:S y:S(x δy)(f(x) ϵf(y))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

Revision on May 4, 2022 at 21:04:04 by Anonymous?. See the history of this page for a list of all contributions to it.