En ℝ, max(a,b) = max(b,a)
Demostrar con Lean4 que si \(a\) y \(b\) son números reales, entonces \(\max(a, b) = \max(b, a)\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : max a b = max b a := by sorry |
Demostración en lenguaje natural
Es consecuencia de la siguiente propiedad
\[\max(a, b) \leq \max(b, a) \tag{1}\]
En efecto, intercambiando las variables en (1) se obtiene
\[\max(b, a) \leq \max(a, b) \tag{2}\]
Finalmente de (1) y (2) se obtiene
\[\max(b, a) = \max(a, b)\]
Para demostrar (1), se observa que
\begin{align}
a &\leq \max(b, a) \\
b &\leq \max(b, a)
\end{align}
y, por tanto,
\[\max(a, b) \leq \max(b, a)\]
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 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) -- Lema auxiliar -- ============= -- 1ª demostración del lema auxiliar -- ================================= example : max a b ≤ max b a := by have h1 : a ≤ max b a := le_max_right b a have h2 : b ≤ max b a := le_max_left b a show max a b ≤ max b a exact max_le h1 h2 -- 2ª demostración del lema auxiliar -- ================================= example : max a b ≤ max b a := by apply max_le { apply le_max_right } { apply le_max_left } -- 3ª demostración del lema auxiliar -- ================================= lemma aux : max a b ≤ max b a := by exact max_le (le_max_right b a) (le_max_left b a) -- 1ª demostración -- =============== example : max a b = max b a := by apply le_antisymm { exact aux a b} { exact aux b a} -- 2ª demostración -- =============== example : max a b = max b a := le_antisymm (aux a b) (aux b a) -- 3ª demostración -- =============== example : max a b = max b a := max_comm a b |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 17.
