Este repositorio contienen las soluciones en Lean4 e Isabelle/HOL de los ejercicios propuestos en el blog Calculemus.

Ejercicios ordenados por fecha de publicación

2020

Enero 2020

• 14 Celebración del día mundial de la lógica (En Isabelle).
• 24 Reto f(f(f(b))) = f(b) (En Isabelle).
• 30 Teorema de Nicómaco (En Isabelle).

Febrero 2020

• 24 Praeclarum theorema (En Isabelle).

Marzo 2020

• 05 El problema lógico del mal (En Isabelle).
• 12 La dama o el tigre (En Isabelle).
• 19 El problema de los infectados (En Isabelle).
• 31 El problema del barbero (En Isabelle).

Abril 2020

• 08 Las relaciones reflexivas y circulares son simétricas (En Isabelle).

2021

Mayo 2021

• 17 Demostraciones de "Si s ⊆ t, entonces s ∩ u ⊆ t ∩ u" (En Lean y en Isabelle).
• 18 Demostraciones de "s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)" (En Lean y en Isabelle).
• 19 Demostraciones de "(s - t) - u ⊆ s - (t ∪ u)" (En Lean y en Isabelle).
• 20 Demostraciones de "(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)" (En Lean y en Isabelle).
• 21 Demostraciones de "s \ (t ∪ u) ⊆ (s \ t) \ u" (En Lean y en Isabelle).
• 24 Demostraciones de "s ∩ t = t ∩ s" (En Lean y en Isabelle).
• 25 Demostraciones de "s ∩ (s ∪ t) = s" (En Lean y en Isabelle).
• 26 Demostraciones de "s ∪ (s ∩ t) = s" (En Lean y en Isabelle).
• 27 Demostraciones de "(s \ t) ∪ t = s ∪ t" (En Lean y en Isabelle).
• 28 Demostraciones de "(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)" (En Lean y en Isabelle).
• 31 Unión de los conjuntos de los pares e impares (En Lean y en Isabelle).

Junio 2021

• 01 Intersección de los primos y los mayores que dos (En Lean y en Isabelle).
• 02 s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s) (En Lean y en Isabelle).
• 03 ⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i)) (En Lean y en Isabelle).
• 04 s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) (En Lean y en Isabelle).
• 05 f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v) (En Lean y en Isabelle).
• 06 f(s ∪ t) = f(s) ∪ f(t) (En Lean y en Isabelle).
• 07 s ⊆ f⁻¹(f(s)) (En Lean y en Isabelle).
• 08 f(s) ⊆ u ↔ s ⊆ f⁻¹(u) (En Lean y en Isabelle).
• 09 Si f es inyectiva, entonces f⁻¹(f(s)) ⊆ s (En Lean y en Isabelle).
• 10 f[f⁻¹[u]​] ⊆ u (En Lean y en Isabelle).
• 11 Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]​]​ (En Lean y en Isabelle).
• 12 Si s ⊆ t, entonces f[s] ⊆ f[t]​ (En Lean y en Isabelle).
• 13 Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]​ (En Lean y en Isabelle).
• 14 f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]​ (En Lean y en Isabelle).
• 15 f[s ∩ t] ⊆ f[s] ∩ f[t]​ (En Lean y en Isabelle).
• 16 Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]​ (En Lean y en Isabelle).
• 17 f[s] \ f[t] ⊆ f[s \ t]​ (En [Lean](./src/A2021/M06/Imagen_de_la_diferencia_