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