Si g·f es suprayectiva, entonces g es suprayectiva
Demostrar que si g·f es suprayectiva, entonces g es suprayectiva.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 |
import tactic open function variables {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} example (Hgf : surjective (g ∘ f)) : surjective g := sorry |
Read More «Si g·f es suprayectiva, entonces g es suprayectiva»