#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$. A function $f \in F^F$ is __continuous at a point__ $c \in F$ if $$isContinuousAt(f, c) \coloneqq \forall \epsilon \in F_{+}. \forall x \in F. \exists \delta \in F_{+}. (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon)$$ $f$ is __pointwise continuous__ in $F$ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \forall c \in F isContinuousAt(f, c)$$ #### In preconvergence spaces #### Let $S$ and $T$ be [[preconvergence space]]s. A function $f \in T^S$ is __continuous at a point__ $c \in S$ if $$isContinuousAt(f, c) \coloneqq \forall I \in DirectedSet_\mathcal{U}. \forall x \in S^I. isLimit_S(x, c) \to isLimit_T(f \circ x, f(c))$$ $f$ is __pointwise continuous__ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \forall c \in S isContinuousAt(f, c)$$ ### 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 __continuous at a point__ $c:F$ $$isContinuousAt(f, c) \coloneqq \prod_{\epsilon:F_{+}} \prod_{x:F} \Vert \sum_{\delta:F_{+}} (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon) \Vert$$ $f$ is __pointwise continuous__ in $F$ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \prod_{c:F} isContinuousAt(f, c)$$ #### In preconvergence spaces #### Let $S$ and $T$ be [[preconvergence space]]s. A function $f:S \to T$ is __continuous at a point__ $c:S$ $$isContinuousAt(f, c) \coloneqq \sum_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit_S(x, c) \to isLimit_T(f \circ x, f(c))$$ $f$ is __pointwise continuous__ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)$$ #### In function limit spaces #### Let $T$ be a [[function limit space]], and let $S \subseteq T$ be a subtype of $T$. A function $f:S \to T$ is __continuous at a point__ $c:S$ if the [[limit of a function|limit of $f$ approaching $c$]] is equal to $f(c)$. $$p:\lim_{x \to c} f(x) = f(c)$$ $f$ is __pointwise continuous__ on $S$ if it is continuous at all points $c:S$: $$p:\prod_{c:S} \lim_{x \to c} f(x) = f(c)$$ The type of all pointwise continuous functions on a subtype $S$ of $T$ is defined as $$C^0(S, T) \coloneqq \sum_{f:S \to T} \prod_{c:S} \lim_{x \to c} f(x) = f(c)$$ ## See also ## * [[Archimedean ordered field]] * [[limit of a function]] * [[differentiable function]] * [[uniformly continuous function]]