Imagen de la intersección general

Demostrar con Lean4 que
f[iIAi]iIf[Ai]

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

1. Demostración en lenguaje natural

Sea y tal que
yf[iIA]


Tenemos que demostrar que
yiIf[A]

Para ello, sea iI, tenemos que demostrar que yf[A].

Por (1), existe un x tal que
xiIAf(x)=y


Por (2),
xA

y, por tanto,
f(x)f[A]

que, junto con (3), da que
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