Autor: José A. Alonso

Esta semana he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:

• 1. (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)
• 2. Pares ∪ Impares = Naturales
• 3. Los primos mayores que 2 son impares
• 4. s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)
• 5. (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

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

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

• 1. s \ (t ∪ u) ⊆ (s \ t) \ u
• 2. s ∩ t = t ∩ s
• 3. s ∩ (s ∪ t) = s
• 4. s ∪ (s ∩ t) = s
• 5. (s \ t) ∪ t = s ∪ t

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

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

• 1. Si la sucesión u converge a a y la v a b, entonces u+v converge a a+b
• 2. Unicidad del límite de las sucesiones convergentes
• 3. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de uₙ+c es a+c
• 4. Si el límite de la sucesión uₙ es a y c ∈ ℝ, entonces el límite de cuₙ es ca
• 5. El límite de uₙ es a syss el de uₙ-a es 0
• 6. Si uₙ y vₙ convergen a 0, entonces uₙvₙ converge a 0
• 7. Teorema del emparedado
• 8. Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u
• 9. s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)
• 10. (s \ t) \ u ⊆ s \ (t ∪ u)
• 11. (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)

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

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)”