Reservoir

This repository contains the solutions in Lean4 and Isabelle/HOL for the exercises proposed in the Calculemus blog.

Latest exercises

• Proofs of "0 + 1 + 2 + 3 + ··· + n = n × (n + 1)/2" (In Lean and Isabelle).
• If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a) (In Lean and Isabelle).
• If x is the limit of u and y is an upper bound of u, then x ≤ y (In Lean and Isabelle).
• If (∀ ε > 0, y ≤ x + ε), then y ≤ x (In Lean4 and Isabelle).
• If x is the supremum of set A, then ∀ y, y < x → ∃ a ∈ A, y < a (In Lean and Isabelle).
• Equivalence of definitions of the Fibonacci function (In Lean4 and Isabelle).
• Proofs of "flatten (mirror a) = reverse (flatten a)" (In Lean4 and Isabelle).
• Proofs that the mirror function of binary trees is involutive (In Lean4 and Isabelle).
• Equivalence of reverse definitions (In Lean and Isabelle).
• Proofs of "take n xs ++ drop n xs = xs" (In Lean and Isabelle).
• Proofs of the equality "length(xs ++ ys) = length(xs) + length(ys)" (In Lean and Isabelle).
• Asociatividad de la concatenación de listas (En Lean y en Isabelle).
• Pruebas de "length (replicate n x) = n" (En Lean y en Isabelle).
• Si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n (En Lean y en Isabelle).
• Las sucesiones divergentes positivas no tienen límites finitos (En Lean y en Isabelle).
• Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u (En Lean y en Isabelle).
• El punto de acumulación de las sucesiones convergente es su límite (En Lean y en Isabelle).
• Las subsucesiones tienen el mismo límite que la sucesión (En Lean y en Isabelle).
• Si a es un punto de acumulación de u, entonces (∀ε>0)(∀n∈ℕ)(∃k≥n)[u(k)−a| < ε]​ (En Lean y en Isabelle).
• Las funciones de extracción no están acotadas (En Lean y en Isabelle).
• Relación entre los índices de las subsucesiones y de la sucesión (En Lean y en Isabelle).
• Las particiones definen relaciones de equivalencia (En Lean y en Isabelle).
• Las particiones definen relaciones transitivas (En Lean y en Isabelle).
• Las familias de conjuntos definen relaciones simétricas (En Lean y en Isabelle).
• Las particiones definen relaciones reflexivas (En Lean y en Isabelle).
• El conjunto de las clases de equivalencia es una partición (En Lean y en Isabelle).
• Las clases de equivalencia de elementos no relacionados son disjuntas (En Lean y en Isabelle).
• Las clases de equivalencia de elementos relacionados son iguales (En Lean y en Isabelle).
• Las sucesiones convergentes son sucesiones de Cauchy (En Lean y en Isabelle).
• La composición por la izquierda con una inyectiva es una operación inyectiva (En Lean y en Isabelle).
• La igualdad de valores es una relación de equivalencia (En Lean y en Isabelle).
• La equipotencia es una relación de equivalencia (En Lean y en Isabelle).
• La equipotencia es una relación transitiva (En Lean y en Isabelle).

Old exercises

Demostraciones de una propiedad de los números enteros

• ∀ m n ∈ ℕ, Even n → Even (m * n) (En Lean4).

Propiedades elementales de los números reales

• En ℝ, (ab)c = b(ac) (En Lean4).
• En ℝ, (cb)a = b(ac) (En Lean4).
• En ℝ, a(bc) = b(ac) (En Lean4).
• En ℝ, si ab = cd y e = f, entonces a(be) = c(df) (En Lean4).
• En ℝ, si bc = ef, entonces ((ab)c)d = ((ae)f)d (En Lean4).
• En ℝ, si c = ba-d y d = ab, entonces c = 0 (En Lean4).
• En ℝ, (a+b)(a+b) = aa+2ab+bb (En Lean4).
• En ℝ, (a+b)(c+d) = ac+ad+bc+bd (En Lean4).
• En ℝ, (a+b)(a-b) = a²-b² (En Lean4).
• En ℝ, si c = da+b y b = ad, entonces c = 2ad (En Lean4).
• En ℝ, si a+b = c, entonces (a+b)(a+b) = ac+bc (En Lean4).
• Si x e y son sumas de dos cuadrados, entonces xy también lo es (En Lean4).
• En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0 (En Lean4).
• En ℝ, x² = 1 → x = 1 ∨ x = -1 (En Lean4).
• En ℝ, x² = y² → x = y ∨ x = -y (En Lean4).
• En ℝ, |a| = |a - b + b| (En Lean4).

