Retículos – Calculemus

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

PorJosé A. Alonso 26 septiembre 20237 septiembre 2023

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:

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (a b c : α)

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

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (a b c : α)

example

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

: (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) :=

by sorry

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

PorJosé A. Alonso 25 septiembre 202326 septiembre 2023

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:

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (a b c : α)

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

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (a b c : α)

example

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

: (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) :=

by sorry

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

PorJosé A. Alonso 22 septiembre 20236 septiembre 2023

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

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]--
variable (x y : α)

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

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]--

variable (x y : α)

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

by sorry

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

PorJosé A. Alonso 21 septiembre 20235 septiembre 2023

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

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y : α)

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

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y : α)

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

by sorry

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

PorJosé A. Alonso 20 septiembre 20234 septiembre 2023

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:

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]
variable (x y z : α)

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

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y z : α)

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

by sorry

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

PorJosé A. Alonso 19 septiembre 20233 septiembre 2023

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:

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y z : α)

example : (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) :=
by sorry

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y z : α)

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

by sorry

En los retículos, x ⊔ y = y ⊔ x

PorJosé A. Alonso 18 septiembre 20231 septiembre 2023

Demostrar con Lean4 que en los retículos se verifica que
\[x ⊔ y = y ⊔ x\]
para todo $x$ e $y$ en el retículo.

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y z : α)

example : x ⊔ y = y ⊔ x :=
by sorry

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y z : α)

example : x ⊔ y = y ⊔ x :=

by sorry

En los retículos, x ⊓ y = y ⊓ x

PorJosé A. Alonso 15 septiembre 20231 septiembre 2023

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

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y z : α)

example : x ⊓ y = y ⊓ x :=
by sorry

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y z : α)

example : x ⊓ y = y ⊓ x :=

by sorry

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

PorJosé A. Alonso 25 octubre 202221 octubre 2022

Demostrar que Si R es un retículo tal que

   ∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)

1	∀ x y z : α, 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 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