octubre 2022 – Página 2

Si R es un retículo tal que (∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))), entonces (∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c))

PorJosé A. Alonso 24 octubre 202220 octubre 2022

Demostrar que si R es un retículo tal que

   (∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))),

1	(∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))),

entonces

   (∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c))

1	(∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c))

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

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

example
  (h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))
  : ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=
sorry

import order.lattice

variables {R : Type*} [lattice R]

example

(h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))

: ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=

sorry

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

PorJosé A. Alonso 21 octubre 202220 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

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

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

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

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

PorJosé A. Alonso 18 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