that for all $d^{\prime}\in D$, $h\circ
d^{\prime(i^{\prime},\mathrm{ar}(h))}\in
G\cap\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})$. We must show that $h\in G$,
i.e. for all $1\leq i\leq\mathrm{ar}(h)$ we have to demonstrate that $h\circ
d^{(i,\mathrm{ar}(h))}\in\mathcal{J}(F\cup\mathbb{C}_{\mathbb{F}(X,Y)})$.

Hereto, let $1\leq i\leq\mathrm{ar}(h)$. In case $i=i^{\prime}$, we obtain
from our assumption that $h\circ
d^{(i,\mathrm{ar}(h))}\in\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})$ and hence,
by the monotonicity of $\mathcal{J}$, that $h\circ
d^{(i,\mathrm{ar}(h))}\in\mathcal{J}(F\cup\mathbb{C}_{\mathbb{F}(X,Y)})$. If
$i\not=i^{\prime}$, then we have that for all $d^{\prime}\in D$,
$d^{\prime(i^{\prime},\mathrm{ar}(h))}\circ
d^{(i,\mathrm{ar}(h))}=d^{(i,\mathrm{ar}(h))}\circ
d^{\prime(i^{\prime},\mathrm{ar}(h))}$. Therefore, since by our assumption,
$h\circ d^{\prime(i^{\prime},\mathrm{ar}(h))}\in G$, for all $d^{\prime}\in
D$, we have that for all $d^{\prime}\in D$, $h\circ
d^{(i,\mathrm{ar}(h))}\circ
d^{\prime(i^{\prime},\mathrm{ar}(h))}\in\mathcal{J}(F\cup\mathbb{C}_{\mathbb{F}(X,Y)})$.
As $\mathcal{J}(F\cup\mathbb{C}_{\mathbb{F}(X,Y)})$ is closed under Rule (R),
it follows that $h\circ
d^{(i,\mathrm{ar}(h))}\in\mathcal{J}(F\cup\mathbb{C}_{\mathbb{F}(X,Y)})$∎

######  Proposition 10.2.

Let $(X,D)$, $(Y,E)$ and $(Z,C)$ be extended IFS. If
$f\in\mathbb{C}_{\mathbb{F}(Y,Z)}$ and
$g_{\kappa}\in\mathbb{C}_{\mathbb{F}(X,Y)}$, for
$1\leq\kappa\leq\mathrm{ar}(f)$, then $f\circ(g_{1}\times\cdots\times
g_{\mathrm{ar}(f)})\in\mathbb{C}_{\mathbb{F}(X,Z)}$.

###### Proof.

The proof is a modification of the proof of [6, Proposition 4.2]. It proceeds
by co-induction. Set

$F:=\mbox{$\\{\,f\circ(g_{1}\times\cdots\times g_{\mathrm{ar}(f)})\mid
f\in\mathbb{C}_{\mathbb{F}(Y,Z)}\wedge
g_{1},\ldots,g_{\mathrm{ar}(f)}\in\mathbb{C}_{\mathbb{F}(X,Y)}\,\\}$}.$

Then we show that $F\subseteq\mathcal{J}^{X,Z}(F)$, that is, we show
$\mathbb{C}_{\mathbb{F}(Y,Z)}\subseteq G$, where

$G:=\mbox{$\\{\,f\in\mathbb{F}(Y,Z)\mid(\forall
g_{1},\ldots,g_{\mathrm{ar}(f)}\in\mathbb{C}_{\mathbb{F}(X,Y)})\,f\circ(g_{1}\times\cdots\times
g_{\mathrm{ar}(f)})\in\mathcal{J}^{X,Z}(F)\,\\}$}.$

Since
$\mathbb{C}_{\mathbb{F}(Y,Z)}=\mathcal{J}^{Y,Z}(\mathbb{C}_{\mathbb{F}(Y,Z)})$
it suffices to show $\mathcal{J}^{Y,Z}(\mathbb{C}_{\mathbb{F}(Y,Z)})\subseteq
G$. Hence, by the inductive definition of
$\mathcal{J}^{Y,Z}(\mathbb{C}_{\mathbb{F}(Y,Z)})$, it is sufficient to
demonstrate that $\Phi^{Y,Z}(\mathbb{C}_{\mathbb{F}(Y,Z)})(G)\subseteq G$,
that is we have to show that Rules (W) and (R) hold.

(W) Assume that $c\in C$ and
$f_{1},\ldots,f_{\mathrm{ar}(c)}\in\mathbb{C}_{\mathbb{F}(Y,Z)}$. We need to
show that $c\circ(f_{1}\times\cdots\times f_{\mathrm{ar}(c)})\in G$. For
$1\leq\kappa\leq\mathrm{ar}(c)$ assume that
$g^{(\kappa)}_{1},\ldots,g^{(\kappa)}_{\mathrm{ar}(f_{\kappa})}\in\mathbb{C}_{\mathbb{F}(X,Y)}$.
Then we must prove that $c\circ(f_{1}\times\cdots\times
f_{\mathrm{ar}(c)})\circ(g^{(1)}_{1}\times\cdots\times
g^{(\mathrm{ar}(c))}_{\mathrm{ar}(f_{\mathrm{ar}(c)})})\in\mathcal{J}^{X,Z}(F)$.
Because $\mathcal{J}^{X,Z}(F)$ is closed under Rule (W), it suffices to
demonstrate that for each $1\leq\kappa\leq\mathrm{ar}(c)$,
$f_{\kappa}\circ(g^{(\kappa)}_{1}\times\cdots\times
g^{(\kappa)}_{\mathrm{ar}(f_{\kappa})})\in F$, which holds by the definition
of $F$.

(R) Let $f\in\mathbb{F}^{(n)}(Y,Z)$ and $1\leq i\leq n$. Suppose, as induction
hypothesis, that for all $e\in E$, $f\circ e^{(i,n)}\in G$. We have to show
that $f\in G$, i.e. $\mathbb{C}_{\mathbb{F}(X,Y)}\subseteq H^{(i)}$, where

$H^{(i)}:=\mbox{$\\{\,g\in\mathbb{F}(X,Y)\mid(\forall
g_{1},\ldots,g_{n}\in\mathbb{C}_{\mathbb{F}(X,Y)})[g_{i}=g\rightarrow
f\circ(g_{1}\times\cdots\times g_{n})\in\mathcal{J}^{X,Z}(F)]\,\\}$}.$

Since
$\mathbb{C}_{\mathbb{F}(X,Y)}=\mathcal{J}^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})$,
it suffices to show that
$\mathcal{J}^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})\subseteq H^{(i)}$, which we
do by side induction, that is, we show that

$\Phi^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})(H^{(i)})\subseteq H^{(i)}.$

($\text{W}_{\text{side}}$) Let $e\in E$ and
$g_{1},\ldots,g_{n},g^{\prime}_{1},\ldots,g^{\prime}_{\mathrm{ar}(e)}\in\mathbb{C}_{\mathbb{F}(X,Y)}$
so that $g_{i}=e\circ(g^{\prime}_{1}\times\cdots\times
g^{\prime}_{\mathrm{ar}(e)})$. Then

$\displaystyle f\circ(g_{1}\times\cdots\times g_{n})$
$\displaystyle=f\circ(g_{1}\times\cdots\times
g_{i-1}\times(e\circ(g^{\prime}_{1}\times\cdots\times
g^{\prime}_{\mathrm{ar}(e)}))\times g_{i+1}\times\cdots\times g_{n})$
$\displaystyle=f\circ(e^{(i,n)}\circ(g_{1}\times\cdots\times g_{i-1}\times
g^{\prime}_{1}\times\cdots\times g^{\prime}_{\mathrm{ar}(e)}\times
g_{i+1}\times\cdots\times g_{n}))$ $\displaystyle=(f\circ
e^{(i,n)})\circ(g_{1}\times\cdots\times g_{i-1}\times
g^{\prime}_{1}\times\cdots\times g^{\prime}_{\mathrm{ar}(e)}\times
g_{i+1}\times\cdots\times g_{n}).$

By the main induction hypothesis, $f\circ e^{(i,n)}\in G$ and hence

$(f\circ e^{(i,n)})\circ(g_{1}\times\cdots\times g_{i-1}\times
g^{\prime}_{1}\times\cdots\times g^{\prime}_{\mathrm{ar}(e)}\times
g_{i+1}\times\cdots\times g_{n})\in\mathcal{J}^{X,Z}(F).$

Therefore, $e\circ(g^{\prime}_{1}\times\cdots\times
g^{\prime}_{\mathrm{ar}(e)})\in H^{(i)}$.

($\text{R}_{\text{side}}$) Let $g\in\mathbb{C}_{\mathbb{F}(X,Y)}$ and $1\leq
j\leq\mathrm{ar}(g)$. Suppose that for all $d\in D$, $g\circ
d^{(j,\mathrm{ar}(g))}\in H^{(i)}$. We have to show that $g\in H^{(i)}$.
Assume to this end that $h_{1},\ldots,h_{n}\in\mathbb{C}_{\mathbb{F}(X,Y)}$
with $h_{i}=g$. We must derive that $f\circ(h_{1}\times\cdots\times
h_{n})\in\mathcal{J}^{X,Z}(F)$. Let
$m:=\sum_{\kappa=1}^{n}\mathrm{ar}(h_{\kappa})$ and
$\hat{\jmath}:=j+\sum_{\kappa=1}^{i-1}\mathrm{ar}(h_{\kappa})$. Because
$\mathcal{J}^{X,Z}(F)$ is closed under Rule (R), it suffices to show that for
all $d\in D$, $(f\circ(h_{1}\times\cdots\times h_{n}))\circ
d^{(\hat{\jmath},m)}\in\mathcal{J}^{X,Z}(F)$, which is the case as the $i$-th
element of $(h_{1}\times\cdots\times h_{n})\circ d^{(\hat{\jmath},m)}$ is
$g\circ d^{(j,\mathrm{ar}(g))}$ and $g\circ
d^{(j,\mathrm{ar}(g))}\in\mathbb{C}_{\mathbb{F}(X,Y)}$ by Lemma 10.1. ∎

######  Lemma 10.3.

Let $(X,D)$ be an extended IFS. Then the following statements hold:

  1. 1.

Let $\mathop{\mathstrut\rm id}\nolimits_{X}\colon X\rightarrow X$ be the
identity on $X$. Then $\mathop{\mathstrut\rm
id}\nolimits_{X}\in\mathbb{C}_{\mathbb{F}(X,X)}$.

  2. 2.

For any $n\in\mathbb{N}_{0}$ and $1\leq i\leq n$, let $\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i}\colon X^{n}\rightarrow X$ be the projection onto the
$i$-th component. Then $\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i}\in\mathbb{C}^{(n)}_{\mathbb{F}(X,X)}$.

  3. 3.

For $n>0$, let $\mathop{\mathstrut\rm diag}\nolimits_{X}^{(n)}\colon
X\rightarrow X^{n}$ be given by $\mathop{\mathstrut\rm
diag}\nolimits^{(n)}(x):=x^{(n)}$. Then $\mathop{\mathstrut\rm
diag}\nolimits_{X}^{(n)}\in\mathbb{C}_{\mathbb{F}(X,X^{n})}$.

###### Proof.

For all statements the proof proceeds by co-induction.

(1) We show that $\\{\mathop{\mathstrut\rm
id}\nolimits_{X}\\}\subseteq\mathcal{J}(\\{\mathop{\mathstrut\rm
id}\nolimits_{X}\\})$. Because of Rule (R) it suffices to show that for all
$d\in D$, $\mathop{\mathstrut\rm
id}\nolimits_{X}\circ\,d\in\mathcal{J}(\\{\mathop{\mathstrut\rm
id}\nolimits_{X}\\})$. By Rule (W) we have that for $d\in D$,
$d\circ(\mathop{\mathstrut\rm
id}\nolimits_{X}\times\cdots\times\mathop{\mathstrut\rm
id}\nolimits_{X})\in\mathcal{J}(\\{\mathop{\mathstrut\rm
id}\nolimits_{X}\\})$. Since $d\circ(\mathop{\mathstrut\rm
id}\nolimits_{X}\times\cdots\times\mathop{\mathstrut\rm
id}\nolimits_{X})={\mathop{\mathstrut\rm id}\nolimits_{X}}\circ d$, we are
done.

(2) Since for $d\in D$,

$d\circ(\mathop{\mathstrut\rm
pr}\nolimits^{(n+\mathrm{ar}(d))}_{i}\times\cdots\times\mathop{\mathstrut\rm
pr}\nolimits^{(n+\mathrm{ar}(d))}_{i+\mathrm{ar}(d)-1})={\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i}}\circ d^{(i,n)},$

it follows in the same way that

$\mbox{$\\{\,\mathop{\mathstrut\rm pr}\nolimits^{(m)}_{j}\mid m>0\wedge 1\leq
j\leq m\,\\}$}\subseteq\mathcal{J}(\mbox{$\\{\,\mathop{\mathstrut\rm
pr}\nolimits^{(m)}_{j}\mid m>0\wedge 1\leq j\leq m\,\\}$}).$

(3) Let $d\in D$ and note that for $x_{1},\ldots,x_{\mathrm{ar}(d)}\in X$,

$\displaystyle(\langle d,\ldots,d\rangle\circ(\mathop{\mathstrut\rm
diag}\nolimits^{(n)}_{X}\times\cdots\times\mathop{\mathstrut\rm
diag}\nolimits^{(n)}_{X}))(x_{1},\ldots,x_{\mathrm{ar}(d)})$
$\displaystyle=\langle
d,\ldots,d\rangle(x_{1}^{(n)},\ldots,x_{\mathrm{ar}(d)}^{(n)})$
$\displaystyle=(d(x_{1},\ldots,x_{\mathrm{ar}(d)}),\ldots,d(x_{1},\ldots,x_{\mathrm{ar}(d)}))$
$\displaystyle=({\mathop{\mathstrut\rm diag}\nolimits^{(n)}_{X}}\circ
d)(x_{1},\ldots,x_{\mathrm{ar}(d)}).$

Thus, $\langle d,\ldots,d\rangle\circ(\mathop{\mathstrut\rm
diag}\nolimits^{(n)}_{X}\times\cdots\times\mathop{\mathstrut\rm
diag}\nolimits^{(n)}_{X})={\mathop{\mathstrut\rm
diag}\nolimits^{(n)}_{X}}\circ d$, from which the statement follows as in case
(1). ∎

In the above case of the $n$-th power of a given space $X$, the projections
were treated as $n$-ary maps. Let us now consider the general case of the
product of spaces. Let to this end $(X_{1},D_{1}),\ldots,(X_{n},D_{n})$ be
extended IFS, and let $\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i}\colon\bigtimes_{j=1}^{n}X_{j}\rightarrow X_{i}$ again
denote the projection onto the $i$-th component. Then we have for $\langle
d_{1},\ldots,d_{n}\rangle\in D^{\times}$ that

