Constant Function of Computable Real Number is Sequentially Computable

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $c \in \R$ be a computable real number.

Then, $f : \R^n \to \R$, defined as:

$\map f \bsx = c$

is sequentially computable.


Proof

For any real sequence $\sequence {x_n}$, we have:

$\sequence {\map f {x_n}} = \sequence c$

Thus, the result follows from Constant Sequence of Computable Real Number is Computable.

$\blacksquare$