En ℝ, min(min(a,b),c) = min(a,min(b,c))
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:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min (min a b) c = min a (min b c) := by sorry |
Demostración en lenguaje natural
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.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
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 |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 18.
