En ℝ, min(a,b) = min(b,a)
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces \(\min(a, b) = \min(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 : min a b = min b a := by sorry |
Demostración en lenguaje natural
Es consecuencia de la siguiente propiedad
\[\min(a, b) \leq \min(b, a) \tag{1}\]
En efecto, intercambiando las variables en (1) se obtiene
\[\min(b, a) \leq \min(a, b) \tag{2}\]
Finalmente de (1) y (2) se obtiene
\[\min(b, a) = \min(a, b)\]
Para demostrar (1), se observa que
\begin{align}
\min(a, b) &\leq b \\
\min(a, b) &\leq a
\end{align}
y, por tanto,
\[\min(a, b) \leq \min(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 : min a b ≤ min b a := by have h1 : min a b ≤ b := min_le_right a b have h2 : min a b ≤ a := min_le_left a b show min a b ≤ min b a exact le_min h1 h2 -- 2ª demostración del lema auxiliar -- ================================= example : min a b ≤ min b a := by apply le_min { apply min_le_right } { apply min_le_left } -- 3ª demostración del lema auxiliar -- ================================= lemma aux : min a b ≤ min b a := by exact le_min (min_le_right a b) (min_le_left a b) -- 1ª demostración -- =============== example : min a b = min b a := by apply le_antisymm { exact aux a b} { exact aux b a} -- 2ª demostración -- =============== example : min a b = min b a := le_antisymm (aux a b) (aux b a) -- 3ª demostración -- =============== example : min a b = min b a := min_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.