$\mathop{\mathstrut\rm pr}\nolimits^{(n)}_{i}\circ\,\,\langle
d_{1},\ldots,d_{n}\rangle=d_{i}\circ(\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i}\times\cdots\times\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i})\quad\text{($s_{D}$-times)},$

which leads to the next result.

######  Lemma 10.4.

Let $(X_{1},D_{1}),\ldots,(X_{n},D_{n})$ be extended IFS. Then
$\mathop{\mathstrut\rm
pr}\nolimits^{(n)}_{i}\in\mathbb{C}^{(1)}_{\mathbb{F}(\bigtimes_{j=1}^{n}X_{j},X_{i})}$,
for $1\leq i\leq n$.

######  Proposition 10.5.

Let $(X,D)$ and $(Y,E)$ be extended IFS. Moreover, for $m\in\mathbb{N}$, let

$\mathop{\mathstrut\rm ev}\colon\mathbb{F}^{(m)}(X,Y)\times X^{m}\rightarrow
Y$

with $\mathop{\mathstrut\rm ev}(f,x):=f(x)$ be the _evaluation map_. Then

$\mathop{\mathstrut\rm
ev}[\mathbb{C}^{(m)}_{\mathbb{F}(X,Y)}\times\mathbb{C}_{X}^{m}]\subseteq\mathbb{C}_{Y}.$

###### Proof.

The statement is derived by co-induction. Let the operator
$\Psi\colon\mathcal{P}(Y)\rightarrow\mathcal{P}(Y)$ be defined by

$\Psi(L):=\\{\,y\mid(\exists e\in E)(\exists
y_{1},\ldots,y_{\mathrm{ar}(e)}\in
L)\,y=e(y_{1},\ldots,y_{\mathrm{ar}(e)})\,\\}.$

Then $\mathbb{C}_{Y}=\nu\Psi$. Set

$Z:=\mbox{$\\{\,y\in Y\mid(\exists f\in\mathbb{C}_{\mathbb{F}(X,Y)})(\exists
x_{1},\ldots
x_{\mathrm{ar}(f)}\in\mathbb{C}_{X})\,y=f(x_{1},\ldots,x_{\mathrm{ar}(f)})\,\\}$}.$

We need to show that $Z\subseteq\Psi(Z)$. Let to this end

$G:=\\{\,f\in\mathbb{F}(X,Y)\mid
f[\mathbb{C}^{\mathrm{ar}(f)}_{X}]\subseteq\Psi(Z)\,\\}.$

Then we have to verify that $\mathbb{C}_{\mathbb{F}(X,Y)}\subseteq G$. Since
$\mathbb{C}_{\mathbb{F}(X,Y)}=\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})$, it
is equivalent to prove that
$\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})\subseteq G$. By the inductive
definition of $\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})$ it suffices in
addition to derive that $\Phi(\mathbb{C}_{\mathbb{F}(X,Y)})(G)\subseteq G$,
that is we need to show that

  * (W)

If $e\in E$ and
$(f_{1},\ldots,f_{\mathrm{ar}(e)})\in\mathbb{C}_{\mathbb{F}(X,Y)}$, then
$e\circ(f_{1}\times\cdots\times f_{\mathrm{ar}(e)})\in G$.

  * (R)

If $f\in\mathbb{F}^{(m)}(X,Y)$ and $1\leq i\leq\mathrm{ar}(f)$ so that $f\circ
d^{(i,m)}\in G$, for all $d\in D$, then $f\in G$.

(W) Let $e\in E$,
$f_{1},\ldots,f_{\mathrm{ar}(e)}\in\mathbb{C}_{\mathbb{F}(X,Y)}$, and
$\vec{x}_{\kappa}\in\mathbb{C}^{\mathrm{ar}(f_{\kappa})}_{X}$, for
$1\leq\kappa\leq\mathrm{ar}(e)$. Then $f_{\kappa}(\vec{x}_{\kappa})\in Z$.
Hence,
$e(f_{1}(\vec{x}_{1}),\ldots,f_{\mathrm{ar}(e)}(\vec{x}_{\mathrm{ar}(e)}))\in\Psi(Z)$.

(R) Let $f\in\mathbb{F}^{(m)}(X,Y)$ and $1\leq i\leq m$ with $f\circ
d^{(i,m)}\in G$, for all $d\in D$. Let $x_{1}$, …, $x_{m}\in\mathbb{C}_{X}$.
Then there is some $d_{i}\in D$ and some
$\vec{x}^{\prime}_{i}\in\mathbb{C}^{\mathrm{ar}(d_{i})}_{X}$ so that
$x_{i}=d_{i}(\vec{x}^{\prime}_{i})$. It follows that

$\displaystyle f(x_{1},\ldots,x_{m})$
$\displaystyle=f(x_{1},\ldots,x_{i-1},d_{i}(\vec{x}^{\prime}_{i}),x_{i+1},\ldots,x_{m})$
$\displaystyle=(f\circ
d^{(i,m)})(x_{1},\ldots,x_{i-1},\vec{x}^{\prime}_{i},x_{i+1},\ldots,x_{m})\in\Psi(Z).\qed$

For $n\in\mathbb{N}_{0}$, let the set $\underline{n}:=\\{0,\ldots,n-1\\}$ be
endowed with the discrete topology. Moreover, for $i\in\underline{n}$, let
$g_{i}\colon\underline{n}\rightarrow\underline{n}$ map $\underline{n}$
constantly onto $i$. Then $(\underline{n},\\{g_{1},\ldots,g_{n-1}\\})$ is a
covering IFS with $\underline{n}=\mathbb{C}_{\underline{n}}$.

######  Corollary 10.6.

Let $(X,D)$ be an IFS. Then
$\mathbb{C}^{(1)}_{\mathbb{F}(\underline{n},X)}=\mathbb{C}^{n}_{X}$.

###### Proof.

As a consequence of the preceding proposition we have that
$\mathbb{C}^{(1)}_{\mathbb{F}(\underline{n},X)}\subseteq\mathbb{C}^{n}_{X}$.
The converse inclusion follows by co-induction. We show that
$\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X})\subseteq\mathcal{J}(\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X}))$.

Let $f\in\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X})$ and
$i\in\underline{n}$. Then there are $d_{i}\in D$ and $x_{i}\in\mathbb{C}_{X}$
so that $f(i)=d_{i}(x_{i})$. Set $h_{i}(a)=x_{i}$, for $a\in\underline{n}$.
Then $h_{i}\in\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X})$. Moreover,
$f\circ g_{i}=d_{i}\circ h_{i}$. As
$\mathcal{J}(\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X}))$ is closed under
Rule (W), we obtain that $d_{i}\circ
h_{i}\in\mathcal{J}(\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X}))$. Hence,
$f\circ g_{i}\in\mathcal{J}(\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X}))$,
for all $i\in\underline{n}$. With Rule (R) we therefore obtain that
$f\in\mathcal{J}(\mathbb{F}^{(1)}(\underline{n},\mathbb{C}_{X}))$. ∎

Observe the difference between $\mathbb{C}_{X^{n}}$ and $\mathbb{C}^{n}_{X}$.
In the first case the digits operate on all components simultaneously, whereas
in the other case they do this in an uncoordinated way and approximate the
single components just as needed.

######  Proposition 10.7.

Let $(X,D),(Y_{1},E_{1})$, and $(Y_{2},E_{2})$ be extended IFS. Then for
$f\in\mathbb{C}_{\mathbb{F}(X,Y_{1})}$ and
$g\in\mathbb{C}_{\mathbb{F}(X,Y_{2})}$, $f\times
g\in\mathbb{C}_{\mathbb{F}(X,Y_{1}\times Y_{2})}$.

###### Proof.

Without loss of generality we assume that all maps in $E_{1}\cup E_{2}$ have
the same arity, say $m$. The proof of the statement proceeds by co-induction.
Let

$F:=\mbox{$\\{\,f\times g\mid f\in\mathbb{C}_{\mathbb{F}(X,Y_{1})}\wedge
g\in\mathbb{C}_{\mathbb{F}(X,Y_{2})}\,\\}$}.$

Then we must show that $F\subseteq\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)$. Set

$A:=\mbox{$\\{\,f\in\mathbb{F}(X,Y_{1})\mid(\forall
g\in\mathbb{C}_{\mathbb{F}(X,Y_{2})})\,f\times g\in\mathcal{J}^{X,Y_{1}\times
Y_{2}}(F)\,\\}$}.$

We show that $\mathbb{C}_{\mathbb{F}(X,Y_{1})}\subseteq A$. Since
$\mathbb{C}_{\mathbb{F}(X,Y_{1})}=\mathcal{J}^{X,Y_{1}}(\mathbb{C}_{\mathbb{F}(X,Y_{1})})$,
it suffices to prove that
$\mathcal{J}^{X,Y_{1}}(\mathbb{C}_{\mathbb{F}(X,Y_{1})})\subseteq A$. By
induction we show that
$\Phi^{X,Y_{1}}(\mathbb{C}_{\mathbb{F}(X,Y_{1})})(A)\subseteq A$, which means
that we have to verify Rules (W) and (R).

($\text{W}_{\text{main}}$) Let $e_{1}\in E_{1}$ and
$f_{1},\ldots,f_{m}\in\mathbb{C}_{\mathbb{F}(X,Y_{1})}$. We need to
demonstrate that $e_{1}\circ(f_{1}\times\cdots\times f_{m})\in A$. To this end
we have to show that for all $g\in\mathbb{C}_{\mathbb{F}(X,Y_{2})}$,
$(e_{1}\circ(f_{1}\times\cdots\times f_{m}))\times
g\in\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)$. Let

$B(h):=\mbox{$\\{\,g\in\mathbb{F}(X,Y_{2})\mid h\times
g\in\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)\,\\}$}.$

For $h:=e_{1}\circ(f_{1}\times\cdots\times f_{m})$ we prove that
$\mathbb{C}_{\mathbb{F}(X,Y_{2})}\subseteq B(h)$, for which it suffices to
demonstrate that

$\Phi^{X,Y_{2}}(\mathbb{C}_{\mathbb{F}(X,Y_{2})})(B(h))\subseteq B(h),$ (10)

which is done by side induction.

($\text{W}_{\text{side}}$) Let $e_{2}\in E_{2}$ and
$g_{1},\ldots,g_{m}\in\mathbb{C}_{\mathbb{F}(X,Y_{2})}$. We need to show that

$(e_{1}\circ(f_{1}\times\cdots\times
f_{m}))\times(e_{2}\circ(g_{1}\times\cdots\times
g_{m}))\in\mathcal{J}^{X_{1}\times X_{2},Y_{1}\times Y_{2}}(F).$

We have that

$(e_{1}\circ(f_{1}\times\cdots\times
f_{m}))\times(e_{2}\circ(g_{1}\times\cdots\times g_{m}))=\langle
e_{1},e_{2}\rangle\circ((f_{1}\times g_{1})\times\cdots\times(f_{m}\times
g_{m})),$

where $\langle e_{1},e_{2}\rangle\in E^{\times}$ and $f_{1}\times
g_{1},\ldots,f_{m}\times g_{m}\in F$. Hence,
$(e_{1}\circ(f_{1}\times\cdots\times
f_{m}))\times(e_{2}\circ(g_{1}\times\cdots\times
g_{m}))\in\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)$, by Rule (W).

($\text{R}_{\text{side}}$) Let $g\in\mathbb{F}(X,Y_{2})$ and $1\leq
i\leq\mathrm{ar}(g)$ so that $g\circ d^{(i,\mathrm{ar}(g))}\in B(h)$, for all
$d\in D$. Then $h\times(g\circ
d^{(i,\mathrm{ar}(g))})\in\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)$. Let
$\tilde{h}:=h\times g$. Then
$\mathrm{ar}(\tilde{h})=\mathrm{ar}(h)+\mathrm{ar}(g)$. For
$j:=\mathrm{ar}(h)+i$ we therefore have that $\tilde{h}\circ
d^{(j,\mathrm{ar}(h)+\mathrm{ar}(g))}=h\times(g\circ d^{(i,\mathrm{ar}(g))})$.
It follows that $\tilde{h}\circ
d^{(j,\mathrm{ar}(h)+\mathrm{ar}(g))}\in\mathcal{J}^{X,Y_{1}\times Y_{2}}$,
for all $d\in D$, from which we obtain by Rule (R) that
$\tilde{h}\in\mathcal{J}^{X,Y_{1}\times Y_{2}}$. Hence, $g\in B(h)$. This
proves (10).

($\text{R}_{\text{main}}$) It remains to verify Rule (R) in the main
induction. Let $f\in A$ and $1\leq i\leq\mathrm{ar}(f)$ such that for all
$d\in D$, $f\circ d^{(i,\mathrm{ar}(f))}\in A$. Thus, $(f\circ
d^{(i,\mathrm{ar}(f))})\times g\in\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)$, for
all $d\in D$ and $g\in\mathbb{C}_{\mathbb{F}(X,Y_{2})}$. Set
$\bar{h}_{g}:=f\times g$. Then
$\mathrm{ar}(\bar{h}_{g})=\mathrm{ar}(f)+\mathrm{ar}(g)$ and for all $d\in D$,

$\bar{h}_{g}\circ d^{(i,\mathrm{ar}(f)+\mathrm{ar}(g))}=(f\circ
d^{(i,\mathrm{ar}(f))})\times g.$

Since $(f\circ d^{(i,\mathrm{ar}(f))})\times g\in\mathcal{J}^{X,Y_{1}\times
Y_{2}}(F)$ by our assumption, we obtain with Rule (R) that
$\bar{h}_{g}\in\mathcal{J}^{X,Y_{1}\times Y_{2}}(F)$. Thus, $f\in A$. ∎

Let $\mathbf{eIFS}$ be the category with extended IFS $(X,D)$ as objects, and
for two objects $(X_{1},D_{1})$ and $(X_{2},D_{2})$,
$\mathbb{C}_{\mathbb{F}(X_{1},X_{2})}$ as set of morphisms from
$(X_{1},D_{1})$ to $(X_{2},D_{2})$. Then it follows that
$\prod_{i=1}^{2}(X_{i},D_{i}):=(X_{1}\times X_{2},D^{\times})$ with canonical
projection $\mathop{\mathstrut\rm pr}\nolimits^{(2)}_{i}$, for $i=1,2$, is the
categorical product of $(X_{1},D_{1})$ and $(X_{2},D_{2})$.

Let $(Y_{1},D_{1})$ and $(Y_{2},D_{2})$ be further objects in $\mathbf{eIFS}$
and $f_{i}\in\mathbb{C}_{\mathbb{F}(X_{i},Y_{i})}$, for $i=1,2$. Set
$h_{i}:=f_{i}\circ(\mathop{\mathstrut\rm
pr}\nolimits^{(2)}_{i}\times\cdots\times\mathop{\mathstrut\rm
pr}\nolimits^{(2)}_{i})\,\,\text{($\mathrm{ar}(f_{i})$-times)}$. Then
$h_{i}\in\mathbb{C}_{\mathbb{F}(X_{1}\times X_{2},Y_{i})}$. Hence,
$h_{1}\times h_{2}\in\mathbb{C}_{\mathbb{F}(X_{1}\times X_{2},Y_{1}\times
Y_{2})}$. Define the action of $\prod$ on $f_{1},f_{2}$ by
$\prod(f_{1},f_{2}):=h_{1}\times h_{2}$. Then
$\prod\colon\mathbf{eIFS}\times\mathbf{eIFS}\rightarrow\mathbf{eIFS}$ is a
functor, showing that the product construction presented in Section 8 is
functorial.

