21 septiembre 2022 – Calculemus

Si a, b, d ∈ ℝ tales que 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ

PorJosé A. Alonso 21 septiembre 202211 septiembre 2022

Demostrar que si a, b, d ∈ ℝ tales que $1 \leq a$ y $b \leq d$ , entonces $2 + a + e^b \leq 3a + e^d$ .

Para ello, completar la siguiente teoría de Lean:

import analysis.special_functions.log.basic
open real
variables a b d : ℝ

example
  (h  : 1 ≤ a)
  (h' : b ≤ d)
  : 2 + a + exp b ≤ 3 * a + exp d :=
sorry

import analysis.special_functions.log.basic

open real

variables a b d : ℝ

example

(h : 1 ≤ a)

(h' : b ≤ d)

: 2 + a + exp b ≤ 3 * a + exp d :=

sorry

Nota: Se pueden usar los lemas

add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d
exp_le_exp : exp a ≤ exp b ↔ a ≤ b

1 2	add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d exp_le_exp : exp a ≤ exp b ↔ a ≤ b