[[!redirects pointwise continuous function]] [[!redirects uniformly continuous function]] #Contents# * table of contents {:toc} ## Definition in cohesive homotopy type theory ## ### In real numbers ### Let $\mathbb{R}$ be the (two-sided) [[Dedekind real numbers]] with a term $$p_\mathbb{R}:isContr(\Pi(\mathbb{R}))$$ representing that the [[shape]] of $\mathbb{R}$ is [[contractible]]. and let $I$ be a [[closed interval]] or [[open interval]] in $\mathbb{R}$. Because the shape of $\mathbb{R}$ is contractible, the shape of any closed or open interval in $\mathbb{R}$ is contractible. Given a function $f:I \to \mathbb{R}$, let us define the graph $G$ of the function $f$ as $$G \coloneqq \sum_{x:I} (x, f(x))$$ in the product type $I \times \mathbb{R}$. $f$ is __continuous__ if the shape of $G$ is contractible: $$p:isContr(\Pi(G))$$ ### Between geometrically contractible types ### Let $S$ and $T$ be types with terms $$p_S:isContr(\Pi(S))$$ $$p_T:isContr(\Pi(T))$$ representing that the [[shape]]s of $S$ and $T$ are [[contractible]]. Given a function $f:S \to T$, let us define the graph $G$ of the function $f$ as $$G \coloneqq \sum_{x:S} (x, f(x))$$ in the product type $I \times \mathbb{R}$. $f$ is __continuous__ if the shape of $G$ is contractible: $$p:isContr(\Pi(G))$$ ## Definition in homotopy type theory ## ### In rational numbers ### Let $\mathbb{Q}$ be the [[rational numbers]]. An function $f:\mathbb{Q} \to \mathbb{Q}$ is __continuous at a point__ $c:\mathbb{Q}$ $$isContinuousAt(f, c) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \prod_{x:\mathbb{Q}} \Vert \sum_{\delta:\mathbb{Q}_{+}} (\vert x - c \vert \lt \delta) \to (\vert f(x) - f(c) \vert \lt \epsilon) \Vert$$ $f$ is __pointwise continuous__ in $\mathbb{Q}$ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \prod_{c:\mathbb{Q}} isContinuousAt(f, c)$$ $f$ is __uniformly continuous__ in $\mathbb{Q}$ if $$isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{\delta:\mathbb{Q}_{+}} \prod_{x:\mathbb{Q}} \prod_{y:\mathbb{Q}} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert$$ ### In Archimedean ordered fields ### Let $F$ be an [[Archimedean ordered field]]. An 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)$$ $f$ is __uniformly continuous__ in $F$ if $$isUniformlyContinuous(f) \coloneqq \prod_{\epsilon:F_{+}} \Vert \sum_{\delta:F_{+}} \prod_{x:F} \prod_{y:F} (x \sim_\delta y) \to (f(x) \sim_\epsilon f(y)) \Vert$$ ### Most general definition ### Let $S$ be a type with a [[predicate]] $\to_S$ between the type of all nets in $S$ $$\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)$$ and $S$ itself, and let $T$ be a type with a [[predicate]] $\to_T$ between the type of all nets in $T$ $$\sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)$$ and $T$ itself. 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} (x \to_S c) \to (f \circ x \to_T f(c))$$ $f$ is __pointwise continuous__ if it is continuous at all points $c$: $$isPointwiseContinuous(f) \coloneqq \prod_{c:S} isContinuousAt(f, c)$$ ## See also ## * [[Archimedean ordered field]] * [[limit of a function]]