As we have already seen, in the framework of computable digit spaces
computability is the appropriate requirement for a map between such spaces to
be considered uniformly continuous, constructively. We will now show that the
above co-inductive-inductively defined function class captures exactly these
functions. Let

$\mathop{\mathstrut\cal
C}\nolimits(X,Y):=\\{\,f\in\mathbb{F}(X,Y)\mid\text{$f$ computable}\,\\}.$

######  Proposition 10.8.

Let $(X,D,Q_{X})$ and $(Y,E,Q_{Y})$ be computable digit spaces so that
$(Y,E,Q_{Y})$ is decidable and well-covering with approximable choice. Then
$\mathop{\mathstrut\cal
C}\nolimits(X,Y)\subseteq\mathbb{C}_{\mathbb{F}(X,Y)}$.

###### Proof.

We show the statement by co-induction, that is we prove that

$\mathop{\mathstrut\cal
C}\nolimits(X,Y)\subseteq\mathcal{J}(\mathop{\mathstrut\cal
C}\nolimits(X,Y)).$

Let $\varepsilon_{Y}\in\mathbb{Q}_{+}$ be a well-covering number for $Y$ and
set

$V:=\mbox{$\\{\,(y,y^{\prime})\in Y\times
Y\mid\rho_{Y}(y,y^{\prime})<\varepsilon_{Y}/2\,\\}$}.$

Moreover, let $M_{X}$ be a bound of $X$ and $q_{X}<1$ the maximum of the
contraction factors of the $d\in D$. Let $\vec{x}\in X^{m}$ denote the
$m$-tuple $(x_{1},\ldots,x_{m})$, and similarly for $\vec{x}^{\prime}$ and
$\vec{\imath}$. Define

$U_{\vec{\imath}}^{(m)}:=\\{\,(\vec{x},\vec{x}^{\prime})\in X^{m}\times
X^{m}\mid(\forall 1\leq\kappa\leq
m)\rho_{X}(x_{\kappa},x^{\prime}_{\kappa})\leq q_{X}^{i_{\kappa}}\cdot
M_{X}\,\\},$

and set

$\mathop{\mathstrut\cal
C}\nolimits^{(m)}_{\vec{\imath}}:=\mbox{$\\{\,f\in\mathop{\mathstrut\cal
C}\nolimits^{(m)}(X,Y)\mid U^{(m)}_{\vec{\imath}}\subseteq(f\times
f)^{-1}[V]\,\\}$}.$

Since every $f\in\mathop{\mathstrut\cal C}\nolimits^{(m)}(X,Y)$ comes equipped
with a computable modulus of continuity, an $\vec{i}\in\mathbb{N}^{m}$ can be
computed for each such $f$ so that $f\in\mathop{\mathstrut\cal
C}\nolimits^{(m)}_{\vec{i}}$. Therefore, it suffices to show that
$\mathop{\mathstrut\cal
C}\nolimits^{(m)}_{\vec{\imath}}\subseteq\mathcal{J}(\mathop{\mathstrut\cal
C}\nolimits(X,Y))$, for all $m$ and every $\vec{\imath}\in\mathbb{N}^{m}$,
which will be done by induction on $i:=\max\mbox{$\\{\,i_{\kappa}\mid
1\leq\kappa\leq m\,\\}$}$.

For $i=0$ we have that $U^{(m)}_{\vec{\imath}}=X^{m}\times X^{m}$. Therefore,
it follows for $f\in\mathop{\mathstrut\cal C}\nolimits^{(m)}_{\vec{\imath}}$
and $\vec{u}\in Q_{X}^{m}$ that
$f[X^{m}]\subseteq\mathrm{B}_{\rho_{Y}}(f(\vec{u}),\varepsilon_{Y}/2)$. Since
$f$ is computable, a basic element $v\in Q_{Y}$ can be found with
$\rho_{Y}(f(\vec{u}),v)<\varepsilon_{Y}/2$. Use decidability to pick some
$e\in E$ with
$\mathrm{B}_{\rho_{Y}}(v,\varepsilon_{Y})\subseteq\mathop{\mathstrut\rm
range}(e)$. Then
$f[X^{m}]\subseteq\mathrm{B}_{\rho_{Y}}(v,\varepsilon_{Y})\subseteq\mathop{\mathstrut\rm
range}(e)$.

Note that by Proposition 5.15, digit $e$ has a computable right inverse
$e^{\prime}$. For $1\leq\kappa\leq\mathrm{ar}(e)$, set
$g_{\kappa}:={\mathop{\mathstrut\rm
pr}\nolimits^{(\mathrm{ar}(e))}_{\kappa}}\circ\,e^{\prime}\circ f$. Then
$g_{\kappa}$ is computable, that is $g_{\kappa}\in\mathop{\mathstrut\cal
C}\nolimits^{(m)}(X,Y)$. Since $f=e\circ(g_{1}\times\cdots\times
g_{\mathrm{ar}(e)})$, we therefore obtain with Rule (W) that
$f\in\mathcal{J}(\mathop{\mathstrut\cal C}\nolimits(X,Y))$.

Now, assume that $i>0$ and let $f\in\mathop{\mathstrut\cal
C}\nolimits^{(m)}_{\vec{\imath}}$. Then $(f\times f)^{-1}[V]\supseteq
U^{(m)}_{\vec{\imath}}$. Choose $1\leq j\leq m$ such that $i_{j}>0$. We want
to apply Rule (R). Therefore, we have to show that for all $d\in D$, $f\circ
d^{(j,m)}\in\mathcal{J}(\mathop{\mathstrut\cal C}\nolimits(X,Y))$. Since $d\in
D$ is a contraction, there is some $\ell<i_{j}$ so that

$(d\times
d)^{-1}[U^{(1)}_{i_{j}}]\supseteq\mbox{$\\{\,(\vec{z},\vec{z}^{\prime})\in
X^{\mathrm{ar}(d)}\times X^{\mathrm{ar}(d)}\mid(\forall
1\leq\sigma\leq\mathrm{ar}(d))\,\rho_{X}(z_{\sigma},z^{\prime}_{\sigma})\leq
q^{\ell}_{X}\cdot M_{X}\,\\}$}.$

For $1\leq\kappa\leq\mathrm{ar}(d)+m-1$ set

$k_{\kappa}:=\begin{cases}i_{\kappa}&\text{if $1\leq\kappa<j$ or
$\mathrm{ar}(d)+j\leq\kappa<\mathrm{ar}(d)+m$}\\\ \ell&\text{if
$j\leq\kappa<\mathrm{ar}(d)+j$.}\end{cases}$

Let $\bar{k}:=\max\mbox{$\\{\,k_{\kappa}\mid
1\leq\kappa\leq\mathrm{ar}(d)+m-1\,\\}$}$. Then $\bar{k}<i$. Moreover, we have
that $(d^{(j,m)}\times d^{(j,m)})^{-1}[U^{(m)}_{\vec{\imath}}]\supseteq
U^{(\mathrm{ar}(d)+m-1)}_{\vec{k}}$. Hence, $(f\circ d^{(j,m)}\times f\circ
d^{(j,m)})^{-1}[V]\supseteq U^{(\mathrm{ar}(d)+m-1)}_{\vec{k}}$, from which it
follows with the induction hypothesis that $f\circ
d^{(j,m)}\in\mathcal{J}(\mathop{\mathstrut\cal C}\nolimits(X,Y))$. ∎

######  Proposition 10.9.

Let $(X,D,Q_{X})$ and $(Y,E,Q_{Y})$ be decidable and well-covering computable
digit spaces with approximable choice. Then
$\mathbb{C}_{\mathbb{F}(X,Y)}\subseteq\mathop{\mathstrut\cal
C}\nolimits(X,Y)$.

###### Proof.

Since computable digit spaces with approximable choice are constructively
dense, Proposition 5.9 permits to derive the assertion for the dense subspaces
$Q^{(z)}_{D}$ and $Q^{(z^{\prime})}_{E}$, respectively, instead of $Q_{X}$ and
$Q_{Y}$. To simplify notation we write $Q_{D}$ instead of $Q^{(z)}_{D}$ and
similarly for $Q^{(z^{\prime})}_{E}$. Let $z\in Q_{X}$ and $z^{\prime}\in
Q_{Y}$ be fixed for the rest of the proof.

Now, let $M_{X}$ and $M_{Y}$, respectively, be bounds of $X$ and $Y$, and
$q_{X},q_{Y}<1$ be the maximum of the contraction factors of the $d\in D$
and/or $e\in E$. For $j\in\mathbb{N}$, set

$V_{j}:=\mbox{$\\{\,(y,y^{\prime})\in Y\times Y\mid\rho_{Y}(y,y^{\prime})\leq
q_{Y}^{j}\cdot M_{Y}\,\\}$}.$

Moreover, let

$U^{(m)}_{i}:=\mbox{$\\{\,(\vec{x},\vec{x}^{\prime})\in X^{m}\times
X^{m}\mid(\forall 1\leq\kappa\leq
m)\,\rho_{X}(x_{\kappa},x^{\prime}_{\kappa})\leq q_{X}^{i}\cdot M_{X}\,\\}$}$

and define

$\begin{split}G_{j}:=\\{\,f\in\mathbb{F}(X,Y)\mid(\exists
i\in\mathbb{N})\,U^{(\mathrm{ar}(f))}_{i}\subseteq(f\times
f)^{-1}[V_{j}]\wedge\hskip 85.35826pt\\\ (\forall\vec{u}\in
Q^{\mathrm{ar}(f)}_{D})(\exists v\in Q_{E})\,(f(\vec{u}),v)\in
V_{j}\,\\}.\end{split}$

Then we have to show that $\mathbb{C}_{\mathbb{F}(X,Y)}\subseteq G_{j}$, for
all $j\in\mathbb{N}$. We proceed by induction on $j$.

The case $j=0$ is obvious, as $V_{j}=Y\times Y$ and hence for $i:=0$,
$(f\times f)^{-1}[V_{j}]\supseteq U^{(\mathrm{ar}(f))}_{i}$, for every
$f\in\mathbb{F}(X,Y)$. In addition, $(f(\vec{u}),v)\in V_{j}$, for any
$\vec{u}\in Q^{\mathrm{ar}(f)}_{D}$ and $v\in Q_{E}$.

Now, assume that $j>0$. We show by side induction that
$\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})\subseteq G_{j}$. Note here that
$\mathbb{C}_{\mathbb{F}(X,Y)}=\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})$. By
the inductive definition of $\mathcal{J}(\mathbb{C}_{\mathbb{F}(X,Y)})$ it
therefore suffices to show that
$\Phi(\mathbb{C}_{\mathbb{F}(X,Y)})(G_{j})\subseteq G_{j}$, that is we need to
show that

  * (W)

If $e\in E$ and
$f_{1},\ldots,f_{\mathrm{ar}(e)}\in\mathbb{C}_{\mathbb{F}(X,Y)}$, then
$e\circ(f_{1}\times\cdots\times f_{\mathrm{ar}(e)})\in G_{j}$.

  * (R)

If $f\in\mathbb{F}(X,Y)$ and $1\leq k\leq\mathrm{ar}(f)$ so that $f\circ
d^{(k,\mathrm{ar}(f))}\in G_{j}$, for all $d\in D$, then $f\in G_{j}$.

(W) Let $e\in E$ and
$f_{1},\ldots,f_{\mathrm{ar}(e)}\in\mathbb{C}_{\mathbb{F}(X,Y)}$. As a digit
map, $e$ in particular has a computable modulus of continuity. Thus, we can
effectively find some $\ell\in\mathbb{N}$ so that $(e\times
e)^{-1}[V_{j}]\supseteq V_{\ell}^{\mathrm{ar}(e)}$. Since $e$ is a
contraction, it follows that $\ell<j$. By the main induction hypothesis
$f_{\kappa}\in G_{\ell}$, for $1\leq\kappa\leq\mathrm{ar}(e)$. Thus, we are
given $i_{1},\ldots,i_{\mathrm{ar}(e)}\in\mathbb{N}$ so that
$U^{(\mathrm{ar}(f_{\kappa}))}_{i_{\kappa}}\subseteq(f_{\kappa}\times
f_{\kappa})^{-1}[V_{\ell}]$, for $1\leq\kappa\leq\mathrm{ar}(e)$. Furthermore,
for each such $\kappa$ and every $\vec{u}_{\kappa}\in
Q^{\mathrm{ar}(f_{\kappa})}_{D}$ we can effectively find some $v_{\kappa}\in
Q_{E}$ with $(f_{\kappa}(\vec{u}_{\kappa}),v_{\kappa})\in V_{\ell}$. Let
$\bar{\imath}:=\max\mbox{$\\{\,i_{\kappa}\mid
1\leq\kappa\leq\mathrm{ar}(e)\,\\}$}$ and
$n:=\sum_{\kappa=1}^{\mathrm{ar}(e)}\mathrm{ar}(f_{\kappa})$. Then
$U^{(\mathrm{ar}(f_{\kappa}))}_{\bar{\imath}}\subseteq
U^{(\mathrm{ar}(f_{\kappa}))}_{i_{\kappa}}$, for
$1\leq\kappa\leq\mathrm{ar}(e)$, and

$\displaystyle((e\circ(f_{1}\times\cdots\times
f_{\mathrm{ar}(e)}))\times(e\circ(f_{1}\times\cdots\times
f_{\mathrm{ar}(e)})))[U^{(n)}_{\bar{\imath}}]$ $\displaystyle\hskip
20.00003pt(e\times E)\circ((f_{1}\times
f_{1})\times\cdots\times(f_{\mathrm{ar}(e)}\times
f_{\mathrm{ar}(e)}))[U^{(\mathrm{ar}(f_{1}))}_{i_{1}}\times\cdots\times
U^{(\mathrm{ar}(f_{\mathrm{ar}(e)}))}_{i_{\mathrm{ar}(e)}}]$
$\displaystyle\hskip 20.00003pt(e\times e)[(f_{1}\times
f_{1})[U^{(\mathrm{ar}(f_{1}))}_{i_{1}}]\times\cdots\times(f_{\mathrm{ar}(e)}\times
f_{\mathrm{ar}(e)})[U^{(\mathrm{ar}(f_{\mathrm{ar}(e)}))}_{i_{\mathrm{ar}(e)}}]]$
$\displaystyle\hskip 20.00003pt\subseteq(e\times
e)[V_{\ell}^{\mathrm{ar}(e)}]$ $\displaystyle\hskip 20.00003pt\subseteq
V_{j}.$

