Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. La suma de dos funciones acotadas superiormente también lo está
- 2. La suma de dos funciones acotadas inferiormente también lo está
- 3. Si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está
- 4. Si x e y son sumas de dos cuadrados, entonces xy también lo es
- 5. La relación de divisibilidad es transitiva
A continuación se muestran las soluciones.