Let $R$ be a binary relation. The converse of $R$ is the relation
\[R^{-1} = \{(y,x):(x,y)\in R\}.\]This is a set:
\[R^{-1} \subseteq \ran R\times\dom R.\]
For any binary relation $R$,
\[(R^{-1})^{-1} = R.\]
A binary relation $R$ is symmetric if and only if
\[R = R^{-1}.\]
If $A$ and $B$ are finite and $f:A\to B$ is a surjection, then
\[\lvert A\rvert = \sum_{b\in B}\big\lvert f^{-1}[\{b\}]\big\rvert.\]
Proof.Since $f$ is a function,
\[A = \bigsqcup_{b\in B}f^{-1}[\{b\}].\]
PROP-CV-FC-C. Corollary of PROP-CV-FC
If $A$ and $B$ are finite and $f:A\to B$ is a surjection such that for every $b\in B$,
\[\big\lvert f^{-1}[\{b\}]\big\rvert = k,\]then
\[\lvert A\rvert = k\lvert B\rvert.\]