Ir al contenido principal

Publicaciones sobre Funciones

Reto 7: La composición de funciones inyectivas es inyectiva

Demostrar que la composición de funciones inyectivas es inyectiva.

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

import Mathlib.Tactic

open Function

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

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

Leer más…