Moreover, we have that

$\displaystyle((e\circ(f_{1}\times\cdots\times
f_{\mathrm{ar}(e)}))(\vec{u}_{1},\ldots,\vec{u}_{\mathrm{ar}(e)}),e(v_{1},\ldots,v_{\mathrm{ar}(e)}))$
$\displaystyle\hskip
20.00003pt=(e(f_{1}(\vec{u}_{1}),\ldots,f_{\mathrm{ar}(e)}(\vec{u}_{\mathrm{ar}(e)})),e(v_{1},\ldots,v_{\mathrm{ar}(e)}))$
$\displaystyle\hskip 20.00003pt\in(e\times e)[V_{\ell}^{\mathrm{ar}(e)}]$
$\displaystyle\hskip 20.00003pt\subseteq V_{j}.$

Note that by definition, $e(v_{1},\ldots,v_{\mathrm{ar}(e)})\in Q_{E}$. Thus,
we have that $e\circ(f_{1}\times\cdots\times f_{\mathrm{ar}(e)})\in G_{j}$.

(R) Let $f\in\mathbb{F}(X,Y)$ and $1\leq i\leq\mathrm{ar}(f)$ so that $f\circ
d^{(i,\mathrm{ar}(f))}\in G_{j}$, for all $d\in D$. Then, for every $d\in D$,
we are given some $\ell_{d}\in\mathbb{N}$ with $((f\circ
d^{(i,\mathrm{ar}(f))})\times(f\circ
d^{(i,\mathrm{ar}(f))}))[U^{(\mathrm{ar}(d)+\mathrm{ar}(f)-1)}_{\ell_{d}}]\subseteq
V_{j}$. By Proposition 5.15 each $d\in D$ has a computable right inverse
$d^{\prime}$. Thus, some $r_{d}\in\mathbb{N}$ can effectively be found with
$(d^{\prime}\times d^{\prime})^{-1}[U^{(\mathrm{ar}(d))}_{\ell_{d}}]\supseteq
U^{(1)}_{r_{d}}$. Define $\bar{r}:=\max\mbox{$\\{\,r_{d}\mid d\in D\,\\}$}$
and $\hat{r}:=\min\mbox{$\\{\,r\geq\bar{r}\mid
q_{X}^{r}\leq\varepsilon_{X}/(2M_{X})\,\\}$}$, where $\varepsilon_{X}$ is a
well-covering number for $X$.

Now, let $\vec{x}=(x_{1},\ldots,x_{\mathrm{ar}(f)})\in X^{\mathrm{ar}(f)}$.
Then $\mathrm{B}_{\rho_{X}}(x_{i},q_{X}^{\hat{r}}\cdot
M_{X})\subseteq\mathrm{B}_{\rho_{X}}(x_{i},\varepsilon_{X}/2)$. By Theorem 7.1
we can therefore compute a basic element
$u\in\mathrm{B}_{\rho_{x}}(x_{i},\varepsilon_{X}/2)$. Use decidability to pick
some $\tilde{d}\in D$ with
$\mathrm{B}_{\rho_{X}}(u,\varepsilon_{X})\subseteq\mathop{\mathstrut\rm
range}(\tilde{d})$. Then $\mathrm{B}_{\rho_{X}}(x_{i},q_{X}^{\hat{r}}\cdot
M_{X})\subseteq\mathop{\mathstrut\rm range}(\tilde{d})$. Let
$\tilde{d}^{\prime}(x_{i})=(\tilde{z}_{1},\ldots,\tilde{z}_{\mathrm{ar}(\tilde{d})})$.
As $\hat{r}\geq r_{\tilde{d}}$, we moreover have that
$U^{(1)}_{\hat{r}}\subseteq U^{(1)}_{r_{\tilde{d}}}$ and hence that

$\tilde{d}^{\prime}[\mathrm{B}_{\rho_{x}}(x_{i},q^{\hat{r}}\cdot
M_{X})]\subseteq\mbox{$\\{\,(z_{1},\ldots,z_{\mathrm{ar}(\tilde{d})})\mid(\forall
1\leq\kappa\leq\mathrm{ar}(\tilde{d}))\,\rho_{X}(z_{\kappa},\tilde{z}_{\kappa})\leq
q_{X}^{\ell_{\tilde{d}}}\cdot M_{X}\,\\}$}.$ (11)

Define $k:=\max\\{\ell_{\tilde{d}},\hat{r}\\}$. We will show that $(f\times
f)[U^{(\mathrm{ar}(f))}_{k}]\subseteq V_{j}$. Let to this end
$(\vec{x},\vec{z})\in U^{(\mathrm{ar}(f))}_{k}$ with
$\vec{x}=(x_{1},\ldots,x_{\mathrm{ar}(f)})$ and similarly for $\vec{z}$. Then
$z_{i}\in\mathrm{B}_{\rho_{X}}(x_{i},q_{X}^{\hat{r}}\cdot
M_{X})\subseteq\mathop{\mathstrut\rm range}(\tilde{d})$. With (11) and the
assumption it follows that

$\begin{split}(f\times f)(\vec{x},\vec{z})=((f\times
f)\circ(\tilde{d}^{(i,m)}\times\tilde{d}^{(i,m)})\circ(\tilde{d}^{\prime(i,m)}\times\tilde{d}^{\prime(i,m)}))(\vec{x},\vec{z})\hskip
56.9055pt\mbox{}\\\ \in((f\times
f)\circ(\tilde{d}^{(i,m)}\times\tilde{d}^{(i,m)}))[U^{(\mathrm{ar}(\tilde{d})+\mathrm{ar}(f)-1)}_{\ell_{\tilde{d}}}]\subseteq
V_{j}.\end{split}$

It remains to verify the second requirement in the definition of $G_{j}$. Let
to this end $\vec{u}\in Q_{D}^{\mathrm{ar}(f)}$ with
$\vec{u}=(u_{1},\ldots,u_{\mathrm{ar}(f)})$. Then there is some $d\in D$ and
there are $w_{1},\ldots,w_{\mathrm{ar}(d)}\in Q_{D}$ such that
$u_{i}=d(w_{1},\ldots,w_{\mathrm{ar}(d)})$. By our assumption, there is some
$v\in Q_{E}$ with

$((f\circ
d^{(i,\mathrm{ar}(f))})(u_{1},\ldots,u_{i-1},w_{1},\ldots,w_{\mathrm{ar}(d)},u_{i+1},\ldots,u_{\mathrm{ar}(f)}),v)\in
V_{j}.$

Whence, $((f(\vec{u}),v)\in V_{j}$. This shows that $f\in G_{j}$.

Now, let $\mathbb{C}_{\mathbb{F}(X,Y)}$ and $p\in\mathbb{Q}_{+}$. Then some
$j\in\mathbb{N}$ can be computed with $q_{Y}^{j}\cdot M_{Y}\leq p$. The above
proof shows how for given $j\in\mathbb{N}$ some $i\in\mathbb{N}$ can
effectively be obtained so that, whenever $\vec{x},\vec{x}^{\prime}\in
X^{\mathrm{ar}(f)}$ with $\rho_{X}(\vec{x},\vec{x}^{\prime})\leq
q_{X}^{i}\cdot M_{X}$ then $\rho_{Y}(f(\vec{x}),f(\vec{x}^{\prime}))\leq
q_{Y}^{j}\cdot M_{Y}\leq p$, which shows that $f$ has a computable modulus of
continuity. Similarly, it follows that $f$ satisfies the second requirement
for computability. ∎

Summing up we obtain the following result.

######  Theorem 10.10.

Let $(X,D,Q_{X})$ and $(Y,E,Q_{Y})$ be decidable and well-covering computable
digit spaces with approximable choice. Then

$\mathbb{C}_{\mathbb{F}(X,Y)}=\mathop{\mathstrut\cal C}\nolimits(X,Y).$

##  11 Compact-valued functions

After having discussed how to obtain co-inductive characterisations of product
and hyperspaces, as well as of uniformly continuous functions, which are the
usual morphisms in the category of compact Hausdorff spaces, we will now
investigate compact-valued maps in this framework.

A central goal is to derive the functoriality of the compact hyperspace
construction within the scope of co-inductive characterisations of spaces and
morphisms. That is, we show that for maps $f\in\mathbb{C}_{\mathbb{F}(X,Y)}$,
$\mathcal{K}(f)\in\mathbb{C}_{\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))}$,
where for compact sets $K$, $\mathcal{K}(f)(K):=f[K]$. Classically, this is a
well known fact. However, the proofs given here are new, and, as has already
been pointed out, algorithms computing the action of the functor on morphisms
can be extracted in case that the underlying IFS are covering, compact and
weakly hyperbolic; similarly in the other cases considered in this section.

In a first step we will show that the continuous image of a compact set is
compact again. As follows from the definition, the algorithm evaluating a
function in $\mathbb{C}_{\mathbb{F}(X,Y)}$ on a given tuple of inputs uses the
information coming with the components of the input tuple only in as much as
it is needed, and also by dealing with each input component separately, not in
parallel. This property seems to be too weak to be able to lift the function
to the hyperspace of non-empty compact sets. The problem is that in the
hyperspace, the compact sets are approximated by iterating digit maps that
operate on the hyperspace. By doing so, the elements of the hyperspace are
considered as abstract objects, not as sets of points or tuples of such. The
internal structure is invisible to the IFS on the hyperspace.

In the subsequent Proposition we get around the problem by dealing with
compact sets that are cubes, but without such information being available it
is not clear how to proceed. In the general case we therefore restrict
ourselves to unary maps. Multi-ary maps $f\colon X^{n}\rightarrow Y$ are then
subsumed by using the IFS $(X^{n},D^{\times})$ instead of $(X,D)$.

######  Proposition 11.1.

Let $(X,D),(Y,E)$ be compact IFS, $f\in\mathbb{C}_{\mathbb{F}(X,Y)}$ and
$K_{1},\ldots,K_{\mathrm{ar}(f)}\in\mathbb{C}_{\mathcal{K}(X)}$. Then
$f[K_{1}\times\cdots\times K_{\mathrm{ar}(f)}]\in\mathbb{C}_{\mathcal{K}(Y)}$.

###### Proof.

For the co-inductive proof we need to derive a stronger statement. Let to this
end $f_{1},\ldots.f_{k}\in\mathbb{C}_{\mathbb{F}(X,Y)}$ and define

$(\bigcup_{i=1}^{k}f_{i})(\vec{x}):=\bigcup_{i=1}^{k}\\{f_{i}(\mathop{\mathstrut\rm
pr}\nolimits^{(k)}_{i}(\vec{x}))\\},$

for $\vec{x}\in\bigtimes_{i=1}^{k}X^{\mathrm{ar}(f_{i})}$. Set

$\mathbb{M}(X,Y):=\mbox{$\\{\,\bigcup_{i=1}^{k}f_{i}\mid k\geq 1\wedge(\forall
1\leq j\leq k)\,f_{j}\in\mathbb{C}_{\mathbb{F}(X,Y)}\,\\}$}.$

In general, the maps in $\mathbb{M}(X,Y)$ will be multi-valued. For such maps
$h\colon X\rightrightarrows Y$ and $K\in\mathcal{K}(X)$,
$h[K]:=\bigcup\mbox{$\\{\,h(x)\mid x\in K\,\\}$}$.

Let

$H:=\mbox{$\\{\,g[K_{1}\times\cdots\times K_{\mathrm{ar}(g)}]\mid
g\in\mathbb{M}(X,Y)\wedge
K_{1},\ldots,K_{\mathrm{ar}(g)}\in\mathbb{C}_{\mathcal{K}(X)}\,\\}$}.$

We will show that $H\subseteq\mathbb{C}_{\mathcal{K}(Y)}$. For
$\mathbb{Z}\subseteq\mathcal{K}(Y)$ define

$\Omega_{\mathcal{K}(Y)}(\mathbb{Z}):=\mbox{$\\{\,M\subseteq
Y\mid(\exists\bar{d}\in\mathcal{K}(D))(\exists
M_{1},\ldots,M_{\mathrm{ar}(\bar{d})}\in\mathbb{Z})\,M=\bar{d}(M_{1},\ldots,M_{\mathrm{ar}(\bar{d})})\,\\}$}.$

Then $\mathbb{C}_{\mathcal{K}(Y)}=\nu\Omega_{\mathcal{K}(Y)}$. Hence, we must
prove that $H\subseteq\Omega_{\mathcal{K}(Y)}(H)$. For $g\in\mathbb{M}(X,Y)$
let

$H(g):=\mbox{$\\{\,g[K_{1}\times\cdots\times K_{\mathrm{ar}(g)}]\mid
K_{1},\ldots,K_{\mathrm{ar}(g)}\in\mathbb{C}_{\mathcal{K}(X)}\,\\}$}.$

We first show that for all $f\in\mathbb{C}_{\mathbb{F}(X,Y)}$,
$H(f)\subseteq\Omega_{\mathcal{K}(Y)}(H)$.

Since
$\mathbb{C}_{\mathbb{F}(X,Y)}=\mathcal{J}^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})=\mu\Phi^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})$,
we can use induction to this aim. Set

$G:=\mbox{$\\{\,f\in\mathbb{F}(X,Y)\mid
H(f)\subseteq\Omega_{\mathcal{K}(Y)}(H)\,\\}$},$

then we need derive that

$\Phi_{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})(G)\subseteq G.$

We have to consider the two cases:

  * (W)

If $e\in E$ and $h\in\mathbb{C}_{\mathbb{F}(X,Y)}$, then $H(e\circ
h)\subseteq\Omega_{\mathcal{K}(Y)}(H)$.

  * (R)

If $f\in\mathbb{F}(X,Y)$ and $1\leq i\leq\mathrm{ar}(f)$ so that for all $d\in
D$, $H(f\circ d^{(i,\mathrm{ar}(f))})\subseteq\Omega_{\mathcal{K}(Y)}(H)$,
then $H(f)\subseteq\Omega_{\mathcal{K}(Y)}(H)$.

(W) Assume that $e\in E$ and $h\in\mathbb{C}_{\mathbb{F}(X,Y)}$, and let
$K_{1},\ldots,K_{\mathrm{ar}(h)}\in\mathbb{C}_{\mathcal{K}(X)}$. Then we need
to prove that $(e\circ h)[K_{1}\times\cdots\times
K_{\mathrm{ar}(h)}]\in\Omega_{\mathcal{K}(Y)}(H)$.

We have that

$(e\circ h)[K_{1}\times\cdots\times
K_{\mathrm{ar}(h)}]=e[h[K_{1}\times\cdots\times
K_{\mathrm{ar}(h)}]]=[e](h[K_{1}\times\cdots\times K_{\mathrm{ar}(h)}]).$

