Día: 30 diciembre 2023

Estas 3 últimas semanas he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

• 1. {x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y
• 2. x ≤ y ∧ x ≠ y ⊢ y ≰ x
• 3. Si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m))
• 4. (∃x ∈ ℝ)(2 < x < 3)
• 5. Si (∃z ∈ ℝ)(x < z < y), entonces x < y
• 6. Existen números primos m y n tales que 4 < m < n < 10
• 7. En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x
• 8. En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y
• 9. En ℝ, x² + y² = 0 ↔ x = 0 ∧ y = 0
• 10. Si |x + 3| < 5, entonces -8 < x < 2
• 11. 3 divide al máximo común divisor de 6 y 15

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (30 de diciembre de 2023)”