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:

Read More «La composición de una función creciente y una decreciente es decreciente»

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:

Read More «Los monoides booleanos son conmutativos»

Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n

Demostrar con Lean4 que si \(M\) es un monoide, \(a ∈ M\) y \(m, n ∈ ℕ\), entonces
\[ a^{m·n} = (a^m)^n \]

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

Read More «Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n»

Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b, c ∈ G\) tales que \(a·b = a·c\), entonces \(b = c\).

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

Read More «Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c»

Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a

Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces
\[(a⁻¹)⁻¹ = a\]

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

Read More «Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a»

Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

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

Read More «Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹»

Unicidad de los inversos en los grupos

Demostrar con Lean4 que si \(a\) es un elemento de un grupo \(G\), entonces \(a\) tiene un único inverso; es decir, si \(b\) es un elemento de \(G\) tal que \(a·b = 1\), entonces \(a⁻¹ = b\).

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

Read More «Unicidad de los inversos en los grupos»

Unicidad del elemento neutro en los grupos

Demostrar con Lean4 que un grupo solo posee un elemento neutro.

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

Read More «Unicidad del elemento neutro en los grupos»

Caracterización de producto igual al primer factor

Un monoide cancelativo por la izquierda es un monoide \(M\) que cumple la propiedad cancelativa por la izquierda; es decir, para todo \(a, b ∈ M\)
\[ a·b = a·c ↔ b = c \]

En Lean4 la clase de los monoides cancelativos por la izquierda es LeftCancelMonoid y la propiedad cancelativa por la izquierda es

Demostrar con Lean4 que si \(M\) es un monoide cancelativo por la izquierda y \(a, b ∈ M\), entonces
\[ a·b = a ↔ b = 1 \]

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

Read More «Caracterización de producto igual al primer factor»

Unicidad de inversos en monoides

Demostrar con Lean4 que si \(M\) es un monoide conmutativo y \(x, y, z ∈ M\) tales que \(x·y = 1\) y \(x·z = 1\), entonces \(y = z\).

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

Read More «Unicidad de inversos en monoides»