En ℝ, si 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ
Demostrar con Lean4 que si a, b y d números reales tales que 1≤a y b≤d, entonces 2+a+eb≤3a+ed.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b d : ℝ) example (h1 : 1 ≤ a) (h2 : b ≤ d) : 2 + a + exp b ≤ 3 * a + exp d := by sorry
Demostración en lenguaje natural
De la primera hipótesis (1≤a), multiplicando por 2, se obtiene 2≤2a y, sumando a ambos lados, se tiene 2+a≤3a
De la hipótesis 2 (b≤d) y de la monotonía de la función exponencial se tiene eb≤ed
Finalmente, de (1) y (2) se tiene 2+a+eb≤3a+ed
Demostraciones con Lean4
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b d : ℝ) -- 1ª demostración example (h1 : 1 ≤ a) (h2 : b ≤ d) : 2 + a + exp b ≤ 3 * a + exp d := by have h3 : 2 + a ≤ 3 * a := calc 2 + a = 2 * 1 + a := by linarith only [] _ ≤ 2 * a + a := by linarith only [h1] _ ≤ 3 * a := by linarith only [] have h4 : exp b ≤ exp d := by linarith only [exp_le_exp.mpr h2] show 2 + a + exp b ≤ 3 * a + exp d exact add_le_add h3 h4 -- 2ª demostración example (h1 : 1 ≤ a) (h2 : b ≤ d) : 2 + a + exp b ≤ 3 * a + exp d := calc 2 + a + exp b ≤ 3 * a + exp b := by linarith only [h1] _ ≤ 3 * a + exp d := by linarith only [exp_le_exp.mpr h2] -- 3ª demostración example (h1 : 1 ≤ a) (h2 : b ≤ d) : 2 + a + exp b ≤ 3 * a + exp d := by linarith [exp_le_exp.mpr h2]
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 15.