summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2025-07-09 00:24:58 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2025-07-09 00:24:58 +0200
commitdc2acaa4c6b29352e3b8a8a3de54602cf9fe018a (patch)
tree2322ae4297cd2985ee8d9380a0940138d70067df /library
parent22e4eba441c9a2205798031b533b4e5d0e2b3054 (diff)
Refine `bijection_circ`
Diffstat (limited to 'library')
-rw-r--r--library/function.tex2
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}