Commit 2021-11-23 15:06 d0e454ac
View on Github →feat(logic/function/basic): add function.{in,sur,bi}jective.comp_left (#10406)
As far as I can tell we don't have these variations.
Note that the surjective and bijective versions do not appear next to the other composition statements, as they require surj_inv to concisely prove.