Si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva
Demostrar que si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 |
import tactic open function variables {A : Type*} {B : Type*} {C : Type*} variables {f : A → B} {g : B → C} example (hg : injective g) (hf : injective f) : injective (g ∘ f) := sorry |
Read More «Si f: A → B y g: B → C son inyectiva, entonces g ∘ f es inyectiva»