Theorem. Given two sets $X$ and $Y$, the functions $f:Z \rightarrow X$, $g:Z \rightarrow Y$ and the coordinate functions $\pi_{X \times Y \rightarrow X}: X \times Y \rightarrow X$ and $\pi_{X \times Y \rightarrow Y}: X \times Y \rightarrow Y$ where $\pi_{X \times Y \rightarrow X}(x, y) := x$ and $\pi_{X \times Y \rightarrow Y}(x, y) := y$, respectively. Show that there is a unique function $h:Z \rightarrow X \times Y$, such that $\pi_{X \times Y \rightarrow X} \circ h = f$ and $\pi_{X \times Y \rightarrow Y} \circ h = g$.

Proof.

The function $h$ exists since $$h = (f, g) =: f \oplus g$$ satisfies the property $$P(h) = (\pi_{X \times Y \rightarrow X} \circ h = f) \wedge (\pi_{X \times Y \rightarrow Y} \circ h = g).$$ Uniqueness of $h$ is given iff $$(\forall h') \: P(h) \wedge P(h') \rightarrow h = h'.$$ Or, equivalently, $$(\forall h') \: h \neq h' \rightarrow \neg P(h) \vee \neg P(h') .$$ Two functions $h$, $h'$ are not equal iff there is an element $z$ in the common domain such that the respective elements in the range are not equal: $$h \neq h' \leftrightarrow (\exists z \in Z) \: h(z) \neq h'(z) \leftrightarrow (h_1(z) \neq h_1'(z) \vee h_2(z) \neq h_2'(z)).$$ Given $h_1(z) \neq h_1'(z)$ we have that $$(\pi_{X \times Y \rightarrow X} \circ h')(z) \neq f(z) \rightarrow \neg P(h').$$ Accordingly, if $h_2(z) \neq h_2'(z)$ $$(\pi_{X \times Y \rightarrow Y} \circ h')(z) \neq g(z) \rightarrow \neg P(h').$$ $\Box$
2015 FEB 14 (v1.0)
Contact me: m.herrmann followed by an -at- followed by blaetterundsterne.org.

This document created with the help of MathJax (Thank you guys!)