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:

Soluciones con Lean

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

Soluciones con Isabelle/HOL

Escribe un comentario