Si r ⊆ s y s ⊆ t, entonces r ⊆ t

Demostrar con Lean4 que si rs y st, entonces rt.

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

Demostración en lenguaje natural


1ª demostración en LN

Tenemos que demostrar que
(x)[xrxt]


Sea x tal que
xr

Puesto que rs, se tiene que
xs

y, puesto que \(s ⊆ t), se tiene que
xt

que es lo que teníamos que demostrar.

2ª demostración en LN

Tenemos que demostrar que
(x)[xrxt]


Sea x tal que
xr

Tenemos que demostrar que
xt

que, puesto que st, se reduce a
xs

que, puesto que rs, se redece a
xr

que es lo que hemos supuesto.

Demostraciones con Lean4

Demostraciones interactivas

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

Referencias

Escribe un comentario