ForMatUS

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

• 1. En los retículos, una distributiva del ínfimo implica la otra
• 2. En los retículos, una distributiva del supremo implica la otra
• 3. En los anillos ordenados, a ≤ b → 0 ≤ b – a
• 4. En los anillos ordenados, 0 ≤ b – a → a ≤ b
• 5. En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (30 de septiembre de 2023)”

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

• 1. En los retículos, x ⊔ y = y ⊔ x
• 2. En los retículos, (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z)
• 3. En los retículos, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)
• 4. En los retículos, x ⊓ (x ⊔ y) = x
• 5. En los retículos, x ⊔ (x ⊓ y) = x

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (23 de septiembre de 2023)”

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

• 1. En ℝ, |a| – |b| ≤ |a – b|
• 2. Si x, y, z ∈ ℕ, entonces x divide a yxz
• 3. Si x divide a w, entonces también divide a y(xz)+x²+w²
• 4. Conmutatividad del máximo común divisor
• 5. En los retículos, x ⊓ y = y ⊓ x

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

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

• 1. En ℝ, |ab| ≤ (a²+b²)/2
• 2. En ℝ, min(a,b) = min(b,a)
• 3. En ℝ, max(a,b) = max(b,a)
• 4. En ℝ, min(min(a,b),c) = min(a,min(b,c))
• 5. En ℝ, min(a,b)+c = min(a+c,b+c)

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (9 de septiembre de 2023)”

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

• 1. En ℝ, si a ≤ b y c < d, entonces a + eᶜ + f ≤ b + eᵈ + f
• 2. En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f)
• 3. En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b)
• 4. En ℝ, si a ≤ b entonces c – e^b ≤ c – e^a
• 5. En ℝ, 2ab ≤ a² + b²

A continuación se muestran las soluciones.
Read More “La semana en Calculemus (2 de septiembre de 2023)”