La semana en Calculemus (2 de marzo de 2024)

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

A continuación se muestran las soluciones.

1. s \ (t ∪ u) ⊆ (s \ t) \ u

Demostrar con Lean4 que
\[ s \setminus (t ∪ u) ⊆ (s \setminus t) \setminus u \]

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

1. Demostración en lenguaje natural

Sea \(x ∈ s \setminus (t ∪ u)\). Entonces,
\begin{align}
&x ∈ s \tag{1} \\
&x ∉ t ∪ u \tag{2} \\
\end{align}
Tenemos que demostrar que \(x ∈ (s \setminus t) \setminus u\); es decir, que se verifican las relaciones
\begin{align}
&x ∈ s \setminus t \tag{3} \\
&x ∉ u \tag{4}
\end{align}
Para demostrar (3) tenemos que demostrar las relaciones
\begin{align}
&x ∈ s \tag{5} \\
&x ∉ t \tag{6}
\end{align}
La (5) se tiene por la (1). Para demostrar la (6), supongamos que \(x ∈ t\); entonces, \(x ∈ t ∪ u\), en contracción con (2). Para demostrar la (4), supongamos que \(x ∈ u\); entonces, \(x ∈ t ∪ u\), en contracción con (2).

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

2. s ∩ t = t ∩ s

Demostrar con Lean4 que
\[ s ∩ t = t ∩ s \]

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

1. Demostración en lenguaje natural

Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∩ t ↔ x ∈ t ∩ s] \]
Demostratemos la equivalencia por la doble implicación.

Sea \(x ∈ s ∩ t\). Entonces, se tiene
\begin{align}
&x ∈ s \tag{1} \\
&x ∈ t \tag{2}
\end{align}
Luego \(x ∈ t ∩ s\) (por (2) y (1)).

La segunda implicación se demuestra análogamente.

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

3. s ∩ (s ∪ t) = s

Demostrar con Lean4 que
\[ s ∩ (s ∪ t) = s \]

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

1. Demostración en lenguaje natural

Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∩ (s ∪ t) ↔ x ∈ s] \]
y lo haremos demostrando las dos implicaciones.

(⟹) Sea \(x ∈ s ∩ (s ∪ t)\). Entonces, \(x ∈ s\).

(⟸) Sea \(x ∈ s\). Entonces, \(x ∈ s ∪ t\) y, por tanto, \(x ∈ s ∩ (s ∪ t)\).

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

4. s ∪ (s ∩ t) = s

Demostrar con Lean4 que
\[ s ∪ (s ∩ t) = s \]

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

1. Demostración en lenguaje natural

Tenemos que demostrar que
\[ (∀ x)[x ∈ s ∪ (s ∩ t) ↔ x ∈ s] \]
y lo haremos demostrando las dos implicaciones.

(⟹) Sea \(x ∈ s ∪ (s ∩ t)\). Entonces, \(x ∈ s\) ó \(x ∈ s ∩ t\). En ambos casos, \(x ∈ s\).

(⟸) Sea \(x ∈ s\). Entonces, \(x ∈ s ∩ t\) y, por tanto, \(x ∈ s ∪ (s ∩ t)\).

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

5. (s \ t) ∪ t = s ∪ t

Demostrar con Lean4 que
\[ (s \setminus t) ∪ t = s ∪ t \]

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

1. Demostración en lenguaje natural

Tenemos que demostrar que
\[ (∀ x)[x ∈ (s \setminus t) ∪ t ↔ x ∈ s ∪ t] \]
y lo demostraremos por la siguiente cadena de equivalencias:
\begin{align}
x ∈ (s \setminus t) ∪ t
&↔ x ∈ (s \setminus t) ∨ (x ∈ t) \\
&↔ (x ∈ s ∧ x ∉ t) ∨ x ∈ t \\
&↔ (x ∈ s ∨ x ∈ t) ∧ (x ∉ t ∨ x ∈ t) \\
&↔ x ∈ s ∨ x ∈ t \\
&↔ x ∈ s ∪ t
\end{align}

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL