La semana en Calculemus (25 de mayo de 2024)

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

A continuación se muestran las soluciones.

1. Los monoides booleanos son conmutativos

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide \(M\) es booleano si
\[ (∀ x ∈ M)[x·x = 1] \]
y es conmutativo si
\[ (∀ x, y ∈ M)[x·y = y·x] \]

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

Demostrar con Lean4 que los monoides booleanos son conmutativos.

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

1.1. Demostración en lenguaje natural

Sean \(a, b ∈ M\). Se verifica la siguiente cadena de igualdades
\begin{align}
a·b &= (a·b)·1 &&\text{[por mul_one]} \\
&= (a·b)·(a·a) &&\text{[por hipótesis, \(a·a = 1\)]} \\
&= ((a·b)·a)·a &&\text{[por mul_assoc]} \\
&= (a·(b·a))·a &&\text{[por mul_assoc]} \\
&= (1·(a·(b·a)))·a &&\text{[por one_mul]} \\
&= ((b·b)·(a·(b·a)))·a &&\text{[por hipótesis, \(b·b = 1\)]} \\
&= (b·(b·(a·(b·a))))·a &&\text{[por mul_assoc]} \\
&= (b·((b·a)·(b·a)))·a &&\text{[por mul_assoc]} \\
&= (b·1)·a &&\text{[por hipótesis, \((b·a)·(b·a) = 1\)]} \\
&= b·a &&\text{[por mul_one]}
\end{align}

1.2. Demostraciones con Lean4

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

1.3. Demostraciones con Isabelle/HOL

2. La composición de una función creciente y una decreciente es decreciente

Sea una función \(f\) de \(ℝ\) en \(ℝ\). Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\). Se dice que \(f\) es decreciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≥ f(y)\).

Demostrar con Lean4 que si \(f\) es creciente y \(g\) es decreciente, entonces \(g ∘ f\) es decreciente.

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

2.1. Demostración en lenguaje natural

Sean \(x, y ∈ ℝ\) tales que \(x ≤ y\). Entonces, por ser \(f\) creciente,
\[ f(x) ≥ f(y) \]
y, por ser g decreciente,
\[ g(f(x)) ≤ g(f(y)) \]
Por tanto,
\[ (g ∘ f)(x) ≤ (g ∘ f)(y) \]

2.2. Demostraciones con Lean4

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

2.3. Demostraciones con Isabelle/HOL

3. Si una función es creciente e involutiva, entonces es la identidad

Sea una función \(f\) de \(ℝ\) en \(ℝ\).

  • Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\).
  • Se dice que \(f\) es involutiva si para todo \(x\) se tiene que \(f(f(x)) = x\).

En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f

Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.

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

3.1. Demostración en lenguaje natural

Tenemos que demostrar que para todo \(x ∈ ℝ\), \(f(x) = x\). Sea \(x ∈ ℝ\). Entonces, por ser \(f\) involutiva, se tiene que
\[ f(f(x)) = x \tag{1} \]
Además, por las propiedades del orden, se tiene que \(f(x) ≤ x\) ó \(x ≤ f(x)\). Demostraremos que \(f(x) = x\) en los dos casos.

Caso 1: Supongamos que
\[ f(x) ≤ x \tag{2} \]
Entonces, por ser \(f\) creciente, se tiene que
\[ f(f(x)) ≤ f(x) \tag{3} \]
Sustituyendo (1) en (3), se tiene
\[ x ≤ f(x) \]
que junto con (1) da
\[ f(x) = x \]

Caso 2: Supongamos que
\[ x ≤ f(x) \tag{4} \]
Entonces, por ser \(f\) creciente, se tiene que
\[ f(x) ≤ f(f(x)) \tag{5} \]
Sustituyendo (1) en (5), se tiene
\[ f(x) ≤ x \]
que junto con (4) da
\[ f(x) = x \]

3.2. Demostraciones con Lean4

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

3.3. Demostraciones con Isabelle/HOL

4. Si f(x) ≤ f(y) → x ≤ y, entonces f es inyectiva

Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que
\[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \]
entonces \(f\) es inyectiva.

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

4.1. Demostración en lenguaje natural

Sean \(x, y ∈ ℝ\) tales que
\[ f(x) = f(y) \tag{1} \]
Tenemos que demostrar que \(x = y\).

De (1), tenemos que
\[ f(x) ≤ f(y) \]
y, por la hipótesis,
\[ x ≤ y \tag{2} \]

También de (1), tenemos que
\[ f(y) ≤ f(x) \]
y, por la hipótesis,
\[ y ≤ x \tag{3} \]

De (2) y (3), tenemos que
\[ x = y \]

4.2. Demostraciones con Lean4

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

4.3. Demostraciones con Isabelle/HOL

5. Los supremos de las sucesiones crecientes son sus límites

Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).

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

5.1. Demostración en lenguaje natural

Sea \(ε ∈ ℝ\) tal que \(ε > 0\). Tenemos que demostrar que
\[ (∃ m ∈ ℕ)(∀ n ∈ ℕ)[n ≥ m → |u_n – S| ≤ ε] \tag{1} \]

Por ser \(S\) un supremo de u, existe un k ∈ ℕ tal que
\[ u_k ≥ S – ε \tag{2} \]
Vamos a demostrar que \(k\) verifica la condición de (1); es decir, que si \(n ∈ ℕ\) tal que \(n ≥ k\), entonces
\[ |u_n – S| ≤ ε \]
o, equivalentemente,
\[ -ε ≤ u_n – S ≤ ε \]

La primera desigualdad se tiene por la siguente cadena:
\begin{align}
-ε &= (S – ε) – S \\
&≤ u_k – S &&\text{[por (2)]} \\
&≤ u_n – S &&\text{[porque \(u\) es creciente y \(n ≥ k\)]}
\end{align}

La segunda desigualdad se tiene por la siguente cadena:
\begin{align}
u_n – S &≤ S – S &&\text{[porque \(S\) es un supremo de \(u\)]} \\
&= 0 \\
&≤ ε
\end{align}

5.2. Demostraciones con Lean4

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

5.3. Demostraciones con Isabelle/HOL