diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-09 00:24:58 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2025-07-09 00:24:58 +0200 |
| commit | dc2acaa4c6b29352e3b8a8a3de54602cf9fe018a (patch) | |
| tree | 2322ae4297cd2985ee8d9380a0940138d70067df /library | |
| parent | 22e4eba441c9a2205798031b533b4e5d0e2b3054 (diff) | |
Refine `bijection_circ`
Diffstat (limited to 'library')
| -rw-r--r-- | library/function.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/function.tex b/library/function.tex index f74acbf..c7f709e 100644 --- a/library/function.tex +++ b/library/function.tex @@ -618,8 +618,8 @@ \end{proposition} \begin{proof} $g\circ f\in\surj{A}{C}$ by \cref{bijections,surjections_circ}. - $g\circ f$ is an injection. + Follows by \cref{circ_rightunique,bijections}. \end{proof} \subsection{Converse as a function} |
