Si a, b, c ∈ ℝ, entonces min(min(a,b),c) = min(a,min(b,c))
Sean a, b y c números reales. Demostrar que
1 |
min (min a b) c = min a (min b c) |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 |
import data.real.basic tactic variables a b c : ℝ example : min (min a b) c = min a (min b c) := sorry |
Soluciones con Lean
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 |
import data.real.basic tactic variables a b c : ℝ -- 1ª demostración -- =============== -- Se usará el siguiente lema auxilar. lemma aux1 : min (min a b) c ≤ min a (min b c) := begin apply le_min, { show min (min a b) c ≤ a, calc min (min a b) c ≤ min a b : min_le_left (min a b) c ... ≤ a : min_le_left a b }, { show min (min a b) c ≤ min b c, apply le_min, { show min (min a b) c ≤ b, calc min (min a b) c ≤ min a b : min_le_left (min a b) c ... ≤ b : min_le_right a b }, { show min (min a b) c ≤ c, { by exact min_le_right (min a b) c }}}, end example : min (min a b) c = min a (min b c) := begin apply le_antisymm, { show min (min a b) c ≤ min a (min b c), by exact aux1 a b c }, { show min a (min b c) ≤ min (min a b) c, calc min a (min b c) = min (min b c) a : by apply min_comm ... = min (min c b) a : by {congr' 1, apply min_comm} ... ≤ min c (min b a) : by apply aux1 ... = min c (min a b) : by {congr' 1, apply min_comm} ... = min (min a b) c : by apply min_comm }, end -- 2ª demostración -- =============== -- Se usará el siguiente lema auxilar. lemma aux2 : min (min a b) c ≤ min a (min b c) := begin apply le_min, { calc min (min a b) c ≤ min a b : by simp [min_le_left] ... ≤ a : by simp [min_le_left] }, { apply le_min, { calc min (min a b) c ≤ min a b : by simp [min_le_left] ... ≤ b : by simp [min_le_right] }, { simp [min_le_right] }}, end example : min (min a b) c = min a (min b c) := begin apply le_antisymm, { by exact aux2 a b c }, { calc min a (min b c) = min (min b c) a : by simp [min_comm] ... = min (min c b) a : by simp [min_comm] ... ≤ min c (min b a) : by simp [aux2] ... = min c (min a b) : by simp [min_comm] ... = min (min a b) c : by simp [min_comm] }, end -- 3ª demostración -- =============== example : min (min a b) c = min a (min b c) := begin apply le_antisymm, { by exact aux2 a b c }, { calc min a (min b c) = min (min c b) a : by simp [min_comm] ... ≤ min c (min b a) : by simp [aux2] ... = min (min a b) c : by simp [min_comm] }, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 19.