Asociatividad_del_supremo.md

Título	Autor
En los retículos, (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)	José A. Alonso

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

Demostración en lenguaje natural

[mathjax] En la demostración se usarán los siguientes lemas \begin{align} &x ≤ y → y ≤ x → x = y \tag{L1} \label{L1} \ &x ≤ x ⊔ y \tag{L2} \label{L2} \ &y ≤ x ⊔ y \tag{L3} \label{L3} \ &x ≤ z → y ≤ z → x ⊔ y ≤ z \tag{L4} \label{L4} \ \end{align}

Por \ref{L1}, basta demostrar las siguientes relaciones: \begin{align} (x ⊔ y) ⊔ z &≤ x ⊔ (y ⊔ z) \tag{1} \label{1} \ x ⊔ (y ⊔ z) &≤ (x ⊔ y) ⊔ z \tag{2} \label{2} \end{align}

Para demostrar (\ref{1}), por \ref{L4}, basta probar \begin{align} x ⊔ y &≤ x ⊔ (y ⊔ z) \tag{1a} \label{1a} \ z &≤ x ⊔ (y ⊔ z) \tag{1b} \label{1b} \end{align}

Para demostrar (\ref{1a}), por \ref{L4}, basta probar \begin{align} x &≤ x ⊔ (y ⊔ z) \tag{1a1} \label{1a1} \ y &≤ x ⊔ (y ⊔ z) \tag{1a2} \label{1a2} \end{align}

La (\ref{1a1}) se tiene por \ref{L2}.

La (\ref{1a2}) se tiene por la siguiente cadena de desigualdades: \begin{align} y &≤ y ⊔ z &&\text{[por \ref{L2}]} \ &≤ x ⊔ (y ⊔ z) &&\text{[por \ref{L3}]} \end{align}

La (\ref{1b}) se tiene por la siguiente cadena de desigualdades \begin{align} z &≤ y ⊔ z &&\text{[por \ref{L3}]} \ &≤ x ⊔ (y ⊔ z) &&\text{[por \ref{L3}]} \end{align}

Para demostrar (\ref{2}), por \ref{L4}, basta probar \begin{align} x &≤ (x ⊔ y) ⊔ z \tag{2a} \label{2a} \ y ⊔ z &≤ (x ⊔ y) ⊔ z \tag{2b} \label{2b} \end{align}

La (\ref{2a}) se demuestra por la siguiente cadena de desigualdades: \begin{align} x &≤ x ⊔ y &&\text{[por \ref{L2}]} \ &≤ (x ⊔ y) ⊔ z &&\text{[por \ref{L2}]} \end{align}

Para demostrar (\ref{2b}), por \ref{L4}, basta probar \begin{align} y &≤ (x ⊔ y) ⊔ z \tag{2b1} \label{2b1} \ z &≤ (x ⊔ y) ⊔ z \tag{2b2} \label{2b2} \end{align}

La (\ref{2b1}) se demuestra por la siguiente cadena de desigualdades: \begin{align} y &≤ x ⊔ y &&\text{[por \ref{L3}]} \ &≤ (x ⊔ y) ⊔ z &&\text{[por \ref{L2}]} \end{align}

La (\ref{2b2}) se tiene por \ref{L3}.

Demostraciones con Lean4

import Mathlib.Order.Lattice

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

-- 1ª demostración
-- ===============

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
by
  have h1 : (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z) := by
  { have h1a : x ⊔ y ≤ x ⊔ (y ⊔ z) := by
    { have h1a1 : x ≤ x ⊔ (y ⊔ z) := by exact le_sup_left
      have h1a2 : y ≤ x ⊔ (y ⊔ z) := calc
        y ≤ y ⊔ z       := by exact le_sup_left
        _ ≤ x ⊔ (y ⊔ z) := by exact le_sup_right
      show x ⊔ y ≤ x ⊔ (y ⊔ z)
      exact sup_le h1a1 h1a2 }
    have h1b : z ≤ x ⊔ (y ⊔ z) := calc
      z ≤ y ⊔ z       := by exact le_sup_right
      _ ≤ x ⊔ (y ⊔ z) := by exact le_sup_right
    show (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z)
    exact sup_le h1a h1b }
  have h2 : x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z := by
  { have h2a : x ≤ (x ⊔ y) ⊔ z := calc
      x ≤ x ⊔ y       := by exact le_sup_left
      _ ≤ (x ⊔ y) ⊔ z := by exact le_sup_left
    have h2b : y ⊔ z ≤ (x ⊔ y) ⊔ z := by
    { have h2b1 : y ≤ (x ⊔ y) ⊔ z := calc
        y ≤ x ⊔ y       := by exact le_sup_right
        _ ≤ (x ⊔ y) ⊔ z := by exact le_sup_left
      have h2b2 : z ≤ (x ⊔ y) ⊔ z := by
        exact le_sup_right
      show  y ⊔ z ≤ (x ⊔ y) ⊔ z
      exact sup_le h2b1 h2b2 }
    show x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z
    exact sup_le h2a h2b }
  show (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z)
  exact le_antisymm h1 h2

