Este repositorio contienen las soluciones en Lean4 e Isabelle/HOL de los ejercicios propuestos en el blog Calculemus.
Ejercicios más recientes
- Si f ∘ f es biyectiva, entonces f es biyectiva (En Lean y en Isabelle).
- Identidad de Brahmagupta-Fibonacci (En Lean y en Isabelle).
- Pruebas de ∑k<n. 2k = 2n-1 (En Lean y en Isabelle).
- Pruebas de "∑i<n i = n(n-1)/2" (En Lean y en Isabelle).
- Pruebas de (1+p)n mayor o igual que 1+np (En Lean y en Isabelle).
- Pruebas de 0³+1³+2³+3³+···+n³ = (n(n+1)/2)² (En Lean y en Isabelle).
- Pruebas de a+aq+aq²+···+aqⁿ = a(1-qⁿ⁺¹)/(1-q) (En Lean y en Isabelle).
- Pruebas de a+(a+d)+(a+2d)+···+(a+nd)=(n+1)(2a+nd)/2 (En Lean y en Isabelle).
- Pruebas de 0+1+2+3+···+n=n(n+1)/2 (En Lean y en Isabelle).
- Si f es continua en a y el límite de u(n) es a, entonces el límite de f(u(n)) es f(a) (En Lean y en Isabelle).
- Si x es límite de u e y es cota superior de u, entonces x ≤ y (En Lean y en Isabelle).
- Si (∀ ε > 0, y ≤ x + ε), entonces y ≤ x (En Lean y en Isabelle).
- Si x es el supremo de A, entonces ∀ y, y < x → ∃ a ∈ A, y < a (En Lean y en Isabelle).
- Pruebas de equivalencia de definiciones de la función de Fibonacci (In Lean4 and Isabelle).
- Pruebas de aplana (espejo a) = reverse (aplana a) (En Lean y en Isabelle).
- Pruebas de que la función espejo de los árboles binarios es involutiva (En Lean y en Isabelle).
- Pruebas de equivalencia de definiciones de inversa (En Lean e Isabelle).
- Pruebas de take n xs ++ drop n xs = xs (In Lean and Isabelle).
- Pruebas de length(xs ++ ys) = length(xs) + length(ys) (En Lean y en 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).
Ejercicios anteriores
Demostraciones de una propiedad de los números enteros
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) = a2-b2 (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) = (am)n (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+ea) ≤ log(1+eb) (En Lean4).
- En ℝ, si a ≤ b, entonces c - eb ≤ c - ea (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
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
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).