Si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ
Demostrar que si a, b, c ∈ ℝ tales que a ≤ b, entonces c – eᵇ ≤ c – eᵃ.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 |
import analysis.special_functions.log.basic import tactic open real variables a b c : ℝ example (h : a ≤ b) : c - exp b ≤ c - exp a := 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 |
import analysis.special_functions.log.basic import tactic open real variables a b c : ℝ -- 1ª demostración -- =============== example (h : a ≤ b) : c - exp b ≤ c - exp a := begin apply sub_le_sub_left _ c, exact exp_le_exp.mpr h, end -- 2ª demostración -- =============== example (h : a ≤ b) : c - exp b ≤ c - exp a := sub_le_sub_left (exp_le_exp.mpr h) c -- 3ª demostración -- =============== example (h : a ≤ b) : c - b ≤ c - a := -- by library_search sub_le_sub_left h c -- 4ª demostración -- =============== example (h : a ≤ b) : c - exp b ≤ c - exp a := by linarith [exp_le_exp.mpr h] -- 5ª demostración -- =============== example (h : a ≤ b) : c - exp b ≤ c - exp a := -- by hint by finish |
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. 17.