La semana en Calculemus (6 de enero de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. f: ℝ → ℝ no es monótona syss (∃x,y)(x ≤ y ∧ f(x) > f(y))
- 2. La función x ↦ -x no es monótona creciente
- 3. En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b
- 4. Si ≤ es un preorden, entonces < es irreflexiva
- 5. Si ≤ es un preorden, entonces < es transitiva
A continuación se muestran las soluciones.
Read More “La semana en Calculemus (6 de enero de 2024)”