Si g·f es inyectiva, entonces f es inyectiva.
Demostrar que si g·f es inyectiva, entonces f es inyectiva.
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 : injective (g ∘ f)) : injective f := sorry |