Autor: José A. Alonso

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.

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.