Composite_of_Injections_is_Injection
Provedcomposite-mappingsinjectionsproofwiki
A composite of injections is an injection. That is, if f and g are injections, then so is f ∘ g.
Preamble
import Mathlib.Logic.Function.Basic
Formal statement
theorem Composite_of_Injections_is_Injection {α β γ : Type _} {f : β → γ} {g : α → β} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (f ∘ g) := by sorrySource