Exercise. [dt-0035]

Liam O'Connor

Prove that the case function $[f,g](x)$ is, given continuous functions $f : A \twoheadrightarrow C$ and $g : B \twoheadrightarrow C$ , continuous on its argument $x$ .

Solution.

Liam O'Connor

As mentioned in Construction [dt-0031], the only directed subsets of $A + B$ are those that contain entirely values of the format $(0,\_)$ and optionally $\bot _{A+B}$ , or those that contain entirely values of the format $(1,\_)$ and optionally $\bot _{A+B}$ . Call this directed subset $X$ .

When $\bigsqcup X = \bot _{A+B}$ : This means that $X = \{\bot _{A+B}\}$ as $\bot$ is always the least element. From Definition [dt-0034], we have: $\begin {array}{lcl} [f,g](\bigsqcup X) &=& [f,g](\bot _{A+B}) \\ &=& \bot _C \\ &=& \bigsqcup \{\bot _C\} \\ &=& \bigsqcup \{[f,g](\bot _{A+B})\} \\ &=& \bigsqcup \{[f,g](x) \mid x \in X\}\end {array}$ This discharges both requirements in Definition [dt-001J] for this case.
When $\bigsqcup X = (0,\_)$ : This means that $X$ consists of at least one $(0,\_)$ value plus possibly $\bot _{A+B}$ , that is $X \setminus \{\bot _{A+B}\} = \{ (0,a) \mid a \in Y\}$ for some nonempty $Y \subseteq A$ . We have the following, using the continuity of $f$ : $\begin {array}{lcl} [f,g](\bigsqcup X) &=& [f,g](\bigsqcup (X \setminus \{\bot _{A+B}\})) \\ &=& [f,g](\bigsqcup \{ (0,a) \mid a \in Y\} )\\ &=& [f,g](0,\bigsqcup Y) \\ &=& f(\bigsqcup Y) \\ &=& \bigsqcup \{ f(a) \mid a \in Y \} \\ &=& \bigsqcup \{ [f,g](0,a) \mid a \in Y\} \\ &=& \bigsqcup \{ [f,g](x) \mid x \in X \setminus \{\bot _{A+B}\} \} \\ &=& \bigsqcup (\{ [f,g](x) \mid x \in X \setminus \{\bot _{A+B}\} \} \cup \{\bot _C\}) \\ &=& \bigsqcup \{ [f,g](x) \mid x \in X \} \\ \end {array}$
When $\bigsqcup X = (1,\_)$ : Similar to the $(0,\_)$ case but using $g$ rather than $f$ .

Exercise. [dt-0035]

Solution.

Definition. Constructors for sums [dt-0032]

Theorem. Continuity of sum constructors [dt-0033]

Definition. The case function [dt-0034]

Exercise. [dt-0035]

Solution.