Propiedades elementales de los monoides

• En los monoides, los inversos a la izquierda y a la derecha son iguales (En Lean y en Isabelle).
• Producto de potencias de la misma base en monoides (En Lean y en Isabelle).
• Equivalencia de inversos iguales al neutro (En Lean y en Isabelle).
• Unicidad de inversos en monoides (En Lean y en Isabelle).
• Caracterización de producto igual al primer factor (En Lean y en Isabelle).
• Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)ⁿ (En Lean y en Isabelle).
• Los monoides booleanos son conmutativos (En Lean y en Isabelle).

Propiedades elementales de los grupos

• Unicidad del elemento neutro en los grupos (En Lean y en Isabelle).
• Si G es un grupo y a ∈ G, entonces aa⁻¹ = 1 (En Lean4).
• Si G es un grupo y a ∈ G, entonces a·1 = a (En Lean4).
• Si G es un grupo y a, b ∈ G tales que ab = 1 entonces a⁻¹ = b (En Lean y en Isabelle).
• Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹ (En Lean y en Isabelle).
• Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a (En Lean y en Isabelle).
• Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c (En Lean y en Isabelle).

Propiedades elementales de los anillos

• Si R es un anillo y a ∈ R, entonces a + 0 = a (En Lean4).
• Si R es un anillo y a ∈ R, entonces a + -a = 0 (En Lean4).
• Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b (En Lean4).
• Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a (En Lean4).
• Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c (En Lean4).
• Si R es un anillo y a, b, c ∈ R tales que a+b=c+b, entonces a=c (En Lean4).
• Si R es un anillo y a ∈ R, entonces a.0 = 0 (En Lean4).
• Si R es un anillo y a ∈ R, entonces 0.a = 0 (En Lean4).
• Si R es un anillo y a, b ∈ R tales que a+b=0, entonces -a=b (En Lean4).
• Si R es un anillo y a, b ∈ R tales que a+b=0, entonces a=-b (En Lean4).
• Si R es un anillo, entonces -0 = 0 (En Lean4).
• Si R es un anillo y a ∈ R, entonces -(-a) = a (En Lean4).
• Si R es un anillo y a, b ∈ R, entonces a - b = a + -b (En Lean4).
• Si R es un anillo y a ∈ R, entonces a - a = 0 (En Lean4).
• En los anillos, 1 + 1 = 2 (En Lean4).
• Si R es un anillo y a ∈ R, entonces 2a = a+a (En Lean4).

Propiedades de orden en los números reales

