Skip to main content

Posts about Functions

Challenge 7: The composition of injective functions is injective

Prove that the composition of injective functions is injective.

To do so, complete the following Lean 4 theory:

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by sorry

Read more…