Si a, b, c ∈ ℝ, entonces min a b + c = min (a + c) (b + c)
Sean a, b y c números reales. Demostrar que
|
1 |
min a b + c = min (a + c) (b + c) |
Para ello, completar la siguiente teoría de Lean:
Lean
|
1 2 3 4 5 6 7 |
import data.real.basic variables a b c : ℝ example : min a b + c = min (a + c) (b + c) := sorry |
Soluciones con Lean
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 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 |
import data.real.basic variables a b c : ℝ -- 1ª demostración -- =============== lemma aux1a : min a b + c ≤ min (a + c) (b + c) := begin have h1 : min a b ≤ a := min_le_left a b, have h2 : min a b + c ≤ a + c := add_le_add_right h1 c, have h3 : min a b ≤ b := min_le_right a b, have h4 : min a b + c ≤ b + c := add_le_add_right h3 c, show min a b + c ≤ min (a + c) (b + c), by exact le_min h2 h4, end lemma aux2a : min (a + c) (b + c) ≤ min a b + c := begin have h1 : min (a + c) (b + c) + -c ≤ min a b, { calc min (a + c) (b + c) + -c ≤ min (a + c + -c) (b + c + -c) : aux1a (a + c) (b + c) (-c) ... = min a b : by ring_nf }, show min (a + c) (b + c) ≤ min a b + c, by exact add_neg_le_iff_le_add.mp h1, end example : min a b + c = min (a + c) (b + c) := begin apply le_antisymm, { exact aux1a a b c, }, { exact aux2a a b c, }, end -- 2ª demostración -- =============== lemma aux1b : min a b + c ≤ min (a + c) (b + c) := begin apply le_min, { apply add_le_add_right, exact min_le_left a b, }, { apply add_le_add_right, exact min_le_right a b, }, end lemma aux2b : min (a + c) (b + c) ≤ min a b + c := begin have h1 : min (a + c) (b + c) + -c ≤ min a b, { calc min (a + c) (b + c) + -c ≤ min (a + c + -c) (b + c + -c) : aux1b (a + c) (b + c) (-c) ... = min a b : by ring_nf }, exact add_neg_le_iff_le_add.mp h1, end example : min a b + c = min (a + c) (b + c) := begin apply le_antisymm, { exact aux1b a b c, }, { exact aux2b a b c, }, end -- 3ª demostración -- =============== lemma aux1c : min a b + c ≤ min (a + c) (b + c) := le_min (add_le_add_right (min_le_left a b) c) (add_le_add_right (min_le_right a b) c) lemma aux2c : min (a + c) (b + c) ≤ min a b + c := begin have h1 : min (a + c) (b + c) + -c ≤ min a b, { calc min (a + c) (b + c) + -c ≤ min (a + c + -c) (b + c + -c) : aux1c (a + c) (b + c) (-c) ... = min a b : by ring_nf }, exact add_neg_le_iff_le_add.mp h1, end example : min a b + c = min (a + c) (b + c) := le_antisymm (aux1b a b c) (aux2b a b c) -- 4ª demostración -- =============== example : min a b + c = min (a + c) (b + c) := begin by_cases (a ≤ b), { have h1 : a + c ≤ b + c, apply add_le_add_right h, calc min a b + c = a + c : by simp [min_eq_left h] ... = min (a + c) (b + c) : by simp [min_eq_left h1]}, { have h2: b ≤ a, linarith, have h3 : b + c ≤ a + c, { exact add_le_add_right h2 c }, calc min a b + c = b + c : by simp [min_eq_right h2] ... = min (a + c) (b + c) : by simp [min_eq_right h3]}, end -- 5ª demostración -- =============== example : min a b + c = min (a + c) (b + c) := (min_add_add_right a b c).symm |
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. 20.
