Si f es inyectiva, entonces f⁻¹[f[s]​] ⊆ s

Demostrar con Lean4 que si f es inyectiva, entonces f¹[f[s]]s.

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

1. Demostración en lenguaje natural

Sea x tal que
xf¹[f[s]]
Entonces,
f(x)f[s]
y, por tanto, existe un
ys
tal que
f(y)=f(x)
De (2), puesto que f es inyectiva, se tiene que
y=x
Finalmente, de (3) y (1), se tiene que
xs
que es lo que teníamos que demostrar.

2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Escribe un comentario