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 |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
De la hipótesis, por la monotonia de la suma, se tiene
\[a + d \leq a + f\]
que, por la monotonía de la exponencial, da
\[e^{a + d} \leq e^{a + f}\]
y, por la monotonía de la suma, se tiene
\[c + e^{a + d} \leq c + e^{a + f}\]
2ª demostración en LN
Tenemos que demostrar que
\[c + e^{a + d} \leq c + e^{a + f}\]
Por la monotonía de la suma, se reduce a
\[e^{a + d} \leq e^{a + f}\]
que, por la monotonía de la exponencial, se reduce a
\[a + d \leq a + f\]
que, por la monotonía de la suma, se reduce a
\[d \leq f\]
que es la hipótesis.
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 |
import Mathlib.Analysis.SpecialFunctions.Log.Basic open Real variable (a c d f : ℝ) -- 1ª demostración example (h : d ≤ f) : c + exp (a + d) ≤ c + exp (a + f) := by have h1 : a + d ≤ a + f := add_le_add_left h a have h2 : exp (a + d) ≤ exp (a + f) := exp_le_exp.mpr h1 show c + exp (a + d) ≤ c + exp (a + f) exact add_le_add_left h2 c -- 2ª demostración example (h : d ≤ f) : c + exp (a + d) ≤ c + exp (a + f) := by apply add_le_add_left apply exp_le_exp.mpr apply add_le_add_left exact h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 15.
