Theorem Marketplace

Theorem Details

-- Composition of two injective functions is injective

import Mathlib.Logic.Function.Basic

theorem injective_comp {α β γ : Type} {f : β → γ} {g : α → β}
  (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (f ∘ g) := by
  intros x y h
  apply hg
  apply hf
  exact h

Bounty: 0.04 ETH

Status: Closed

Proof

-- Composition of two injective functions is injective

import Mathlib.Logic.Function.Basic

theorem injective_comp {α β γ : Type} {f : β → γ} {g : α → β}
  (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (f ∘ g) := by
  intros x y h
  apply hg
  apply hf
  exact h

Back to Bounties