A double downward arrow symbol serving as both a relation and delimiter in category theory and formal logic.
Examples
Logical consequence in formal logic
P \land Q \\[8pt] \Downarrow \\[8pt] Q
Double vertical arrow as delimiter in matrix notation
\left\Downarrow \begin{matrix} a_{11} & a_{12} \\ a_{21} & a_{22} \end{matrix} \right\rangle
Component-wise relation in vector inequalities
x > 0 \Downarrow y < 0 \text{ means both conditions must hold}