Since, $h\in\mathbb{C}_{\mathbb{F}(X,Y)}$ and
$K_{1},\ldots,K_{\mathrm{ar}(h)}\in\mathbb{C}_{\mathcal{K}(X)}$, it follows
that $h[K_{1}\times\cdots\times K_{\mathrm{ar}(h)}]\in H$. Therefore, $(e\circ
h)[K_{1}\times\cdots\times K_{\mathrm{ar}(h)}]\in\Omega_{\mathcal{K}(Y)}(H)$.

(R) Let $f\in\mathbb{F}(X,Y)$ and $1\leq i\leq\mathrm{ar}(f)$ so that for all
$d\in D$, $H(f\circ
d^{(i,\mathrm{ar}(f))})\subseteq\Omega_{\mathcal{K}(Y)}(H)$. Moreover, for
$1\leq\kappa\leq\mathrm{ar}(f)$, let
$K_{\kappa}\in\mathbb{C}_{\mathcal{K}(X)}$. Then there exist
$d_{1},\ldots,d_{r}\in D$ and
$N_{1},\ldots,N_{r}\in\mathbb{C}_{\mathcal{K}(X)}$ so that
$K_{i}=[d_{1},\ldots,d_{r}](N_{1},\ldots,N_{r})$. It follows that

$\displaystyle f[K_{1}\times\cdots\times K_{\mathrm{ar}(f)}]$
$\displaystyle\quad=f[K_{1}\times\cdots\times
K_{i-1}\times[d_{1},\ldots,d_{r}](N_{1},\ldots,N_{r})\times
K_{i+1}\times\cdots\times K_{\mathrm{ar}(f)}]$
$\displaystyle\quad=f[K_{1}\times\ldots\times
K_{i-1}\times(\bigcup_{\kappa=1}^{r}d_{\kappa}[N_{\kappa}])\times
K_{i+1}\times\cdots K_{\mathrm{ar}(f)}]$
$\displaystyle\quad=\bigcup_{\kappa=1}^{r}f[K_{1}\times\cdots\times
K_{i-1}\times d_{\kappa}[N_{\kappa}]\times K_{i+1}\times\cdots
K_{\mathrm{ar}(f)}]$ $\displaystyle\quad=\bigcup_{\kappa=1}^{r}(f\circ
d_{\kappa}^{(i,\mathrm{ar}(f))})[K_{1}\times\cdots\times K_{i-1}\times
N_{\kappa}\times K_{i+1}\times\cdots\times K_{\mathrm{ar}(f)}].$

Since $d_{\kappa}\in D$, for $1\leq\kappa\leq r$, it follows with our
assumption that there are
$e^{(\kappa)}_{1},\ldots,e^{(\kappa)}_{s_{\kappa}}\in E$ and
$M^{(\kappa)}_{1},\ldots,M^{(\kappa)}_{s_{\kappa}}\in H$ such that

$\begin{split}(f\circ d_{\kappa}^{(i,\mathrm{ar}(f))})[K_{1}\times\cdots\times
K_{i-1}\times N_{\kappa}\times K_{i+1}\times\cdots\times
K_{\mathrm{ar}(f)}]\hskip 56.9055pt\mbox{}\\\
=[e^{(\kappa)},\ldots,e^{(\kappa)}_{s_{\kappa}}](M^{(\kappa)}_{1},\ldots,M^{(\kappa)}_{s_{\kappa}}).\end{split}$

Thus,

$\bigcup_{\kappa=1}^{r}(f\circ
d_{\kappa}^{(i,\mathrm{ar}(f))})[K_{1}\times\cdots\times K_{i-1}\times
N_{\kappa}\times K_{i+1}\times\cdots\times
K_{\mathrm{ar}(f)}]=\bigcup_{\kappa=1}^{r}\bigcup_{\sigma_{\kappa}=1}^{n_{\kappa}}e^{(\kappa)}_{\sigma_{\kappa}}[M^{(\kappa)}_{\sigma_{\kappa}}].$

Note that the maps $e^{(\kappa)}_{\sigma_{\kappa}}$ with $1\leq\kappa\leq r$
and $1\leq\sigma_{\kappa}\leq n_{\kappa}$ need not be pairwise distinct. Let
$e_{1},\ldots,e_{\ell}\in E$ be pairwise distinct so that
$\\{e_{1},\ldots,e_{\ell}\\}=\bigcup_{\kappa=1}^{r}\\{e^{(\kappa)}_{1},\ldots,e^{(\kappa)}_{n_{\kappa}}\\}$.
Then

$\bigcup_{\kappa=1}^{r}\bigcup_{\sigma_{\kappa}=1}^{n_{\kappa}}e^{(\kappa)}_{\sigma_{\kappa}}[M^{(\kappa)}_{\sigma_{\kappa}}]=[e_{1},\ldots,e_{\ell}](L_{1},\ldots,L_{r}),$

where for $1\leq\iota\leq\ell$,
$L_{\iota}:=\bigcup\mbox{$\\{\,M^{(\kappa)}_{\sigma_{\kappa}}\mid
1\leq\kappa\leq r\wedge 1\leq\sigma_{\kappa}\leq n_{\kappa}\wedge
e^{(\kappa)}_{\sigma_{\kappa}}=e_{\iota}\,\\}$}$. Since
$M^{(\kappa)}_{\sigma_{\kappa}}=h^{(\kappa)}_{\sigma_{\kappa}}[\bigtimes_{\iota_{\kappa,\sigma_{\kappa}}=1}^{\mathrm{ar}(h^{(\kappa)}_{\sigma_{\kappa}})}\widetilde{M}^{(\kappa,\sigma_{\kappa})}_{\iota_{\kappa,\sigma_{\kappa}}}]$,
for some $h^{(\kappa)}_{\sigma_{\kappa}}\in\mathbb{M}(X,Y)$ and
$\widetilde{M}^{(\kappa,\sigma_{\kappa})}_{\iota_{\kappa,\sigma_{\kappa}}}\in\mathbb{C}_{\mathcal{K}(X)}$,
we have

$\begin{split}L_{\iota}=\hskip 363.62617pt\\\
(\bigcup\nolimits_{1\leq\kappa\leq r,1\leq\sigma_{\kappa}\leq
n_{\kappa}:\mathcal{K}(e^{(\kappa)}_{\sigma_{\kappa}})=\mathcal{K}(e_{\iota})}h^{(\kappa)}_{\sigma_{\kappa}})[\bigtimes\nolimits_{1\leq\kappa\leq
r,1\leq\sigma_{\kappa}\leq
n_{\kappa}:\mathcal{K}(e^{(\kappa)}_{\sigma_{\kappa}})=\mathcal{K}(e_{\iota})}\bigtimes\nolimits_{\iota_{\kappa,\sigma_{\kappa}}=1}^{\mathrm{ar}(h^{(\kappa)}_{\sigma_{\kappa}})}\widetilde{M}^{(\kappa,\sigma_{\kappa})}_{\iota_{\kappa,\sigma_{\kappa}}}].\end{split}$
(12)

It follows that $L_{\iota}\in H$ and thus $f[K_{1}\times\cdots\times
K_{\mathrm{ar}(f)}]\in\Omega_{\mathcal{K}(Y)}(H)$.

Observe that because of the possibility that the
$e^{(\kappa)}_{\sigma_{\kappa}}$ are not pairwise distinct and in particular
Line (12) we have to consider multi-valued maps in this proof.

Finally, we let $g\in\mathbb{M}(X,Y)$. It remains to show that
$H(g)\subseteq\Omega_{\mathcal{K}(Y)}(H)$. Let to this end
$f_{1},\ldots,f_{k}\in\mathbb{C}_{\mathbb{F}(X,Y)}$ with
$g=f_{1}\cup\cdots\cup f_{k}$, and
$K^{(\kappa)}_{\sigma_{\kappa}}\in\mathbb{C}_{\mathcal{K}(X)}$, for
$1\leq\kappa\leq k$ and $1\leq\sigma_{\kappa}\leq\mathrm{ar}(f_{\kappa})$.

As we have just seen, $f_{\kappa}[K^{(\kappa)}_{1}\times\cdots\times
K^{(\kappa)}_{\mathrm{ar}(f_{\kappa})}]\in\Omega_{\mathcal{K}(Y)}(H)$. Hence,
there are $e^{(\kappa)}_{1},\ldots,e^{(\kappa)}_{r_{\kappa}}\in E$ and
$M^{(\kappa)}_{1},\ldots,M^{(\kappa)}_{r_{\kappa}}\in H$, for $1\leq\kappa\leq
k$, with

$f_{\kappa}[K^{(\kappa)}_{1}\times\cdots\times
K^{(\kappa)}_{\mathrm{ar}(f_{\kappa})}]=[e^{(\kappa)}_{1},\ldots,e^{(\kappa)}_{r_{\kappa}}](M^{(\kappa)}_{1},\ldots,M^{(\kappa)}_{r_{\kappa}}).$

Again the $e^{(\kappa)}_{\iota_{\kappa}}$ with $1\leq\kappa\leq k$ and
$1\leq\iota_{\kappa}\leq r_{\kappa}$ need not be pairwise distinct. By
proceeding as in the previous proof step we can find pairwise distinct
$e^{\prime}_{1},\ldots,e^{\prime}_{\ell}\in E$ and $L_{1},\ldots,L_{\ell}\in
H$ so that
$\\{e^{\prime}_{1},\ldots,e^{\prime}_{\ell}\\}=\\{\,e^{(\kappa)}_{\iota_{\kappa}}\mid
1\leq\kappa\leq k\wedge 1\leq\iota_{\kappa}\leq r_{\kappa}\,\\}$ and

$\displaystyle g[K^{(1)}_{1}\times\cdots\times K^{(k)}_{\mathrm{ar}(f_{k})}]$
$\displaystyle=\bigcup_{\kappa=1}^{k}f_{\kappa}[K^{(\kappa)}_{1}\times\cdots\times
K^{(\kappa)}_{\mathrm{ar}(f_{\kappa})}]$
$\displaystyle=\bigcup_{\kappa=1}^{k}[e^{(\kappa)}_{1},\ldots,e^{(\kappa)}_{r_{\kappa}}](M^{(\kappa)}_{1},\ldots,M^{(\kappa)}_{r_{\kappa}})$
$\displaystyle=[e^{\prime}_{1},\ldots,e^{\prime}_{\ell}](L_{1},\ldots,L_{\ell}),$

showing that $g[K^{(1)}_{1}\times\cdots\times
K^{(k)}_{\mathrm{ar}(f_{k})}]\in\Omega_{\mathcal{K}(Y)}(H)$. ∎

For the subsequent technical lemma we extend the union taking operation to
compact-valued maps. For Hausdorff spaces $X,Y,Z$ such that $Z$ is compact,
and maps $f\colon X\rightarrow\mathcal{K}(Z)$ and $g\colon
Y\rightarrow\mathcal{K}(Z)$ define $f\cup g\colon X\times Y\to\mathcal{K}(Z)$
by

$(f\cup g)(x,y):=f(x)\cup g(y).$

######  Lemma 11.2.

Let $(X,D)$, $(Y,E)$ be compact IFS and

$F:=\mbox{$\\{\,\bigcup_{i=1}^{k}\mathcal{K}(f_{i})\mid k\geq 1\wedge(\forall
1\leq i\leq k)\,f_{i}\in\mathbb{C}^{(1)}_{\mathbb{F}(X,Y)}\,\\}$}.$

Then $\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$ is closed under union.

###### Proof.

Let

$A:=\mbox{$\\{\,f\in\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))\mid(\forall
g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F))\,f\cup
g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)\,\\}$}.$

We will prove by induction that
$\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)\subseteq A$, that is we have
to show that

$\Phi^{\mathcal{K}(X),\mathcal{K}(Y)}(F)(A)\subseteq A,$

which in turn means that we have to verify Rules (W) and (R).

($\text{W}_{\text{main}}$) Let $\bar{e}\in\mathcal{K}(E)$ with
$\bar{e}=[e_{1},\ldots,e_{r}]$, for $e_{1},\ldots,e_{r}\in E$. Moreover, let
$f_{1},\ldots,f_{r}\in F$. We must demonstrate that
$\bar{e}\circ(f_{1}\times\cdots\times f_{r})\in A$. To this end we have to
show that for all $g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$,
$\bar{e}\circ(f_{1}\times\cdots\times f_{r})\cup
g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. For
$h\in\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))$ set

$B(h):=\mbox{$\\{\,g\in\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))\mid h\cup
g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)\,\\}$}.$

Let $h:=\bar{e}\circ(f_{1}\times\cdots\times f_{r})$. We prove that
$\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)\subseteq B(h)$, that is we
have to demonstrate that

$\Phi^{\mathcal{K}(X),\mathcal{K}(Y)}(F)(B(h))\subseteq B(h),$ (13)

which is done by side induction.

($\text{W}_{\text{side}}$) Let $\hat{e}\in\mathcal{K}(E)$, say
$\hat{e}=[e^{\prime}_{1},\ldots,e^{\prime}_{s}]$ with
$e^{\prime}_{1},\ldots,e^{\prime}_{s}\in E$. Furthermore, let
$g_{1},\ldots,g_{s}\in F$. We need to show that

$(\bar{e}\circ(f_{1}\times\cdots\times
f_{r}))\cup(\hat{e}\circ(g_{1}\times\cdots\times
g_{s}))\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F).$

Note that $\bar{e}=\mathcal{K}(e_{1})\cup\cdots\cup\mathcal{K}(e_{r})$ and
analogously for $\hat{e}$. Then

$\begin{split}(\bar{e}\circ(f_{1}\times\cdots\times
f_{r}))\cup(\hat{e}\circ(g_{1}\times\cdots\times g_{s}))=\hskip 128.0374pt\\\
\mathcal{K}(e_{1})\circ f_{1}\cup\cdots\cup\mathcal{K}(e_{r})\circ
f_{r}\cup\mathcal{K}(e^{\prime}_{1})\circ
g_{1}\cup\cdots\cup\mathcal{K}(e^{\prime}_{s})\circ g_{s}.\end{split}$

Let $R:=\mbox{$\\{\,(j_{1},j_{2})\mid 1\leq j_{1}\leq r\wedge 1\leq j_{2}\leq
s\wedge e_{j_{1}}=e^{\prime}_{j_{2}}\,\\}$}$. Then we have that

$\displaystyle\mathcal{K}(e_{1})\circ
f_{1}\cup\cdots\cup\mathcal{K}(e_{r})\circ
f_{r}\cup\mathcal{K}(e^{\prime}_{1})\circ
g_{1}\cup\cdots\cup\mathcal{K}(e^{\prime}_{s})\circ g_{s}$
$\displaystyle\quad=[e_{i_{1}},\ldots,e_{i_{k}},e_{i_{k+1}},\ldots,e_{i_{k^{\prime}}},e^{\prime}_{i_{k^{\prime}+1}},\ldots,e^{\prime}_{i_{\ell}}]\circ((f_{i_{1}}\cup
g_{i_{1}})\times\cdots\times(f_{i_{k}}\cup g_{i_{k}})\times$
$\displaystyle\hskip 227.62204ptf_{i_{k+1}}\times\cdots\times
f_{i_{k^{\prime}}}\times g_{i_{k^{\prime}+1}}\times\cdots\times
g_{i_{\ell}}),$

