La semana en Calculemus (21 de abril de 2024)

Desde el 18 de marzo, he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:

A continuación se muestran las soluciones.

1. 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.1. Demostración en lenguaje natural

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

1.2. Demostraciones con Lean4

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

1.3. Demostraciones con Isabelle/HOL

2. f[f⁻¹[u]] ⊆ u

Demostrar con Lean4 que
\[ f[f⁻¹[u]] ⊆ u \]

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

2.1. Demostración en lenguaje natural

Sea \(y ∈ f[f⁻¹[u]]\). Entonces existe un \(x\) tal que
\begin{align}
&x ∈ f⁻¹[u] \tag{1} \\
&f(x) = y \tag{2}
\end{align}
Por (1),
\[ f(x) ∈ u \]
y, por (2),
\[ y ∈ u \]

2.2. Demostraciones con Lean4

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

2.3. Demostraciones con Isabelle/HOL

3. Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]]

Demostrar con Lean4 que si \(f\) es suprayectiva, entonces
\[ u ⊆ f[f⁻¹[u]] \]

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

3.1. Demostración en lenguaje natural

Sea \(y ∈ u\). Por ser \(f\) suprayectiva, exite un \(x\) tal que
\[ f(x) = y \tag{1} \]
Por tanto, \(x ∈ f⁻¹[u]\) y
\[ f(x) ∈ f[f⁻¹[u]] \tag{2} \]
Finalmente, por (1) y (2),
\[ y ∈ f[f⁻¹[u]] \]

3.2. Demostraciones con Lean4

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

3.3. Demostraciones con Isabelle/HOL

4. Si s ⊆ t, entonces f[s] ⊆ f[t]

Demostrar con Lean4 que si \(s ⊆ t\), entonces \(f[s] ⊆ f[t]\).

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

4.1. Demostración en lenguaje natural

Sea \(y ∈ f[s]\). Entonces, existe un x tal que
\begin{align}
&x ∈ s \tag{1} \\
&f(x) = y \tag{2}
\end{align}
Por (1) y la hipótesis,
\[ x ∈ t \tag{3} \]
Por (3),
\[ f(x) ∈ f[t] \tag{4} \]
y, por (2) y (4),
\[ y ∈ f[t] \]

4.2. Demostraciones con Lean4

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

4.3. Demostraciones con Isabelle/HOL

5. Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]

Demostrar con Lean4 que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\).

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

5.1. Demostración en lenguaje natural

Por la siguiente cadena de implicaciones:
\begin{align}
x ∈ f⁻¹[u] &⟹ f(x) ∈ u \\
&⟹ f(x) ∈ v &&\text{[porque \(u ⊆ v\)]} \\
&⟹ x ∈ f⁻¹[v]
\end{align}

5.2. Demostraciones con Lean4

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

5.3. Demostraciones con Isabelle/HOL

6. f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]

Demostrar con Lean4 que \(f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]\).

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

6.1. Demostración en lenguaje natural

Tenemos que demostrar que, para todo \(x\),
\[ x ∈ f⁻¹[A ∪ B] ↔ x ∈ f⁻¹[A] ∪ f⁻¹[B] \]
Lo haremos demostrando las dos implicaciones.

(⟹) Supongamos que \(x ∈ f⁻¹[A ∪ B]\). Entonces, \(f(x) ∈ A ∪ B\).
Distinguimos dos casos:

Caso 1: Supongamos que \(f(x) ∈ A\). Entonces, \(x ∈ f⁻¹[A]\) y, por tanto,
\(x ∈ f⁻¹[A] ∪ f⁻¹[B]\).

Caso 2: Supongamos que \(f(x) ∈ B\). Entonces, \(x ∈ f⁻¹[B]\) y, por tanto,
\(x ∈ f⁻¹[A] ∪ f⁻¹[B]\).

(⟸) Supongamos que \(x ∈ f⁻¹[A] ∪ f⁻¹[B]\). Distinguimos dos casos.

Caso 1: Supongamos que \(x ∈ f⁻¹[A]\). Entonces, \(f(x) ∈ A\) y, por tanto,
\(f(x) ∈ A ∪ B\). Luego, \(x ∈ f⁻¹[A ∪ B]\).

Caso 2: Supongamos que \(x ∈ f⁻¹[B]\). Entonces, \(f(x) ∈ B\) y, por tanto,
\(f(x) ∈ A ∪ B\). Luego, \(x ∈ f⁻¹[A ∪ B]\).

6.2. Demostraciones con Lean4

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

6.3. Demostraciones con Isabelle/HOL

7. f[s ∩ t] ⊆ f[s] ∩ f[t]

Demostrar con Lean4 que
\[ f[s ∩ t] ⊆ f[s] ∩ f[t]​ \]

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

