Definition:Partial Function Equality

Definition

Let $g: \N^k \to \N$ and $h: \N^k \to \N$ be partial functions.

We write:

$\map g {n_1, n_2, \ldots, n_k} \approx \map h {n_1, n_2, \ldots, n_k}$

if and only if either:

both $\map g {n_1, n_2, \ldots, n_k}$ and $\map h {n_1, n_2, \ldots, n_k}$ are defined and equal

or:

neither $\map g {n_1, n_2, \ldots, n_k}$ nor $\map h {n_1, n_2, \ldots, n_k}$ are defined.

That is, if and only if $\map g {n_1, n_2, \ldots, n_k} = \map h {n_1, n_2, \ldots, n_k}$ wherever either are defined.

Thus, $g$ is equal to $h$, and we can write $g = h$, if and only if:

$\forall x \in \N^k: \map g x \approx \map h x$