14 noviembre 2023 – Calculemus

La composición de funciones suprayectivas es suprayectiva

PorJosé A. Alonso 14 noviembre 20233 noviembre 2023

Demostrar con Lean4 que la composición de funciones suprayectivas es suprayectiva.

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

import Mathlib.Tactic
open Function
variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

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

import Mathlib.Tactic

open Function

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

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

example

(hg : Surjective g)

(hf : Surjective f)

: Surjective (g ∘ f) :=

by sorry