Día: 28 octubre 2023

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

• 1. Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s
• 2. La función (x ↦ x + c) es inyectiva
• 3. Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva
• 4. La composición de funciones inyectivas es inyectiva
• 5. Hay algún número real entre 2 y 3

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (28 de octubre de 2023)”