Injection_if_Composite_is_Injection
Provedcomposite-mappingsinjectionsproofwiki
Let f and g be mappings such that their composite g ∘ f is an injection. Then f is an injection.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Injection_if_Composite_is_Injection {α β γ : Type _} {f : α → β} {g : β → γ} (h : Function.Injective (g ∘ f)) : Function.Injective f := by sorrySource