La semana en Calculemus (10 de diciembre de 2023)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. P → ¬¬P
- 2. Si f no está acotada superiormente, entonces (∀a)(∃x)(f(x) > a)
- 3. Si ¬(∀a)(∃x)(f(x) > a), entonces f está acotada superiormente
- 4. Si f no es monótona, entonces ∃x∃y(x ≤ y ∧ f(y) < f(x))
- 5. Si 0 < 0, entonces a > 37 para cualquier número a
A continuación se muestran las soluciones.
Read More “La semana en Calculemus (10 de diciembre de 2023)”