• En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e (En Lean4).
• En ℝ, si 2a ≤ 3b, 1 ≤ a y d = 2, entonces d + a ≤ 5b (En Lean4).
• En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ (En Lean4).
• En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f (En Lean4).
• En ℝ, si d ≤ f, entonces c + e^{(a + d)} ≤ c + e^{(a + f)} (En Lean4).
• En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b) (En Lean4).
• En ℝ, si a ≤ b, entonces c - e^b ≤ c - e^a (En Lean4).
• En ℝ, 2ab ≤ a² + b² (En Lean4).
• En ℝ, |ab| ≤ (a²+b²)/2 (En Lean4).
• En ℝ, min(a,b) = min(b,a) (En Lean4).
• En ℝ, max(a,b) = max(b,a) (En Lean4).
• En ℝ, min(min(a,b),c) = min(a,min(b,c)) (En Lean4).
• En ℝ, min(a,b)+c = min(a+c,b+c) (En Lean4).
• En ℝ, |a| - |b| ≤ |a - b| (En Lean4).
• En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε (En Lean4).
• En ℝ, a < b → ¬(b < a) (En Lean4).
• Hay algún número real entre 2 y 3 (En Lean4).
• Si (∀ε > 0)(x ≤ ε), entonces x ≤ 0 (En Lean4).
• Si 0 < 0, entonces a > 37 para cualquier número a (En Lean4).
• {x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y (En Lean4).
• x ≤ y ∧ x ≠ y ⊢ y ≰ x (En Lean4).
• (∃x ∈ ℝ)(2 < x < 3)​ (En Lean4).
• Si (∃z ∈ ℝ)(x < z < y), entonces x < y (En Lean4).
• En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x (En Lean4).
• En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y (En Lean4).
• Si |x + 3| < 5, entonces -8 < x < 2 (En Lean4).
• En ℝ, y > x² ⊢ y > 0 ∨ y < -1 (En Lean4).
• En ℝ, -y > x² + 1 ⊢ y > 0 ∨ y < -1 (En Lean4).
• En ℝ, si x < |y|, entonces x < y ó x < -y (En Lean4).
• En ℝ, x ≤ |x| (En Lean4).
• En ℝ, -x ≤ |x| (En Lean4).
• En ℝ, |x + y| ≤ |x| + |y| (En Lean4).
• En ℝ, si x ≠ 0 entonces x < 0 ó x > 0 (En Lean4).
• Si (∃ x, y ∈ ℝ)(z = x² + y² ∨ z = x² + y² + 1), entonces z ≥ 0 (En Lean4).
• En ℝ, si 1 < a, entonces a < aa (En Lean4).
• Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y (En Lean y en Isabelle).

Divisibilidad

• Si x, y, z ∈ ℕ, entonces x divide a yxz (En Lean4).
• Si x divide a w, también divide a y(xz)+x²+w² (En Lean4).
• Transitividad de la divisibilidad (En Lean4).
• Si a divide a b y a c, entonces divide a b+c (En Lean4).
• Conmutatividad del máximo común divisor (En Lean4).
• Si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m)) (En Lean4).
• Existen números primos m y n tales que 4 < m < n < 10 (En Lean4).
• 3 divide al máximo común divisor de 6 y 15 (En Lean4).
• Si m divide a n o a k, entonces m divide a nk (En Lean4).
• Existen infinitos números primos (En Lean4).
• Si n² es par, entonces n es par (En Lean4).
• La raíz cuadrada de 2 es irracional (En Lean).
• Un número es par si y solo si lo es su cuadrado (En Lean y en Isabelle).

Retículos

• En los retículos, x ⊓ y = y ⊓ x (En Lean4).
• En los retículos, x ⊔ y = y ⊔ x (En Lean4).
• En los retículos, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) (En Lean4).
• En los retículos, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) (En Lean4).
• En los retículos, x ⊓ (x ⊔ y) = x (En Lean4).
• En los retículos, x ⊔ (x ⊓ y) = x (En Lean4).
• En los retículos, una distributiva del ínfimo implica la otra (En Lean4).
• En los retículos, una distributiva del supremos implica la otra (En Lean4).

Relaciones de orden

• En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b (En Lean4).
• Si ≤ es un preorden, entonces < es irreflexiva (En Lean4).
• Si ≤ es un preorden, entonces < es transitiva (En Lean4).

Relaciones de equivalencia

• La congruencia módulo 2 es una relación de equivalencia (En Lean y en Isabelle).

Anillos ordenados

• En los anillos ordenados, a ≤ b → 0 ≤ b - a (En Lean4).
• En los anillos ordenados, 0 ≤ b - a → a ≤ b (En Lean4).
• En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc (En Lean4).

Espacios métricos

• En los espacios métricos, dist(x,y) ≥ 0 (En Lean4).

Funciones reales

