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 |
Demostración en lenguaje natural
Aplicando la monotonía de la exponencial a la hipótesis, se tiene
\[e^a \leq e^b\]
y, restando de \(c\), se invierte la desigualdad
\[c – e^b ≤ c – e^a\]
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a b c : ℝ) -- 1ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := by have h1 : exp a ≤ exp b := exp_le_exp.mpr h show c - exp b ≤ c - exp a exact sub_le_sub_left h1 c -- 2ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := by apply sub_le_sub_left _ c apply exp_le_exp.mpr h -- 3ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := sub_le_sub_left (exp_le_exp.mpr h) c -- 4ª demostración example (h : a ≤ b) : c - exp b ≤ c - exp a := by linarith [exp_le_exp.mpr h] |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 16.
