La semana en Calculemus (21 de abril de 2024)
Desde el 18 de marzo, he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:
- 1. Si f es inyectiva, entonces f⁻¹(f(s)) ⊆ s
- 2. f(f⁻¹(u)) ⊆ u
- 3. Si f es suprayectiva, entonces u ⊆ f(f⁻¹(u))
- 4. Si s ⊆ t, entonces f(s) ⊆ f(t)
- 5. Si u ⊆ v, entonces f⁻¹(u) ⊆ f⁻¹(v)
- 6. f⁻¹(A ∪ B) = f⁻¹(A) ∪ f⁻¹(B)
- 7. f(s ∩ t) ⊆ f(s) ∩ f(t)
- 8. Si f es inyectiva, entonces f(s) ∩ f(t) ⊆ f(s ∩ t)
- 9. f(s) \ f(t) ⊆ f(s \ t)
- 10. f(s) ∩ t = f(s ∩ f⁻¹(t))
A continuación se muestran las soluciones.
Read More “La semana en Calculemus (21 de abril de 2024)”