How to write the division function in arrow notation Basically the title, I'm not sure which one is formal:
$$
\begin{aligned}
division:\mathbb{R} \times \mathbb{R} &\rightarrow \mathbb{R} \cup \text{\{"impossible"\}} \\
(x,y) &\mapsto \begin{cases}
x/y,  & \text{if $y \neq 0$} \\
\text{"impossible''}, & \text{else}
\end{cases}
\end{aligned}
$$
Or
$$
\begin{aligned}
division:\mathbb{R} \times \mathbb{R}\backslash\{0\} &\rightarrow \mathbb{R} \\
(x,y) &\mapsto x/y
\end{aligned}
$$
 A: You can exclude denominators equal to zero right from the start:
$$\begin{align}
\operatorname{div}:\Bbb R \times \Bbb R_{\neq0}&\to\Bbb R \\
(x,y) &\mapsto x / y
\end{align}$$
So you know that arguments of the form $(x,0)$ are not valid, just like you already know that arguments like $(x,\mathrm{flowerpot})$ are not valid because "flowerpot" is not a valid denominator as it's not an element of $\Bbb R\!\setminus\!\{0\}$.
A: Well, in a purely mathematical context, I'd chose the second.
But you mentioned in your comment that this function is intended to be implemented in a computer program, presumably using IEEE 754 floating-point representation, so here's a slightly more apt version for that context.
Let $\mathbb{R}' = \mathbb{R} \cup \lbrace +\infty, -\infty, \text{NaN}, -0 \rbrace$.  This an extended real number line including the IEEE 754 special values.  Then:
$$\text{division}: \mathbb{R}' \times \mathbb{R}' \mapsto \mathbb{R}' \\
(x, y) \mapsto \begin{cases}
x/y & \text{if } x \in \mathbb{R} \text{ and } y \in \mathbb{R}\backslash \lbrace 0 \rbrace \\
0 & \text{if } x \in \mathbb{R} \text{ and } y \in \lbrace +\infty, -\infty \rbrace \\
+\infty & \text{if } (x > 0 \text{ and } y = +0) \text { or } (x < 0 \text{ and } y = -0) \\
+\infty & \text{if } (x = +\infty \text { and } y > 0) \text{ or } (x = -\infty \text { and } y < 0)\\
-\infty & \text{if } (x < 0 \text{ and } y = +0) \text { or } (x > 0 \text{ and } y = -0) \\
-\infty & \text{if } (x = -\infty \text { and } y > 0) \text{ or } (x = +\infty \text { and } y < 0)\\
\text{NaN} & \text{otherwise}
\end{cases}
$$
I'm probably way overthinking this, though.
A: If you want to formalize a division operation that returns a sentinel value $null$ for "no output", then you should also expand the domain of the function representing that operation to $R'=ℝ∪\{null\}$ and define $div : R'×R'→R'$ via:
  $(x,y) = x/y$ for each $x∈ℝ$ and $y∈ℝ∖\{0\}$.
  $(x,y) = null$ for each $x∈ℝ$ and $y = 0$.
  $(x,y) = null$ for each $x,y∈R'$ such that $x = null$ or $y = null$.
The first part captures the standard division. The second captures "no answer for division by zero". The third is the usual null-propagation (i.e. if an input is missing then the output is missing too).
Beware that there are tons of different meanings for "$null$" and this is just one common one that is incompatible with the meaning of null in object-oriented programming languages that support comparison between null pointers. In contrast, any semantics that has null-propagation should also stipulate that "$null=null$" evaluates to $null$. For instance, "$1/0 = 0/0$" evaluates to $null$ as desirable.
Note that the meaning of $null$ used here is compatible with the formalization of partial functions as standard functions that may map an input to $null$, and composition of these maybe-$null$ functions exactly match the composition of the original partial functions. But many logicians do not like this extra $null$ possibility, and it's usually mathematically cleaner to stick to standard functions.
