En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc

Demostrar con Lean4 que, en los anillos ordenados,
\[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]

Para ello, completar la siguiente teoría de Lean4:

Read More «En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc»

En los anillos ordenados, 0 ≤ b – a → a ≤ b

Demostrar con Lean4 que en los anillos ordenados
\[ 0 ≤ b – a → a ≤ b \]

Para ello, completar la siguiente teoría de Lean4:

Read More «En los anillos ordenados, 0 ≤ b – a → a ≤ b»

En los anillos ordenados, a ≤ b → 0 ≤ b – a

Demostrar con Lean4 que en los anillos ordenados se verifica que
\[ a ≤ b → 0 ≤ b – a \]

Para ello, completar la siguiente teoría de Lean4:

Read More «En los anillos ordenados, a ≤ b → 0 ≤ b – a»

En los retículos, una distributiva del supremo implica la otra

Demostrar con Lean4 que si \(R\) es un retículo tal que
\[ (∀ x,\ y,\ z \in R) [x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)] \]
entonces
\[ (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) \]
para todos los elementos del retículo.

Para ello, completar la siguiente teoría de Lean4:

Read More «En los retículos, una distributiva del supremo implica la otra»

En los retículos, una distributiva del ínfimo implica la otra

Demostrar con Lean4 que si α es un retículo tal que se
$$(∀ x, y, z) [x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))]$$
entonces
$$(a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)$$
para todos los elementos de α.

Para ello, completar la siguiente teoría de Lean4:

Read More «En los retículos, una distributiva del ínfimo implica la otra»