Homotopy Type Theory pointwise continuous function > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | ~~Removed~~ | ~~Chan~~ged

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

~~A function~~ $f$ ~~$f$~~ is 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:T} \Vert \sum_{\delta:V} \prod_{x:S} \prod_{y:S} (x \sim_\epsilon y) \to (f(x) \sim_\delta f(y)) \Vert

Homotopy Type Theory pointwise continuous function > history (Rev #4, changes)

Contents

Definition

In premetric spaces

See also