Las funciones con inversa por la derecha son suprayectivas

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 la función f tiene inversa por la derecha, entonces f 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]

Una función tiene inversa por la izquierda si y solo si es inyectiva

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

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

Finalmente, que f es inyectiva está definido por

Demostrar que una función f, con dominio no vacío, tiene inversa por la izquierda si y solo si es inyectiva.

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 inyectivas tienen inversa por la izquierda

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

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

Finalmente, que f es inyectiva está definido por

Demostrar que si f es una función inyectiva con dominio no vacío, entonces f tiene inversa por la izquierda.

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 por la izquierda son inyectivas

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

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

Finalmente, que f es inyectiva está definido por

Demostrar que si f tiene inversa por la izquierda, entonces f es inyectiva.

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]

La congruencia módulo 2 es una relación de equivalencia

Se define la relación R entre los números enteros de forma que x está relacionado con y si x-y es divisible por 2. Demostrar que R es una relación de equivalencia.

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]