20 octubre 2022 – Calculemus

Si R es un retículo y x, y ∈ R, entonces x ⊓ (x ⊔ y) = x

PorJosé A. Alonso 20 octubre 2022

Demostrar que si R es un retículo y x, y ∈ R, entonces

x ⊓ (x ⊔ y) = x

1	x ⊓ (x ⊔ y) = x

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

import order.lattice
variables {R : Type*} [lattice R]
variables x y : R

example : x ⊓ (x ⊔ y) = x :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

variables x y : R

example : x ⊓ (x ⊔ y) = x :=

sorry

PorJosé A. Alonso 20 octubre 2022

Demostrar que si R es un retículo y x, y, z ∈ R, entonces

(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)

1	(x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)

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

import order.lattice

variables {R : Type*} [lattice R]
variables x y z : R

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

variables x y z : R

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=

sorry