Imagen de la unión general

Demostrar con Lean4 que
f[A]=f[A]

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

1. Demostración en lenguaje natural

Tenemos que demostrar que, para todo y,
yf[A]yf[A]
Lo haremos demostrando las dos implicaciones.

(⟹) Supongamos que yf[A]. Entonces, existe un x tal que
xAf(x)=y
Por (1), existe un i tal que
ixA
Por (4),
f(x)f[A]
Por (3),
f(x)f[A]
y, por (2),
yf[A]

(⟸) Supongamos que yf[A]. Entonces, existe un i tal que
iyf[A]
Por (6), existe un x tal que
xAf(x)=y
Por (5) y (7),
xA
Luego,
f(x)f[A]
y, por (8),
yf[A]

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

Escribe un comentario