-- 2ª demostración
-- ===============

example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) :=
by
  apply le_antisymm
  · -- (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z)
    apply sup_le
    · -- x ⊔ y ≤ x ⊔ (y ⊔ z)
      apply sup_le
      . -- x ≤ x ⊔ (y ⊔ z)
        apply le_sup_left
      · -- y ≤ x ⊔ (y ⊔ z)
        apply le_trans
        . -- y ≤ y ⊔ z
          apply @le_sup_left _ _ y z
        . -- y ⊔ z ≤ x ⊔ (y ⊔ z)
          apply le_sup_right
    . -- z ≤ x ⊔ (y ⊔ z)
      apply le_trans
      . -- z ≤ x ⊔ (y ⊔ z)
        apply @le_sup_right _ _ y z
      . -- y ⊔ z ≤ x ⊔ (y ⊔ z)
        apply le_sup_right
  . -- x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z
    apply sup_le
    · -- x ≤ (x ⊔ y) ⊔ z
      apply le_trans
      . -- x ≤ x ⊔ y
        apply @le_sup_left _ _ x y
      . -- x ⊔ y ≤ (x ⊔ y) ⊔ z
        apply le_sup_left
    . -- y ⊔ z ≤ (x ⊔ y) ⊔ z
      apply sup_le
      · -- y ≤ (x ⊔ y) ⊔ z
        apply le_trans
        . -- y ≤ x ⊔ y
          apply @le_sup_right _ _ x y
        . -- x ⊔ y ≤ (x ⊔ y) ⊔ z
          apply le_sup_left
      . -- z ≤ (x ⊔ y) ⊔ z
        apply le_sup_right

-- 3ª demostración
-- ===============

example : x ⊔ y ⊔ z = x ⊔ (y ⊔ z) :=
by
  apply le_antisymm
  · apply sup_le
    · apply sup_le
      . apply le_sup_left
      · apply le_trans
        . apply @le_sup_left _ _ y z
        . apply le_sup_right
    . apply le_trans
      . apply @le_sup_right _ _ y z
      . apply le_sup_right
  . apply sup_le
    · apply le_trans
      . apply @le_sup_left _ _ x y
      . apply le_sup_left
    . apply sup_le
      · apply le_trans
        . apply @le_sup_right _ _ x y
        . apply le_sup_left
      . apply le_sup_right

-- 4ª demostración
-- ===============

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
by
  apply le_antisymm
  . -- (x ⊔ y) ⊔ z ≤ x ⊔ (y ⊔ z)
    apply sup_le
    . -- x ⊔ y ≤ x ⊔ (y ⊔ z)
      apply sup_le le_sup_left (le_sup_of_le_right le_sup_left)
    . -- z ≤ x ⊔ (y ⊔ z)
      apply le_sup_of_le_right le_sup_right
  . -- x ⊔ (y ⊔ z) ≤ (x ⊔ y) ⊔ z
    apply sup_le
    . -- x ≤ (x ⊔ y) ⊔ z
      apply le_sup_of_le_left le_sup_left
    . -- y ⊔ z ≤ (x ⊔ y) ⊔ z
      apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right

-- 5ª demostración
-- ===============

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
by
  apply le_antisymm
  . apply sup_le
    . apply sup_le le_sup_left (le_sup_of_le_right le_sup_left)
    . apply le_sup_of_le_right le_sup_right
  . apply sup_le
    . apply le_sup_of_le_left le_sup_left
    . apply sup_le (le_sup_of_le_left le_sup_right) le_sup_right

-- 6ª demostración
-- ===============

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
le_antisymm
  (sup_le
    (sup_le le_sup_left (le_sup_of_le_right le_sup_left))
    (le_sup_of_le_right le_sup_right))
  (sup_le
    (le_sup_of_le_left le_sup_left)
    (sup_le (le_sup_of_le_left le_sup_right) le_sup_right))

-- 7ª demostración
-- ===============

example : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) :=
-- by apply?
sup_assoc

-- Lemas usados
-- ============

-- #check (le_antisymm : x ≤ y → y ≤ x → x = y)
-- #check (le_sup_left : x ≤ x ⊔ y)
-- #check (le_sup_of_le_left : z ≤ x → z ≤ x ⊔ y)
-- #check (le_sup_of_le_right : z ≤ y → z ≤ x ⊔ y)
-- #check (le_sup_right : y ≤ x ⊔ y)
-- #check (le_trans : x ≤ y → y ≤ z → x ≤ z)
-- #check (sup_assoc : (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z))
-- #check (sup_le : x ≤ z → y ≤ z → x ⊔ y ≤ z)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 21.