En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f)
Demostrar con Lean4 que si \(a\), \(c\), \(d\) y \(f\) son números reales tales que \(d ≤ f\), entonces
\[c + e^{a + d} \leq c + e^{a + f}\]
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 c d f : ℝ) example (h : d ≤ f) : c + exp (a + d) ≤ c + exp (a + f) := by sorry |
Read More «En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f)»