Commit 2025-02-14 22:49 00c5dfd0

View on Github →

feat(Function/Basic): iff lemmas for injectivity/surjectivity of composition (#20646) in/surjective_comp_left_iff: assuming the domain of · is nonempty, (g ∘ ·) is in/surjective iff g is in/surjective_comp_right_iff_sur/injective: assuming the codomain of · is nontrivial, (· ∘ f) is in/surjective iff f is sur/injective

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

Modified Mathlib/Data/Set/Image.lean

modified theorem Function.Injective.preimage_surjective

modified theorem Set.preimage_injective

modified theorem Set.preimage_surjective

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.injective_comp_left_iff

added theorem Function.injective_comp_right_iff_surjective

added theorem Function.surjective_comp_left_iff

added theorem Function.surjective_comp_right_iff_injective