---
Título: En ℝ, min(min(a,b),c) = min(a,min(b,c))
Autor:  José A. Alonso
---

Demostrar con Lean4 que \(a\), \(b\) y \(c\) números reales, entonces \(\min(\min(a, b), c) = \min(a, \min(b, c))\).

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

<pre lang="lean">
import Mathlib.Data.Real.Basic

variable {a b c : ℝ}

example :
  min (min a b) c = min a (min b c) :=
by sorry
</pre>
<!--more-->

<b>Demostración en lenguaje natural</b>

[mathjax]
Por la propiedad antisimétrica, la igualdad es consecuencia de las siguientes desigualdades
\begin{align}
   \min(\min(a, b), c) &\leq \min(a, \min(b, c)) \tag{1} \\
   \min(a, \min(b, c)) &\leq \min(\min(a, b), c) \tag{2}
\end{align}

La (1) es consecuencia de las siguientes desigualdades
\begin{align}
   \min(\min(a, b), c) &\leq a \tag{1a} \\
   \min(\min(a, b), c) &\leq b \tag{1b} \\
   \min(\min(a, b), c) &\leq c \tag{1c}
\end{align}
En efecto, de (1b) y (1c) se obtiene
\[ \min(\min(a, b), c) \leq \min(b,c) \]
que, junto con (1a) da (1).

La (2) es consecuencia de las siguientes desigualdades
\begin{align}
   \min(a, \min(b, c)) &\leq a \tag{2a} \\
   \min(a, \min(b, c)) &\leq b \tag{2b} \\
   \min(a, \min(b, c)) &\leq c \tag{2c}
\end{align}
En efecto, de (2a) y (2b) se obtiene
\[ \min(a, \min(b, c)) \leq \min(a, b) \]
que, junto con (2c) da (2).

La demostración de (1a) es
\[ \min(\min(a, b), c) \leq \min(a, b) \leq a \]
La demostración de (1b) es
\[ \min(\min(a, b), c) \leq \min(a, b) \leq b \]
La demostración de (2b) es
\[ \min(a, \min(b, c)) \leq \min(b, c) \leq b \]
La demostración de (2c) es
\[ \min(a, \min(b, c)) \leq \min(b, c) \leq c \]
La (1c) y (2a) son inmediatas.

<b>Demostraciones con Lean4</b>

<pre lang="lean">
import Mathlib.Data.Real.Basic

variable {a b c : ℝ}

-- Lemas auxiliares
-- ================

lemma aux1a : min (min a b) c ≤ a :=
calc min (min a b) c
     ≤ min a b := by exact min_le_left (min a b) c
   _ ≤ a       := min_le_left a b

lemma aux1b : min (min a b) c ≤ b :=
calc min (min a b) c
     ≤ min a b := by exact min_le_left (min a b) c
   _ ≤ b       := min_le_right a b

lemma aux1c : min (min a b) c ≤ c :=
by exact min_le_right (min a b) c

-- 1ª demostración del lema aux1
lemma aux1 : min (min a b) c ≤ min a (min b c) :=
by
  apply le_min
  { show min (min a b) c ≤ a
    exact aux1a }
  { show min (min a b) c ≤ min b c
    apply le_min
    { show min (min a b) c ≤ b
      exact aux1b }
    { show min (min a b) c ≤ c
      exact aux1c }}

-- 2ª demostración del lema aux1
lemma aux1' : min (min a b) c ≤ min a (min b c) :=
le_min aux1a (le_min aux1b aux1c)

lemma aux2a : min a (min b c) ≤ a :=
by exact min_le_left a (min b c)

lemma aux2b : min a (min b c) ≤ b :=
calc min a (min b c)
     ≤ min b c        := by exact min_le_right a (min b c)
   _ ≤ b              := min_le_left b c

lemma aux2c : min a (min b c) ≤ c :=
calc min a (min b c)
     ≤ min b c        := by exact min_le_right a (min b c)
   _ ≤ c              := min_le_right b c

-- 1ª demostración del lema aux2
lemma aux2 : min a (min b c) ≤ min (min a b) c :=
by
  apply le_min
  { show min a (min b c) ≤ min a b
    apply le_min
    { show min a (min b c) ≤ a
      exact aux2a }
    { show min a (min b c) ≤ b
      exact aux2b }}
  { show min a (min b c) ≤ c
    exact aux2c }

-- 2ª demostración del lema aux2
lemma aux2' : min a (min b c) ≤ min (min a b) c :=
le_min (le_min aux2a aux2b) aux2c

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

example :
  min (min a b) c = min a (min b c) :=
by
  apply le_antisymm
  { show min (min a b) c ≤ min a (min b c)
    exact aux1 }
  { show min a (min b c) ≤ min (min a b) c
    exact aux2 }

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

example : min (min a b) c = min a (min b c) :=
by
  apply le_antisymm
  { exact aux1 }
  { exact aux2 }

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

example : min (min a b) c = min a (min b c) :=
le_antisymm aux1 aux2


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

example : min (min a b) c = min a (min b c) :=
min_assoc a b c
</pre>

<b>Demostraciones interactivas</b>

Se puede interactuar con las demostraciones anteriores en <a href="https://lean.math.hhu.de/#url=https://raw.githubusercontent.com/jaalonso/Calculemus2/main/src/Asociatividad_del_minimo.lean" rel="noopener noreferrer" target="_blank">Lean 4 Web</a>.

<b>Referencias</b>

<ul>
<li> J. Avigad y P. Massot. <a href="https://bit.ly/3U4UjBk">Mathematics in Lean</a>, p. 18.</li>
</ul>