En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b)
Demostrar con Lean4 que si \(a\) y \(b\) son números reales tales que \(a \leq b\), entonces
\[\log(1+e^a) \leq \log(1+e^b)\]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b : ℝ) example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by sorry |
Read More «En ℝ, si a ≤ b, entonces log(1+e^a) ≤ log(1+e^b)»