Una función tiene inversa si y solo si es biyectiva

En Lean se puede definir que g es una inversa de f por

y que f tiene inversa por

Demostrar que la función f tiene inversa si y solo si f es biyectiva.

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

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las funciones biyectivas tienen inversa

En Lean se puede definir que g es una inversa de f por

y que f tiene inversa por

Demostrar que si la función f es biyectiva, entonces f tiene inversa.

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

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las funciones con inversa son biyectivas

En Lean se puede definir que g es una inversa de f por

y que f tiene inversa por

Demostrar que si la función f tiene inversa, entonces f es biyectiva.

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

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Una función tiene inversa por la derecha si y solo si es suprayectiva

En Lean, que g es una inversa por la izquierda de f está definido por

que g es una inversa por la derecha de f está definido por

y que f tenga inversa por la derecha está definido por

Finalmente, que f es suprayectiva está definido por

Demostrar que la función f tiene inversa por la derecha si y solo si es suprayectiva.

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

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las funciones suprayectivas tienen inversa por la derecha

En Lean, que g es una inversa por la izquierda de f está definido por

que g es una inversa por la derecha de f está definido por

y que f tenga inversa por la derecha está definido por

Finalmente, que f es suprayectiva está definido por

Demostrar que si f es una función suprayectiva, entonces f tiene inversa por la derecha.

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

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]