26 octubre 2023 – Calculemus

La composición de funciones inyectivas es inyectiva

PorJosé A. Alonso 26 octubre 202319 octubre 2023

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

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

import Mathlib.Tactic

open Function

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

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

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}

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

example

(hg : Injective g)

(hf : Injective f) :

Injective (g ∘ f) :=

by sorry