where $1\leq k\leq k^{\prime}\leq\ell$ and
$i_{1},\ldots,i_{\ell},i^{\prime}_{1},\ldots,i^{\prime}_{k}\in\mathbb{N}$ so
that

$\displaystyle R=\\{(i_{1},i^{\prime}_{1}),\ldots,(i_{k},i^{\prime}_{k})\\},$
$\displaystyle\\{1,\ldots,r\\}\setminus\mathop{\mathstrut\rm
pr}\nolimits^{(2)}_{1}[R]=\\{i_{k+1},\ldots,i_{k^{\prime}}\\},$
$\displaystyle\\{1,\ldots,s\\}\setminus\mathop{\mathstrut\rm
pr}\nolimits^{(2)}_{2}[R]=\\{i_{k^{\prime}+1},\ldots,i_{\ell}\\}.$

It follows that
$e_{i_{1}},\ldots,e_{i_{k}},e_{i_{k+1}},\ldots,e_{i_{k^{\prime}}},e^{\prime}_{i_{k^{\prime}+1}},\ldots,e^{\prime}_{i_{\ell}}$
are pairwise distinct and $f_{i_{1}}\cup g_{i_{1}},\ldots,f_{i_{k}}\cup
g_{i_{k}},f_{i_{k+1}},\ldots,f_{i_{k^{\prime}}},g_{i_{k^{\prime}+1}},\ldots,g_{i_{\ell}}\in
F$. Thus, $(\bar{e}\circ(f_{1}\times\cdots\times
f_{r}))\cup(\hat{e}\circ(g_{1}\times\cdots\times
g_{s}))\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$, by Rule (W).

($\text{R}_{\text{side}}$) Let $g\in\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))$
and $1\leq i\leq\mathrm{ar}(g)$ so that $g\circ\bar{e}^{(i,\mathrm{ar}(g))}\in
B(h)$, for all $\bar{e}\in\mathcal{K}(E)$. Then
$h\cup(g\circ\bar{e}^{(i,\mathrm{ar}(g))})\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$.
Set $\hat{h}:=h\cup g$. Obviously,
$\mathrm{ar}(\hat{h})=\mathrm{ar}(h)+\mathrm{ar}(g)$. For
$j:=\mathrm{ar}(h)+i$ we therefore have that
$\hat{h}\circ\bar{e}^{(j,\mathrm{ar}(\hat{h}))}=h\cup(g\circ\bar{e}^{(i,\mathrm{ar}(g))})$.
It follows that
$\hat{h}\circ\bar{e}^{(j,\mathrm{ar}(\hat{h}))}\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$,
for all $\bar{e}\in\mathcal{K}(E)$, from which we obtain with Rule (R) that
$\hat{h}\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. Hence, $g\in
B(h)$. This proves (13).

($\text{R}_{\text{main}}$) It remains to verify Rule (R) in the main
induction. Let $f\in\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))$ and $1\leq
i\leq\mathrm{ar}(f)$ such that for all $\bar{d}\in\mathcal{K}(D)$,
$f\circ\bar{d}^{(i,\mathrm{ar}(f))}\in A$. Thus,
$(f\circ\bar{d}^{(i,\mathrm{ar}(f))})\cup
g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$, for all
$g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. Set
$\tilde{h}_{g}:=f\cup g$. Then
$\mathrm{ar}(\tilde{h}_{g})=\mathrm{ar}(f)+\mathrm{ar}(g)$ and for all
$\bar{d}\in\mathcal{K}(D)$,

$\tilde{h}_{g}\circ\bar{d}^{(i,\mathrm{ar}(\tilde{h}_{g}))}=(f\circ\bar{d}^{(i,\mathrm{ar}(f))})\cup
g.$

Since $(f\circ\bar{d}^{(i,\mathrm{ar}(f))})\cup
g\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$, by our assumption, we
obtain with Rule (R) that
$\tilde{h}_{g}\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. Thus $f\in
A$. ∎

######  Theorem 11.3.

Let $(X,D),(Y,E)$ be compact IFS. Then for all
$f\in\mathbb{C}^{(1)}_{\mathbb{F}(X,Y)}$,

$\mathcal{K}(f)\in\mathbb{C}_{\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))}.$

###### Proof.

Again we need to derive a stronger statement. Let

$F:=\mbox{$\\{\,\bigcup_{i=1}^{k}\mathcal{K}(f_{i})\mid k\geq 1\wedge(\forall
1\leq i\leq k)\,f_{i}\in\mathbb{C}^{(1)}_{\mathbb{F}(X,Y)}\,\\}$}.$

We will show that
$F\subseteq\mathbb{C}_{\mathbb{F}(\mathcal{K}(X),\mathcal{K}(Y))}$. By using
co-induction it is sufficient to prove that
$F\subseteq\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$.

Set

$B:=\mbox{$\\{\,f\in\mathbb{F}(X,Y)\mid\mathrm{ar}(f)=1\rightarrow\mathcal{K}(f)\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)\,\\}$}.$

Then we show first that $\mathbb{C}_{\mathbb{F}(X,Y)}\subseteq B$. Because
$\mathbb{C}_{\mathbb{F}(X,Y)}=\mathcal{J}^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})$,
we only need to derive that
$\mathcal{J}^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})\subseteq B$. To achieve this
we use induction, that is we show
$\Phi^{X,Y}(\mathbb{C}_{\mathbb{F}(X,Y)})(B)\subseteq B$. Hereto we have to
verify the following two rules:

  * (W)

If $e\in E$ and $h\in\mathbb{C}_{\mathbb{F}(X,Y)}$, then $e\circ h\in B$.

  * (R)

If $f\in\mathbb{F}(X,Y)$ and $1\leq i\leq\mathrm{ar}(f)$ such that for all
$d\in D$, $f\circ d^{(i,\mathrm{ar}(f))}\in B$, then $f\in B$.

(W) We have that $\mathcal{K}(e\circ
h)=\mathcal{K}(e)\circ\mathcal{K}(h)=[e]\circ\mathcal{K}(h)$. Now, assume that
$\mathrm{ar}(e\circ h)=1$, then also $\mathrm{ar}(h)=1$. Since
$\mathcal{K}(h)\in F$ and $[e]\in\mathcal{K}(E)$, it follows with Rule (W) for
$\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$ that
$[e]\circ\mathcal{K}(h)\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$.
Thus, $e\circ h\in B$

(R) Let $f\in\mathbb{F}(X,Y)$ and $1\leq i\leq\mathrm{ar}(f)$ so that for all
$d\in D$, $f\circ d^{(i,\mathrm{ar}(f))}\in B$. Suppose that
$\mathrm{ar}(f\circ d^{(i,\mathrm{ar}(f))})=1$. Then $\mathrm{ar}(f)=1$ and
hence $i=1$. Moreover, $\mathcal{K}(f\circ
d)\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. Now, let
$\bar{d}\in\mathcal{K}(D)$ with $\bar{d}=[d_{1},\ldots,d_{s}]$. Note that
$[d_{1},\ldots,d_{s}]=\mathcal{K}(d_{1})\cup\cdots\cup\mathcal{K}(d_{s})$. It
follows that

$\mathcal{K}(f)\circ[d_{1},\ldots,d_{s}]=\mathcal{K}(f)\circ(\bigcup_{\kappa=1}^{s}\mathcal{K}(d_{\kappa}))=\bigcup_{\kappa=1}^{s}\mathcal{K}(f)\circ\mathcal{K}(d_{\kappa})=\bigcup_{\kappa=1}^{s}\mathcal{K}(f\circ
d_{\kappa}).$

By our assumption, $f\circ{d_{\kappa}}\in B$. Hence, $\mathcal{K}(f\circ
d_{\kappa})\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$, for all
$1\leq\kappa\leq s$, as a consequence of which we obtain with Lemma 11.2 that
$\bigcup_{\kappa=1}^{s}\mathcal{K}(f\circ
d_{\kappa})\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. This shows that
$\mathcal{K}(f)\circ\bar{d}\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$,
for all $\bar{d}\in\mathcal{K}(D)$. By Rule (R) for
$\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$ we thus have that
$\mathcal{K}(f)\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$, which means
that $f\in B$.

Finally, let $f_{1},\ldots,f_{k}\in\mathbb{C}^{(1)}_{\mathbb{F}(X,Y)}$. Then
$f_{1},\ldots,f_{k}\in B$ and hence
$\mathcal{K}(f_{j})\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$, for
$1\leq j\leq k$. With Lemma 11.2 we therefore have that also
$\bigcup_{j=1}^{k}\mathcal{K}(f_{j})\in\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$,
which shows that $F\subseteq\mathcal{J}^{\mathcal{K}(X),\mathcal{K}(Y)}(F)$. ∎

The simplest compact sets are the singleton sets of points of the underlying
space.

######  Lemma 11.4.

Let $(X,D)$ be a compact IFS. Then $\mbox{$\\{\,\\{x\\}\mid
x\in\mathbb{C}_{X}\,\\}$}\subseteq\mathbb{C}_{\mathcal{K}(X)}$.

###### Proof.

Let $\mathbb{Z}:=\mbox{$\\{\,\\{x\\}\mid x\in\mathbb{C}_{X}\,\\}$}$. The
statement will be derived by co-induction. To this end we have to show that
$\mathbb{Z}\subseteq\Omega_{\mathcal{K}(X)}(\mathbb{Z})$.

Let $x\in X$. Since $x\in\mathbb{C}_{X}$, there are $d\in D$ and
$y\in\mathbb{C}_{X}$ with $x=d(y)$. Then $\\{y\\}\in\mathbb{Z}$ and

$[d](\\{y\\})=d[\\{y\\}]=\\{d(y)\\}=\\{x\\}.\qed$

Define $\eta\colon\mathbb{C}_{X}\rightarrow\mathbb{C}_{\mathcal{K}(X)}$ by
letting

$\eta(x):=\\{x\\}.$

######  Proposition 11.5.

Let $(X,D)$ be a compact IFS. Then
$\eta\in\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(X))}$.

###### Proof.

Again we use co-induction to derive the statement: We show that
$\\{\eta\\}\subseteq\mathcal{J}^{X,\mathcal{K}(X)}(\\{\eta\\})$. Note that for
any $d\in D$, $[d]\in\mathcal{K}(D)$. Moreover, $[d]\circ\eta=\eta\circ d$. By
Rule (W) we have that
$[d]\circ\eta\in\mathcal{J}^{X,\mathcal{K}(X)}(\\{\eta\\})$, i.e., $\eta\circ
d\in\mathcal{J}^{X,\mathcal{K}(X)}(\\{\eta\\})$. Therefore
$\eta\in\mathcal{J}^{X,\mathcal{K}(X)}(\\{\eta\\})$, by Rule (R). ∎

We have already introduced the union taking operation for compact-valued maps.

######  Theorem 11.6.

Let $(X,D)$, $(Y,E)$ be extended IFS and $(Z,C)$ be a compact IFS. Then, for
$f\in\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))}$ and
$g\in\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))}$, $f\cup
g\in\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))}$.

###### Proof.

The proof of this result essentially follows the lines of the proof of Lemma
11.2. However, now we use strong co-induction. Let

$A:=\mbox{$\\{\,f\cup g\mid
f\in\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))}\wedge
g\in\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))}\,\\}$}.$

Then we need to show that $A\subseteq\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(A\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$.
Set

$B:=\mbox{$\\{\,f\in\mathbb{F}(X,\mathcal{K}(Z))\mid(\forall
g\in\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))})\,f\cup g\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(A\cup\mathbb{C}_{\mathbb{F}(X\times
Y,\mathcal{K}(Z))})\,\\}$}.$

We show that $\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))}\subseteq B$. Since
$\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))}=\mathcal{J}^{X,\mathcal{K}(Z)}(\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))})$,
it suffices to prove that
$\mathcal{J}^{X,\mathcal{K}(Z)}(\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))})\subseteq
B$. By induction we show that
$\Phi^{X,\mathcal{K}(Z)}(\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))})(B)\subseteq
B$, which means that we have to verify Rules (W) and (R).

($\text{W}_{\text{main}}$) Let $\bar{c}\in\mathcal{K}(C)$ with
$\bar{c}=[c_{1},\ldots,c_{r}]$, for $c_{1},\ldots,c_{r}\in C$. Moreover, let
$f_{1},\ldots,f_{r}\in\mathbb{C}_{\mathbb{F}(X,\mathcal{K}(Z))}$. We must
demonstrate that $\bar{c}\circ(f_{1}\times\cdots\times f_{r})\in B$. To this
end we have to show that for all
$g\in\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))}$,
$(\bar{c}\circ(f_{1}\times\cdots f_{r}))\cup g\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(A\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$.
For $h\in\mathbb{F}(X,\mathcal{K}(Z))$ set

$H(h):=\mbox{$\\{\,g\in\mathbb{F}(Y,\mathcal{K}(Z))\mid h\cup
g\in\mathcal{J}^{X\times Y,\mathcal{K}(Z)}(A\cup\mathbb{C}_{\mathbb{F}(X\times
Y,\mathcal{K}(Z))})\,\\}$}.$

Let $h:=\bar{c}\circ(f_{1}\times\cdots\times f_{r})$. We prove that
$\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))}\subseteq H(h)$, for which it
suffices to demonstrate that

$\Phi^{Y,\mathcal{K}(Z)}(\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))})(H(h))\subseteq
H(h),$ (14)

which is done by side induction.

($\text{W}_{\text{side}}$) Let $\hat{c}\in\mathcal{K}(C)$, say
$\hat{c}=[c^{\prime}_{1},\ldots,c^{\prime}_{s}]$ with
$c^{\prime}_{1},\ldots,c^{\prime}_{s}\in C$. Furthermore, let
$g_{1},\ldots,g_{s}\in\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))}$. We need to
show that

$(\bar{c}\circ(f_{1}\times\cdots\times
f_{r}))\cup(\hat{c}\circ(g_{1}\times\cdots\times
g_{s}))\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(A\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))}).$

Note again that $\bar{c}=\mathcal{K}(c_{1})\cup\cdots\cup\mathcal{K}(c_{r})$,
and analogously for $\hat{c}$. Then

$\begin{split}(\bar{c}\circ(f_{1}\times\cdots\times
f_{r}))\cup(\hat{c}\circ(g_{1}\times\cdots\times g_{s}))=\hskip 128.0374pt\\\
\mathcal{K}(c_{1})\circ f_{1}\cup\cdots\cup\mathcal{K}(c_{r})\circ
f_{r}\cup\mathcal{K}(c^{\prime}_{1})\circ
g_{1}\cup\cdots\cup\mathcal{K}(c^{\prime}_{s})\circ g_{s}.\end{split}$

