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