Processing math: 100%
Skip to main content

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≤b, entonces c−eb≤c−ea

Para ello, completar la siguiente teoría de Lean4:

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 ea≤eb y, restando de c, se invierte la desigualdad c−eb≤c−ea

Demostraciones con Lean4

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