As in the proof of Lemma 11.2 it follows that there are pairwise distinct
$c^{\prime\prime}_{i_{1}}$, …, $c^{\prime\prime}_{i_{k}}$,
$c^{\prime\prime}_{i_{k+1}}$, …, $c^{\prime\prime}_{i_{k^{\prime}}}$, …,
$c^{\prime\prime}_{i_{k^{\prime}+1}}$,
$c^{\prime\prime}_{\ell}\in\\{c_{1},\ldots,c_{r},c^{\prime}_{1},\ldots,c^{\prime}_{s}\\}$
so that (up to some reshuffling of arguments)

$\begin{split}\mathcal{K}(c_{1})\circ
f_{1}\cup\cdots\cup\mathcal{K}(c_{r})\circ
f_{r}\cup\mathcal{K}(c^{\prime}_{1})\circ
g_{1}\cup\cdots\cup\mathcal{K}(c^{\prime}_{s})\circ g_{s}\hskip
130.88284pt\mbox{}\\\
=[c^{\prime\prime}_{i_{1}},\ldots,c^{\prime\prime}{i_{\ell}}]\circ((f_{i_{1}}\cup
g_{i_{1}})\times\cdots\times(f_{i_{k}}\cup g^{\prime}_{i_{k}})\times
f_{i_{k+1}}\times\cdots\times f_{i_{k^{\prime}}}\times
g_{i_{k^{\prime}+1}}\times\cdots\times g_{i_{\ell}}).\end{split}$

Then
$[c^{\prime\prime}_{i_{1}},\ldots,c^{\prime\prime}{i_{\ell}}]\in\mathcal{K}(C)$,
$f_{i_{1}}\cup g_{i_{1}},\ldots,f_{i_{k}}\cup g_{i_{k}}\in A$, and
$f_{i_{k+1}},\ldots,f_{i_{k^{\prime}}},g_{i_{k^{\prime}+1}},\ldots,g_{i_{\ell}}\in\mathbb{C}_{\mathbb{F}(X\times
Y,\mathcal{K}(Z))}$, where we identify maps $f\colon X^{n}\rightarrow Z$ with
$f\circ(\mathop{\mathstrut\rm
pr}\nolimits^{(n+1)}_{1}\times\cdots\times\mathop{\mathstrut\rm
pr}\nolimits^{(n+1)}_{n})\colon X^{n}\times Y\to Z$, and similarly for maps
$g\colon Y^{m}\rightarrow Z$. Thus, $(\bar{c}\circ(f_{1}\times\cdots\times
f_{r}))\cup(\hat{c}\circ(g_{1}\times\cdots\times
g_{s}))\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(A\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$ by
Rule (W).

Note that the remaining proof steps are essentially the same as in the proof
of Lemma 11.2. We include them only for completeness reasons.

($\text{R}_{\text{side}}$) Let $g\in\mathbb{F}(Y,\mathcal{K}(Z))$ and $1\leq
i\leq\mathrm{ar}(g)$ so that $g\circ e^{(i,\mathrm{ar}(g))}\in B(h)$, for all
$e\in E$. Then $h\cup(g\circ e^{(i,\mathrm{ar}(g))})\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(F\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$.
Let $\hat{h}:=h\cup g$. Then
$\mathrm{ar}(\hat{h})=\mathrm{ar}(h)+\mathrm{ar}(g)$. For
$j:=\mathrm{ar}(h)+i$ we therefore have that $\hat{h}\circ
e^{(j,\mathrm{ar}(\hat{h}))}=h\cup(g\circ e^{(i,\mathrm{ar}(g))})$. It follows
that $\hat{h}\circ e^{(j,\mathrm{ar}(\hat{h}))}\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(F\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$,
for all $e\in E$, from which we obtain by Rule (R) that
$\hat{h}\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(F\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$.
Hence, $g\in B(h)$. This proves (14).

($\text{R}_{\text{main}}$) It remains to verify Rule (R) in the main
induction. Let $f\in A$ and $1\leq i\leq\mathrm{ar}(f)$ such that for all
$d\in D$, $f\circ d^{(i,\mathrm{ar}(f))}\in A$. Thus, $(f\circ
d^{(i,\mathrm{ar}(f))})\cup g\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(F\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$,
for all $g\in\mathbb{C}_{\mathbb{F}(Y,\mathcal{K}(Z))}$. Set
$\bar{h}_{g}:=f\cup g$. Then
$\mathrm{ar}(\bar{h}_{g})=\mathrm{ar}(f)+\mathrm{ar}(g)$ and for all $d\in D$,

$\bar{h}_{g}\circ d^{(i,\mathrm{ar}(\bar{h}_{g}))}=(f\circ
d^{(i,\mathrm{ar}(f))})\cup g.$

Since $(f\circ d^{(i,\mathrm{ar}(f))})\cup g\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(F\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$ by
our assumption, we obtain with Rule (R) that
$\bar{h}_{g}\in\mathcal{J}^{X\times
Y,\mathcal{K}(Z)}(F\cup\mathbb{C}_{\mathbb{F}(X\times Y,\mathcal{K}(Z))})$.
Thus $f\in A$. ∎

Since the identity on any extended IFS is in $\mathbb{C}_{\mathbb{F}(X,X)}$,
by Lemma 10.3(1), it follows in particular that the binary operation of taking
unions is in
$\mathbb{C}_{\mathbb{F}(\mathcal{K}(X)\times\mathcal{K}(X),\mathcal{K}(X))}$.

######  Corollary 11.7.

Let $(X,D)$ be a compact IFS. Then the following two statements hold:

  1. 1.

$\mathbb{C}_{\mathcal{K}(X)}$ is closed under taking finite unions, that is,
for all $K,M\subseteq X$,

$K,M\in\mathbb{C}_{\mathcal{K}(X)}\Rightarrow K\cup
M\in\mathbb{C}_{\mathcal{K}(X)}.$

  2. 2.

$\cup\in\mathbb{C}_{\mathbb{F}(\mathcal{K}(X)\times\mathcal{K}(X),\mathcal{K}(X))}$.

The first statement follows from the second one by Proposition 10.5.

##  12 Michael’s Theorem

In his seminal 1951 paper on spaces of subsets [23], E. Michael showed that
the union of all sets in a compact set of compact sets is compact again. We
will reprove this result in a non-topological way by using only the co-
inductive characterisations of the spaces involved.

The difficulty we have to overcome herewith is that, as we have seen in
Section 9, in general the canonical maps in $\mathcal{K}^{2}(D)$ are no longer
of type $\mathcal{K}^{2}(X)^{r}\to\mathcal{K}^{2}(X)$, even if all maps in $D$
are unary. Thus, $(\mathcal{K}^{2}(X),\mathcal{K}^{2}(D))$ will not be an
extended IFS any more.

Let
$[[d^{(1)}_{1},\ldots,d^{(1)}_{r_{1}}],\ldots,[d^{(n)}_{1},\ldots,d^{(n)}_{r_{n}}]]\in\mathcal{K}^{2}(D)$
and $\mathbb{K}_{1},\ldots,\mathbb{K}_{n}\in\mathcal{K}^{2}(X)$. Then we have

$\displaystyle\bigcup[[d^{(1)}_{1},\ldots,d^{(1)}_{r_{1}}],\ldots,[d^{(n)}_{1},\ldots,d^{(n)}_{r_{n}}]](\mathbb{K}_{1},\ldots,\mathbb{K}_{n})$
$\displaystyle\quad=\bigcup\bigcup_{\kappa=1}^{n}[d^{(\kappa)}_{1},\ldots,d^{(\kappa)}_{r_{\kappa}}][\mathbb{K}_{\kappa}]$
$\displaystyle\quad=\bigcup\bigcup_{\kappa=1}^{n}\mbox{$\\{\,\bigcup_{{\sigma_{\kappa}}=1}^{r_{\kappa}}d^{(\kappa)}_{\sigma_{\kappa}}[K^{(\kappa)}_{\sigma_{\kappa}}]\mid(K^{(\kappa)}_{1},\ldots,K^{(\kappa)}_{r_{\kappa}})\in\mathbb{K}_{\kappa}\,\\}$}$
$\displaystyle\quad=\bigcup_{\kappa=1}^{n}\bigcup\mbox{$\\{\,\bigcup_{{\sigma_{\kappa}}=1}^{r_{\kappa}}d^{(\kappa)}_{\sigma_{\kappa}}[K^{(\kappa)}_{\sigma_{\kappa}}]\mid(K^{(\kappa)}_{1},\ldots,K^{(\kappa)}_{r_{\kappa}})\in\mathbb{K}_{\kappa}\,\\}$}$
$\displaystyle\quad=\bigcup_{\kappa=1}^{n}\bigcup_{{\sigma_{\kappa}}=1}^{r_{\kappa}}\bigcup\mbox{$\\{\,d^{(\kappa)}_{\sigma_{\kappa}}[K^{(\kappa)}_{\sigma_{\kappa}}]\mid
K^{(\kappa)}_{\sigma_{\kappa}}\in\mathop{\mathstrut\rm
pr}\nolimits^{({r_{\kappa}})}_{\sigma_{\kappa}}[\mathbb{K}_{\kappa}]\,\\}$}$
$\displaystyle\quad=\bigcup_{\kappa=1}^{n}\bigcup_{{\sigma_{\kappa}}=1}^{r_{\kappa}}\bigcup\mathcal{K}(d^{(\kappa)}_{\sigma_{\kappa}})[\mathop{\mathstrut\rm
pr}\nolimits^{({r_{\kappa}})}_{\sigma_{\kappa}}[\mathbb{K}_{\kappa}]].$

Now, let $e_{1},\ldots,e_{m}\in D$ be pairwise distinct so that

$\\{\mathcal{K}(e_{1}),\ldots,\mathcal{K}(e_{m})\\}=\mbox{$\\{\,\mathcal{K}(d^{(\kappa)}_{\sigma_{\kappa}})\mid
1\leq\sigma_{\kappa}\leq r_{\kappa}\wedge 1\leq\kappa\leq n\,\\}$}.$

Moreover, set

$\mathbb{M}_{\iota}:=\bigcup\mbox{$\\{\,\mathop{\mathstrut\rm
pr}\nolimits^{(r_{\kappa})}_{\sigma_{\kappa}}[\mathbb{K}_{\kappa}]\mid\mathcal{K}(d^{(\kappa)}_{\sigma_{\kappa}})=\mathcal{K}(e_{\iota})\wedge
1\leq\sigma_{\kappa}\leq r_{\kappa}\wedge 1\leq\kappa\leq n\,\\}$},$

for $1\leq\iota\leq m$. Then

$\bigcup_{\kappa=1}^{n}\bigcup_{{\sigma_{\kappa}}=1}^{r_{\kappa}}\mathcal{K}(d^{(\kappa)}_{\sigma_{\kappa}})[\mathop{\mathstrut\rm
pr}\nolimits^{({r_{\kappa}})}_{\sigma_{\kappa}}[\mathbb{K}_{\kappa}]]=\bigcup_{\iota=1}^{m}\mathcal{K}(e_{\iota})[\mathbb{M}_{\iota}]=[\mathcal{K}(e_{1}),\ldots,\mathcal{K}(e_{m})](\mathbb{M}_{1},\ldots,\mathbb{M}_{m}).$

Let us summarise what we have just seen.

######  Lemma 12.1.

Let $(X,D)$ be an IFS. Then, given
$[[d^{(1)}_{1},\ldots,d^{(1)}_{r_{1}}],\ldots,[d^{(n)}_{1},\ldots,d^{(n)}_{r_{n}}]]\in\mathcal{K}^{2}(D)$,
we can compute $e_{1},\ldots,e_{m}\in D$ so that when given in addition
$\mathbb{K}_{1},\ldots,\mathbb{K}_{n}\in\mathcal{K}^{2}(X)$, we can
furthermore define $\mathbb{M}_{1},\ldots,\mathbb{M}_{m}\in\mathcal{K}^{2}(X)$
such that

$\bigcup[[d^{(1)}_{1},\ldots,d^{(1)}_{r_{1}}],\ldots,[d^{(n)}_{1},\ldots,d^{(n)}_{r_{n}}]](\mathbb{K}_{1},\ldots,\mathbb{K}_{n})=\bigcup[\mathcal{K}(e_{1}),\ldots,\mathcal{K}(e_{m})](\mathbb{M}_{1},\ldots,\mathbb{M}_{m}).$

This gives us a hint on how to deal with unions over compact collections of
compact sets.

For $\mathbb{K},\mathbb{M}\in\mathcal{K}^{2}(X)$, we write
$\mathbb{K}\mathbin{\overset{\cup}{=}}\mathbb{M}$, , if

$\bigcup\mathbb{K}=\bigcup\mathbb{M}.$

Moreover, we set $\mathcal{K}_{D}:=\mbox{$\\{\,\mathcal{K}(d)\mid d\in
D\,\\}$}$. Note that $(\mathcal{K}^{2}(X),\mathcal{K}(\mathcal{K}_{D}))$ is a
compact IFS, and let

$\begin{split}\Omega^{\langle
2\rangle}_{X}(\mathcal{Z}):=\\{\,\mathbb{K}\in\mathcal{K}^{2}(X)\mid(\exists
d_{1},\ldots,d_{s}\in D)\hskip 142.26378pt\\\
(\exists\mathbb{M}_{1},\ldots,M_{m}\in\mathcal{Z})\,\mathbb{K}\mathbin{\overset{\cup}{=}}[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})](\mathbb{M}_{1},\ldots,\mathbb{M}_{s})\,\\},\end{split}$

for $\mathcal{Z}\subseteq\mathcal{K}^{2}(X)$. We define
$\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}:=\nu\Omega^{\langle 2\rangle}_{X}$.

######  Lemma 12.2.

Let $(X,D)$ be a compact covering IFS. Then
$\mathcal{K}^{2}(X)=\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}$.

###### Proof.

We have that
$\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}\subseteq\mathcal{K}^{2}(X)$ by
definition. For the converse inclusion note that it follows as in the proof of
Proposition 9.2(1) that

$\mathcal{K}^{2}(X)=\bigcup\mbox{$\\{\,\mathop{\mathstrut\rm
range}(\bar{d})\mid\bar{d}\in\mathcal{K}^{2}(D)\,\\}$}.$

Therefore, if $\mathbb{K}\in\mathcal{K}^{2}(X)$, then there is some
$[[d^{(1)}_{1},\ldots,d^{(1)}_{r_{1}}],\ldots,[d^{(n)}_{1},\ldots,d^{(n)}_{r_{n}}]]\in\mathcal{K}^{2}(D)$
and there are $\mathbb{K}_{1},\ldots,\mathbb{K}_{n}\in\mathcal{K}^{2}(X)$ so
that
$\mathbb{K}=[[d^{(1)}_{1},\ldots,d^{(1)}_{r_{1}}],\ldots,[d^{(n)}_{1},\ldots,d^{(n)}_{r_{n}}]](\mathbb{K}_{1},\ldots,\mathbb{K}_{n})$.
Because of Lemma 12.1 we can now compute $e_{1},\ldots,e_{m}\in D$ and define
$\mathbb{M}_{1},\ldots,\mathbb{M}_{m}\in\mathcal{K}^{2}(X)$ so that
$\mathbb{K}\mathbin{\overset{\cup}{=}}[\mathcal{K}(e_{1}),\ldots,\mathcal{K}(e_{m})](\mathbb{M}_{1},\ldots,\mathbb{M}_{m})$.
Thus, $\mathbb{K}\in\Omega_{X}^{\langle 2\rangle}(\mathcal{K}^{2}(X))$. With
co-induction it follows that
$\mathcal{K}^{2}(X)\subseteq\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}$. ∎