7.1. Demostración en lenguaje natural

Sea tal que
\[ y ∈ f[s ∩ t] \]
Por tanto, existe un \(x\) tal que
\begin{align}
x ∈ s ∩ t \tag{1} \\
f(x) = y \tag{2}
\end{align}
Por (1), se tiene que
\begin{align}
x ∈ s \tag{3} \\
x ∈ t \tag{4}
\end{align}
Por (2) y (3), se tiene
\[ y ∈ f[s] \tag{5} \]
Por (2) y (4), se tiene
\[ y ∈ f[t] \tag{6} \]
Por (5) y (6), se tiene
\[ y ∈ f[s] ∩ f[t] \]

7.2. Demostraciones con Lean4

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

6.3. Demostraciones con Isabelle/HOL

8. Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]

Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\[ f[s] ∩ f[t] ⊆ f[s ∩ t] \]

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

8.1. Demostración en lenguaje natural

Sea \(y ∈ f[s] ∩ f[t]\). Entonces, existen \(x₁\) y \(x₂\) tales que
\begin{align}
&x₁ ∈ s \tag{1} \\
&f(x₁) = y \tag{2} \\
&x₂ ∈ t \tag{3} \\
&f(x₂) = y \tag{4}
\end{align}
De (2) y (4) se tiene que
\[ f(x₁) = f(x₂) \]
y, por ser \(f\) inyectiva, se tiene que
\[ x₁ = x₂ \]
y, por (1), se tiene que
\[ x₂ ∈ t \]
y, por (3), se tiene que
\[ x₂ ∈ s ∩ t \]
Por tanto,
\[ f(x₂) ∈ f[s ∩ t] \]
y, por (4),
\[ y ∈ f[s ∩ t] \]

8.2. Demostraciones con Lean4

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

8.3. Demostraciones con Isabelle/HOL

9. f[s] \ f[t] ⊆ f[s \ t]

Demostrar con Lean4 que
\[f[s] \setminus f[t] ⊆ f[s \setminus t] \]

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

9.1. Demostración en lenguaje natural

Sea \(y ∈ f[s] \setminus f[t]\). Entonces,
\begin{align}
&y ∈ f[s] \tag{1} \\
&y ∉ f[t] \tag{2}
\end{align}
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ s \tag{3} \\
&f(x) = y \tag{4}
\end{align}
Por tanto, para demostrar que \(y ∈ f[s \setminus t]\), basta probar que \(x ∉ t\). Para ello, supongamos que \(x ∈ t\). Entonces, por (4), \(y ∈ f[t]\), en contradicción con (2).

9.2. Demostraciones con Lean4

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

9.3. Demostraciones con Isabelle/HOL

10. f[s] ∩ t = f[s ∩ f⁻¹[t]]

Demostrar con Lean4 que
\[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]

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

10.1. Demostración en lenguaje natural

Tenemos que demostrar que, para toda \(y\),
\[ y ∈ f[s] ∩ t ↔ y ∈ f[s ∩ f⁻¹[t]] \]
Lo haremos probando las dos implicaciones.

(⟹) Supongamos que \(y ∈ f[s] ∩ t\). Entonces, se tiene que
\begin{align}
&y ∈ f[s] \tag{1} \\
&y ∈ t \tag{2}
\end{align}
Por (1), existe un \(x\) tal que
\begin{align}
&x ∈ s \tag{3} \\
&f(x) = y \tag{4}
\end{align}
Por (2) y (4),
\[ f(x) ∈ t \]
y, por tanto,
\[ x ∈ f⁻¹[t] \]
que, junto con (3), da
\{ x ∈ s ∩ f⁻¹[t] \]
y, por tanto,
\[ f(x) ∈ f[s ∩ f⁻¹[t]] \]
que, junto con (4), da
\[ y ∈ f[s ∩ f⁻¹[t]] \]

(⟸) Supongamos que \(y ∈ f[s ∩ f⁻¹[t]]\). Entonces, existe un \(x\) tal que
\begin{align}
&x ∈ s ∩ f⁻¹[t] \tag{5} \\
&f(x) = y \tag{6}
\end{align}
Por (1), se tiene que
\begin{align}
&x ∈ s \tag{7} \\
&x ∈ f⁻¹[t] \tag{8}
\end{align}
Por (7) se tiene que
\[ f(x) ∈ f[s] \]
y, junto con (6), se tiene que
\[ y ∈ f[s] \tag{9} \]
Por (8), se tiene que
\[ f(x) ∈ t \]
y, junto con (6), se tiene que
\[ y ∈ t \tag{10} \]
Por (9) y (19), se tiene que
\[ y ∈ f[s] ∩ t \]

10.2. Demostraciones con Lean4

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

10.3. Demostraciones con Isabelle/HOL