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»

En los retículos, x ⊔ (x ⊓ y) = x

Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊔ (x ⊓ y) = x \]

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

Read More «En los retículos, x ⊔ (x ⊓ y) = x»

En los retículos, x ⊓ (x ⊔ y) = x

Demostrar con Lean4 que en los retículos se verifica que
\[ x ⊓ (x ⊔ y) = x \]

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

Read More «En los retículos, x ⊓ (x ⊔ y) = x»

En los retículos, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)

Demostrar con Lean4 que en los retículos se verifica que
\[ (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) \]

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

Read More «En los retículos, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)»