#Contents# * table of contents {:toc} Whenever editing is allowed on the [[nLab:HomePage|nLab]] again, this article should be ported over there. ## Definition ## ### In Archimedean ordered fields ### Let $F$ be an [[Archimedean ordered field]]. A function $f:F \to F$ is __continuous at a point__ $c:F$ $$isContinuousAt(f, c) \coloneqq \prod_{\epsilon:(0, \infty)} \prod_{x:F} \left[\sum_{\delta:(0, \infty)} \left[\sum_{a:(-\delta, \delta)} x - c = a\right] \to \left[\sum_{b:(-\epsilon, \epsilon)} f(x) - f(c) = b\right]\right]$$ $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]]