Theorem Function.surjective_comp_right_iff_injective

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_right_iff_injectiveView on Github →