[[!redirects continuous function]] ## Definition ## ### In real numbers ### Let $\mathbb{R}$ be the [[Dedekind real numbers]] with a term $$p_\mathbb{R}:isContr(\esh(\mathbb{R}))$$ representing that the [[shape]] of $\mathbb{R}$ is [[contractible]] (which derives from [[axiom R-flat]]), 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 mapping $f:I \to \mathbb{R}$, let us define the graph $G$ of the mapping $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(\esh(G))$$ ### Between geometrically contractible spaces ### Let $S$ and $T$ be [[space]]s with terms $$p_S:isContr(\esh(S))$$ $$p_T:isContr(\esh(T))$$ representing that the [[shape]]s of $S$ and $T$ are [[contractible]]. Given a mapping $f:S \to T$, let us define the graph $G$ of the mapping $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(\esh(G))$$ ## See also ## * [[geometrically contractible space]]