Theorem Function.surjective_comp_left_iff

Modification history

2025-02-14 22:49
Mathlib/Logic/Function/Basic.lean
feat(Function/Basic): iff lemmas for injectivity/surjectivity of composition (#20646) …
Added Function.surjective_comp_left_iffView on Github →