Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0
- 2. Si x, y, ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε
- 3. La suma de una cota superior de f y una cota superior de g es una cota superior de f+g
- 4. La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
- 5. El producto de dos funciones no negativas es no negativa
A continuación se muestran las soluciones.