--- Título: En ℝ, si d ≤ f, entonces c + e^(a + d) ≤ c + e^(a + f) Autor: José A. Alonso --- 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:

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) [mathjax] 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

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.