• La suma de una cota superior de f y una cota superior de g es una cota superior de f+g (En Lean4).
• La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g (En Lean4).
• El producto de funciones no negativas es no negativo (En Lean4).
• Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces ab es una cota superior de fg (En Lean4).
• La suma de dos funciones acotadas superiormente también lo está (En Lean4).
• La suma de dos funciones acotadas inferiormente también lo está (En Lean4).
• Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf (En Lean4).
• Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está (En Lean4).
• Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior (En Lean4).
• Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior (En Lean4).
• La función identidad no está acotada superiormente (En Lean4).
• Si f no está acotada superiormente, entonces (∀a)(∃x)(f(x) > a)​ (En Lean4).
• Si ¬(∀a)(∃x)(f(x) > a)​, entonces f está acotada superiormente (En Lean4).
• Suma de funciones monótonas (En Lean4).
• Si c es no negativo y f es monótona, entonces cf es monótona. (En Lean4).
• La composición de dos funciones monótonas es monótona (En Lean4).
• Si f es monótona y f(a) < f(b), entonces a < b (En Lean4).
• Si a, b ∈ ℝ tales que a ≤ b y f(b) < f(a), entonces f no es monótona (En Lean4).
• No para toda f : ℝ → ℝ monótona, (∀a,b)(f(a) ≤ f(b) → a ≤ b)​ (En Lean4).
• Si f no es monótona, entonces ∃x∃y(x ≤ y ∧ f(y) < f(x))​ (En Lean4).
• f: ℝ → ℝ no es monótona syss (∃x,y)(x ≤ y ∧ f(x) > f(y))​ (En Lean4).
• La función x ↦ -x no es monótona creciente (En Lean4).
• La suma de dos funciones pares es par (En Lean4).
• El producto de dos funciones impares es par (En Lean4).
• El producto de una función par por una impar es impar (En Lean4).
• Si f es par y g es impar, entonces (f ∘ g) es par (En Lean4).
• Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales (En Lean4).
• La composición de una función creciente y una decreciente es decreciente (En Lean y en Isabelle).
• Si una función es creciente e involutiva, entonces es la identidad (En Lean y en Isabelle).
• Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva (En Lean y en Isabelle).
• Las funciones con inversa por la izquierda son inyectivas (En Lean y en Isabelle).
• Si g ∘ f es inyectiva, entonces f es inyectiva (En Lean4 y en Isabelle).

Teoría de conjuntos

