Menu Close

Día: 24 de noviembre de 2022

Si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva

Demostrar que si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva.

Para ello, completar la siguiente teoría de Lean:

import tactic
 
open function
 
variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A  B} {g : B  C}
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g  f) :=
sorry