#Contents# * table of contents {:toc} ## Definition ## ### In premetric spaces ### Let $T$ and $V$ be types, $S$ be a $T$-[[premetric space]] and $U$ be a $V$-[[premetric space]]. An function $f:S \to U$ is __continuous at a point__ $c:S$ if the [[limit of a function|limit]] of $f$ approaching $c$ exists and is equal to $f(c)$ $$isContinuousAt(f, c) \coloneqq isContr(\lim_{x \to c} f(x) = f(c))$$ $f$ is __pointwise continuous__ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)$$ $f$ is __uniformly continuous__ if $$isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:V} \Vert \sum_{\delta:T} \prod_{x:S} \prod_{y:S} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert$$ ## See also ## * [[premetric space]] * [[limit of a function]]