• Para cualquier conjunto s, s ⊆ s (En Lean4).
• Si r ⊆ s y s ⊆ t, entonces r ⊆ t (En Lean4).
• Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u (En Lean y en Isabelle).
• s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) (En Lean y en Isabelle).
• (s \ t) \ u ⊆ s \ (t ∪ u) (En Lean y en Isabelle).
• (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u) (En Lean y en Isabelle).
• s \ (t ∪ u) ⊆ (s \ t) \ u (En Lean y en Isabelle).
• s ∩ t = t ∩ s (En Lean y en Isabelle).
• s ∩ (s ∪ t) = s (En Lean y en Isabelle).
• s ∪ (s ∩ t) = s (En Lean y en Isabelle).
• (s \ t) ∪ t = s ∪ t (En Lean y en Isabelle).
• (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) (En Lean y en Isabelle).
• pares ∪ impares = naturales (En Lean y en Isabelle).
• Los primos mayores que 2 son impares (En Lean y en Isabelle).
• s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) (En Lean y en Isabelle).
• (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) (En Lean y en Isabelle).
• s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) (En Lean y en Isabelle).
• f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]​ (En Lean y en Isabelle).
• f[s ∪ t] = f[s] ∪ f[t]​ (En Lean y en Isabelle).
• s ⊆ f⁻¹[f[s]​]​ (En Lean y en Isabelle).
• f[s] ⊆ u ↔ s ⊆ f⁻¹[u]​ (En Lean y en Isabelle).
• Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s (En Lean4).
• La función (x ↦ x + c) es inyectiva (En Lean4).
• Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva (En Lean4).
• La composición de funciones inyectivas es inyectiva (En Lean4).
• La función (x ↦ x + c) es suprayectiva (En Lean4).
• Si c ≠ 0, entonces la función (x ↦ cx) es suprayectiva (En Lean4).
• Si c ≠ 0, entonces la función (x ↦ cx + d) es suprayectiva (En Lean4).
• Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9 (En Lean4).
• La composición de funciones suprayectivas es suprayectiva (En Lean4).
• Si f es inyectiva, entonces f⁻¹[f[s]​] ⊆ s (En Lean y en Isabelle).
• f[f⁻¹[u]​] ⊆ u (En Lean y en Isabelle).
• Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]​ (En Lean y en Isabelle).
• Si s ⊆ t, entonces f[s] ⊆ f[t]​ (En Lean y en Isabelle).
• Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​ (En Lean y en Isabelle).
• f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]​ (En Lean y en Isabelle).
• f[s ∩ t] ⊆ f[s] ∩ f[t]​ (En Lean y en Isabelle).
• Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​ (En Lean y en Isabelle).
• f[s] \ f[t] ⊆ f[s \ t]​ (En Lean y en Isabelle).
• f[s] ∩ v = f[s ∩ f⁻¹[v]​]​ (En Lean y en Isabelle).
• Unión con la imagen (En Lean y en Isabelle).
• Intersección con la imagen inversa (En Lean y en Isabelle).
• Unión con la imagen inversa (En Lean y en Isabelle).
• Imagen de la unión general (En Lean y en Isabelle).
• Imagen de la intersección general (En Lean y en Isabelle).
• Imagen de la intersección general mediante aplicaciones inyectivas (En Lean y en Isabelle).
• Imagen inversa de la unión general (En Lean y en Isabelle).
• Imagen inversa de la intersección general (En Lean y en Isabelle).
• Teorema de Cantor (En Lean y en Isabelle).
• Si g ∘ f es suprayectiva, entonces g es suprayectiva (En Lean4 y en Isabelle).
• Las funciones inyectivas tienen inversa por la izquierda (En Lean y en Isabelle).
• Las funciones con inversa por la derecha son suprayectivas (En Lean y en Isabelle).
• Las funciones suprayectivas tienen inversa por la derecha (En Lean y en Isabelle).
• Las funciones con inversa son biyectivas (En Lean y en Isabelle).
• Las funciones biyectivas tienen inversa (En Lean y en Isabelle).
• La equipotencia es una relación reflexiva (En Lean y en Isabelle).
• La inversa de una función es biyectiva (En Lean y en Isabelle).
• La equipotencia es una relación simétrica (En Lean y en Isabelle).
• La composición de funciones biyectivas es biyectiva (En Lean y en Isabelle).

Lógica

• Si ¬(∃x)P(x), entonces (∀x)¬P(x) (En Lean4).
• Si (∀x)¬P(x), entonces ¬(∃x)P(x) (En Lean4).
• Si ¬(∀x)P(x), entonces (∃x)¬P(x) (En Lean4).
• Si (∃x)¬P(x), entonces ¬(∀x)P(x) (En Lean4).
• ¬¬P → P (En Lean4).
• P → ¬¬P (En Lean4).
• (P → Q) ↔ ¬P ∨ Q (En Lean4).
• La paradoja del barbero (En Lean y en Isabelle).

Límites de sucesiones

• La sucesión constante sₙ = c converge a c (en Lean4 y en Isabelle).
• Si la sucesión s converge a b y la t a c, entonces s+t converge a b+c (En Lean4 y en Isabelle).
• Unicidad del límite de las sucesiones convergentes (En Lean4 y en Isabelle).
• Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de uₙ+c es a+c (En Lean y en Isabelle).
• Si el límite de la sucesión u(n) es a y c ∈ ℝ, entonces el límite de cu(n) es ca (En Lean y en Isabelle).
• El límite de u es a syss el de u-a es 0 (En Lean y en Isabelle).
• Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0 (En Lean y en Isabelle).
• Teorema del emparedado (En Lean y en Isabelle).
• Los supremos de las sucesiones crecientes son sus límites (En Lean y en Isabelle).
• Las sucesiones convergentes están acotadas (En Lean y en Isabelle).
• Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ (En Lean y en Isabelle).
• Si uₙ está acotada y lim vₙ = 0, entonces lim (uₙ·vₙ) = 0 (En Lean y en Isabelle).
• Si el límite de la sucesión uₙ es a, entonces el límite de -uₙ es -a (En Lean y en Isabelle).