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

• 1. s ∪ (⋂ᵢ Aᵢ) = ⋂ᵢ (Aᵢ ∪ s)
• 2. f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)
• 3. f(s ∪ t) = f(s) ∪ f(t)
• 4. s ⊆ f⁻¹(f(s))
• 5. f(s) ⊆ u ↔ s ⊆ f⁻¹(u)

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

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