Autor: José A. Alonso

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

• 1. La raíz cuadrada de 2 es irracional
• 2. Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales
• 3. En ℝ, |a| = |a – b + b|
• 4. En ℝ, si 1 < a, entonces a < aa
• 5. La sucesión constante sₙ = c converge a c

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (3 de febrero de 2024)”

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

• 1. En ℝ, x² = y² → x = y ∨ x = -y
• 2. ¬¬P → P
• 3. (P → Q) ↔ ¬P ∨ Q
• 4. Existen infinitos números primos
• 5. Si n² es par, entonces n es par

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (27 de enero de 2024)”

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

• 1. En ℝ, y > x² ⊢ y > 0 ∨ y < -1
• 2. En ℝ, -y > x² + 1 ⊢ y > 0 ∨ y < -1
• 3. En ℝ, si x < |y|, entonces x < y ó x < -y
• 4. En ℝ, x ≤ |x|
• 5. En ℝ, -x ≤ |x|

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (13 de enero de 2024)”

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

• 1. f: ℝ → ℝ no es monótona syss (∃x,y)(x ≤ y ∧ f(x) > f(y))
• 2. La función x ↦ -x no es monótona creciente
• 3. En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b
• 4. Si ≤ es un preorden, entonces < es irreflexiva
• 5. Si ≤ es un preorden, entonces < es transitiva

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (6 de enero de 2024)”