Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. El producto de dos funciones impares es par
- 2. El producto de una función par por una impar es impar
- 3. Si f es par y g es impar, entonces f ∘ g es par
- 4. Para cualquier conjunto s, s ⊆ s
- 5. Si r ⊆ s y s ⊆ t, entonces r ⊆ t
A continuación se muestran las soluciones.