Esta semana he publicado en Calculemus las demostraciones con Lean4 e Isabelle/HOL de las siguientes propiedades:

• 1. Unión con la imagen
• 2. Intersección con la imagen
• 3. Unión con la imagen inversa
• 4. Imagen de la unión general
• 5. Imagen de la intersección general

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (27 de abril de 2024)”

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

• 1. s ∪ (⋂ᵢ Aᵢ) = ⋂ᵢ (Aᵢ ∪ s)
• 2. f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)
• 3. f(s ∪ t) = f(s) ∪ f(t)
• 4. s ⊆ f⁻¹(f(s))
• 5. f(s) ⊆ u ↔ s ⊆ f⁻¹(u)

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (16 de marzo de 2024)”