Let $d_{1},\ldots,s_{s}\in D$ and note that

$\begin{split}\bigcup[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})](\mathbb{M}_{1},\ldots,\mathbb{M}_{s})&=\bigcup\bigcup_{\kappa=1}^{s}\mathcal{K}(d_{\kappa})[\mathbb{M}_{\kappa}]\\\
&=\bigcup_{\kappa=1}^{s}\bigcup_{M\in\mathbb{M}_{\kappa}}\mathcal{K}(d_{\kappa})(M)\\\
&=\bigcup_{\kappa=1}^{s}\bigcup_{M\in\mathbb{M}_{\kappa}}d_{\kappa}[M]\\\
&=\bigcup_{\kappa=1}^{s}d_{\kappa}[\bigcup\mathbb{M}_{\kappa}]\\\
&=[d_{1},\ldots,d_{s}](\bigcup\mathbb{M}_{1},\ldots,\bigcup\mathbb{M}_{s}).\end{split}$
(15)

It follows that $[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})]$ respects
$\mathbin{\overset{\cup}{=}}$ and can hence be lifted to the quotient
$\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}$. We denote the lifted map by
$[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})]^{*}$ and set

$\mathcal{K}^{*}(\mathcal{K}_{D}):=\\{\,[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})]^{*}\mid
s>0\wedge d_{1},\ldots,d_{s}\in D\,\\}.$

######  Lemma 12.3.

Let $(X,D)$ be a compact covering IFS. Then also
$(\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}},\mathcal{K}^{*}(\mathcal{K}_{D}))$
is a compact covering IFS. Moreover,
$\mathbb{C}_{\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}}=\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}/\mathbin{\overset{\cup}{=}}$.

###### Proof.

$\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}$ is a topological space with
the quotient topology. Since $\bigcup\\{K\\}=K$, for every
$K\in\mathcal{K}(X)$,
$\bigcup\colon\mathcal{K}^{2}(X)\rightarrow\mathcal{K}(X)$ is an onto map,
which is well known, to be continuous [20, Corollary 7.2.4]. Since $X$ is
compact, also $\mathcal{K}(X)$, $\mathcal{K}^{2}(X)$ and
$\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}$ are compact. Moreover,
$\mathcal{K}(X)$ and $\mathcal{K}^{2}(X)$ are Hausdorff spaces. Thus,
$\bigcup$ is a closed mapping and, as a consequence, the Vietoris topology on
$\mathcal{K}(X)$ is equivalent to the quotient topology with respect to
$\bigcup$ [30, Theorem 9.2]. It follows that the quotient topology on
$\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}$ is Hausdorff.

By Lemma 12.1,
$(\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}},\mathcal{K}^{*}(\mathcal{K}_{D}))$
is covering. The remaining statement follows with co-induction.

Let
$\mathbb{K}\in\mathbb{C}_{\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}}$.
Then there are $d_{1},\ldots,d_{s}\in D$ and
$\mathbb{M}_{1},\ldots,\mathbb{M}_{s}\in\mathcal{K}^{2}(X)$, so that

$[\mathbb{K}]_{\mathbin{\overset{\cup}{=}}}=[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})]^{*}([\mathbb{M}_{1}]_{\mathbin{\overset{\cup}{=}}},\ldots,[\mathbb{M}_{s}]_{\mathbin{\overset{\cup}{=}}})=[[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})](\mathbb{M}_{1},\ldots,\mathbb{M}_{s})]_{\mathbin{\overset{\cup}{=}}}.$

Hence,
$\mathbb{K}\mathbin{\overset{\cup}{=}}[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})](\mathbb{M}_{1},\ldots,\mathbb{M}_{s})$,
which shows that
$\mathbb{C}_{\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}}\subseteq\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}/\mathbin{\overset{\cup}{=}}$.
The converse inclusion follows similarly. ∎

Assume that
$(\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}},\mathcal{K}^{*}(\mathcal{K}_{D}))$
is weakly hyperbolic. Then it follows that from each
$\mathcal{K}^{*}(\mathcal{K}_{D})$-tree representing an equivalence class in
$\mathcal{K}^{2}(X)/\mathbin{\overset{\cup}{=}}$ one obtains a
$\mathcal{K}(\mathcal{K}_{D})$-tree representing the same class by stripping
off the ‘$*$’ decoration. This also shows that
$\mathcal{K}(\mathcal{K}_{D})$-trees witnessing that
$\mathbb{K}\in\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}$ do not only represent
$\mathbb{K}$ but all sets in the $\mathbin{\overset{\cup}{=}}$-equivalence
class of $\mathbb{K}$. Such multi-representations are also common in
Weihrauch’s Type-Two Theory of Effectivity.

######  Proposition 12.4.

Let $(X,D)$ be a compact covering IFS. Then
$\mbox{$\\{\,\bigcup\mathbb{K}\mid\mathbb{K}\in\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}\,\\}$}\subseteq\mathbb{C}_{\mathcal{K}(X)}$.

###### Proof.

Let $\mathbb{K}\in\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}$. Then there are
(constructively) $d_{1},\ldots,d_{s}\in D$ and
$\mathbb{M}_{1},\ldots,\mathbb{M}_{s}\in\mathbb{C}^{\prime}_{\mathbb{K}^{2}(X)}$
so that

$\bigcup\mathbb{K}=\bigcup[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})](\mathbb{M}_{1},\ldots,\mathbb{M}_{s})=[d_{1},\ldots,d_{s}](\bigcup\mathbb{M}_{1},\ldots,\bigcup\mathbb{M}_{s}),$

where the last equality holds by (15). It follows that

$\mbox{$\\{\,\bigcup\mathbb{K}\mid\mathbb{K}\in\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}\,\\}$}\subseteq\Omega_{\mathcal{K}(X)}(\mbox{$\\{\,\bigcup\mathbb{K}\mid\mathbb{K}\in\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}\,\\}$}).$

With co-induction we therefore obtain that
$\mbox{$\\{\,\bigcup\mathbb{K}\mid\mathbb{K}\in\mathbb{C}^{\prime}_{\mathcal{K}^{2}(X)}\,\\}$}\subseteq\mathbb{C}_{\mathcal{K}(X)}$.
∎

This is a constructive version of Michael’s Theorem: If all IFS involved are
weakly hyperbolic, given a $\mathcal{K}_{D}$-tree representing $\mathbb{K}$ we
can compute a $\mathcal{K}(D)$-tree representing $\bigcup\mathbb{K}$.

The next results even allows the extraction of an algorithm for the
computation of union as an operation from $\mathcal{K}^{2}(X)$ to
$\mathcal{K}(X)$.

######  Theorem 12.5.

Let $(X,D)$ be a compact covering IFS. Then
$\bigcup\in\mathbb{C}_{\mathbb{F}(\mathcal{K}^{2}(X),\mathcal{K}(X))}$.

###### Proof.

We again use co-induction and show that
$\\{\bigcup\\}\subseteq\mathcal{J}^{\mathcal{K}^{2}(X),\mathcal{K}(X)}(\\{\bigcup\\})$.
Let to this end $d_{1},\ldots,d_{s}\in D$. As we have seen in the preceding
proof,

$[d_{1},\ldots,d_{s}]\circ(\bigcup\times\cdots\times\bigcup)=\bigcup\circ[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})].$

By Rule (W) for $\mathcal{J}^{\mathcal{K}^{2}(X),\mathcal{K}(X)}$ we have for
all $d_{1},\ldots,d_{s}\in D$ that
$[d_{1},\ldots,d_{s}]\circ(\bigcup\times\cdots\times\bigcup)\in\mathcal{J}^{\mathcal{K}^{2}(X),\mathcal{K}(X)}(\\{\bigcup\\})$.
Thus,
$\bigcup\circ[\mathcal{K}(d_{1}),\ldots,\mathcal{K}(d_{s})]\in\mathcal{J}^{\mathcal{K}^{2}(X),\mathcal{K}(X)}(\\{\bigcup\\})$,
for all $d_{1},\ldots,d_{s}\in D$, from which it follows with Rule (R) that
$\bigcup\in\mathcal{J}^{\mathcal{K}^{2}(X),\mathcal{K}(X)}(\\{\bigcup\\})$. ∎

##  13 Conclusion

In this paper, a uniform framework for computing with infinite objects like
real numbers, compact sets, tuples of such, and uniformly continuous maps is
presented. It combines and extends the approaches developed in a series of
papers by Berger and co-authors [5, 6, 8, 9, 11]. In particular, it allows to
deal with compact-valued maps and their selection functions. Maps of this kind
abundantly occur in applied mathematics. They are studied in set-valued
analysis [2, 3], and have applications in areas such as optimal control and
mathematical economics, to mention a few. In addition, they are used to model
non-determinism.

The framework is based on covering extended iterated function systems, where
the underlying spaces are compact metric spaces and the contraction maps in
the function systems are allowed to be multi-ary, or, more generally, weakly
hyperbolic compact covering extended iterated function systems operating on
Hausdorff spaces with, not necessarily unary, maps in the function system.
Because of the covering condition co-inductive characterisations of the
functions systems can be given. Results with computational content are then
derived by constructively reasoning on the basis of these characterisations.
Realisability facilitates the extraction of algorithms from the corresponding
proofs. In so doing, points of the spaces are represented by finitely
branching infinite trees. The computational power of the approach is that of
Type-Two Theory of Effectivity.

## Acknowledgement

The author is grateful to the anonymous referees for their careful reading of
the manuscript and valuable comments helping to improve the paper.

## References

  * [1] J Adámek, S Milius, L Moss, _Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors_ , Manuscript, 2019.
  * [2] J-P Aubin, A Cellina, _Differential Inclusions, Set-Valued Maps and Viability Theory_ , Springer, Berlin, 1984.
  * [3] J-P Aubin, H Frankowska, _Set-Valued Analysis_ , Birkhäuser, Basel, 1990.
  * [4] M F Barnsley, D C Wilson, K Leśnik, Some recent progress concerning topology of fractals, in K P Hard et al., editors, _Recent Progress in General Topology III_ , Atlantis Press, 2014, doi: 10.2991/978-94-6239-024-9.
  * [5] U Berger, Realisability for induction and coinduction with applications to constructive analysis, _Journal of Universal Computer Science_ 16 (18) (2010) 2535–2555.
  * [6] U Berger, From coinductive proofs to exact real arithmetic: theory and applications, _Logical Methods in Computer Science_ 7(1) (2011) 1–24, doi: 10.2168/LMCS7(1:8)2011.
  * [7] U Berger, Unpublished notes, 2017.
  * [8] U Berger, T Hou, Coinduction for exact real number computation, _Theory of Computing Systems_ 43 (2008) 394–409, doi: 10.1007.s0022400790176.
  * [9] U Berger, M Seisenberger, Proofs, programs, processes, in F Ferreira, B Löwe, E Mayordomo, L M Gomes, editors, _Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010_ , Ponta Delgada, Azores, Portugal, Springer-Verlag, Berlin, 2010, pages 39–48.
  * [10] U Berger, M Seisenberger, Proofs, programs, processes, _Theory of Computing Systems_ 51 (2012) 313–329; doi: 10.1007/s00224-011-9325-8.
  * [11] U Berger, D Spreen, A coinductive approach to computing with compact sets, _Journal Logic & Analysis_ 8 (3) (2016) 1–35, doi: 10.4115/jla.2016.8.3.
  * [12] U Berger, H Tsuiki, Intuitionistic fixed point logic, _Annals Pure Applied Logic_ 172 (3) (2021), doi.org/10.1016/j.apal.2020.102903.
  * [13] V Brattka, G Presser, Computability on subsets of metric spaces, _Theoretical Computer Science_ 305 (2003) 43–76, doi: 10.1016/S0304-3975(02)00693-X.
  * [14] A Ciaffaglione, P Di Gianantonio, A certified, corecursive implementation of exact real numbers, _Theoretical Computer Science_ 351 (2006) 39–51; doi: 10.1016/ j.tcs.2005.09.061.
  * [15] A Edalat, Power domains and iterated function systems, _Information and Computation_ 124 (1996) 182–197.
  * [16] A Edalat, R Heckmann, Computing with real numbers: I. The LFT approach to real number computation; II. A domain framework for computational geometry, in G Barthe, P Dybjer, L Pinto, J Saraiva, editors, _Applied Semantics — Lecture Notes from the International Summer School_ , Caminha, Portugal, Springer-Verlag, Berlin, 2002, pages 193–267, doi: 10.1007/35404569965.
  * [17] A Edalat, P Sünderhauf, A domain-theoretic approach to real number computation, _Theoretical Computer Science_ 210 (1998) 73–98, doi: 10.1016/S03043975(98)000978.
  * [18] R Engelking, _General Topology_ , revised and completed ed., Heldermann Verlag, Berlin, 1989.
  * [19] J E Hutchinson, Fractals and self-similarity, _Indiana University Mathematics J_ 30 (5) (1981) 713–747.
  * [20] E Klein, A C Thompson, _Theory of Correspondences: Including Applications to Mathematical Economics_ , Wiley, New York, 1984.
  * [21] J R Marcial-Romero, M Hötzel Escardó, Semantics of a sequential language for exact real number computation, _Theoretical Computer Science_ 379(12) (2007) 120–141, doi: 10.1016/j.tcs.2007.01.021.
  * [22] A Kameyama, Distances on topological self-similar sets and the kneading determinants, _Journal of Mathematics of Kyoto University_ 40 (4) (2000) 603–674.
  * [23] E Michael, Topologies on spaces of subsets, _Transactions American Mathematical Society_ 71 (1951) 152–182.
  * [24] J R Munkres, _Topology_ , 2nd ed., Prentice Hall, Upper Saddle River, NJ, 2000.
  * [25] J J M M Rutten, Universal coalgebra: a theory of systems, _Theoretical Computer Science_ 249 (2000) 3–80.
  * [26] H Schwichtenberg, S S Wainer, _Proofs and computations_ , Cambridge University Press, Cambridge, 2012.
  * [27] A Scriven, A functional algorithm for exact real integration with invariant measures _Electronic Notes in Theoretical Computer Science_ 218 (2008) 337–353.
  * [28] H Tsuiki, Real number computation through Gray code embedding, _Theoretical Computer Science_ 284(2) (2002) 467–485.
  * [29] K Weihrauch, _Computable Analysis_ , SpringerVerlag, Berlin, 2000, doi: 10.1007/ 9783642569999.
  * [30] S Willard, _General Topology_ , Addison-Wesley, Reading, MA, 1970.