Homotopy Type Theory pointwise continuous function > history (Rev #5)

Definition
- In premetric spaces
See also

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 $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

Homotopy Type Theory pointwise continuous function > history (Rev #5)

Contents

Definition

In premetric spaces

See also