Día: 31 octubre 2022

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

• 1. Si R es un retículo tal que x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z), entonces (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)
• 2. Si R es un retículo tal que x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z), entonces (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
• 3. Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a
• 4. Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b
• 5. Si R es un anillo ordenado y a, b, c ∈ R tales que a ≤ b y 0 ≤ c, entonces ac ≤ bc

A continuación se muestran las soluciones.
Read More “DAO: La semana en Calculemus (28 de octubre de 2022)”