Skip to main content

En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e

Demostrar con Lean4 que si \(a\), \(b\), \(c\), \(d\) y \(e\) son números reales tales \(a \leq b\), \(b < c\), \(c \leq d\) y \(d < e\), entonces \(a < e\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c d e : ℝ)

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
sorry

Demostraciones en lenguaje natural (LN)

1ª demostración en LN

Por la siguiente cadena de desigualdades \begin{align} a &\leq b &&\text{[por la hipótesis 1 (\(a \leq b\))]} \\ &< c &&\text{[por la hipótesis 2 (\(b < c\))]} \\ &\leq d &&\text{[por la hipótesis 3 (\(c \leq d\))]} \\ &< e &&\text{[por la hipótesis 4 (\(d < e\))]} \end{align}

2ª demostración en LN

A partir de las hipótesis 1 (\(a \leq b\)) y 2 (\(b < c\)) se tiene \[a < c\] que, junto la hipótesis 3 (\(c \leq d\)) da \[a < d\] que, junto la hipótesis 4 (\(d < e\)) da \[a < e.\]

3ª demostración en LN

Demostrar \(a < e\), por la hipótesis 1 (\(a \leq b\)) se reduce a \[b < e\] que, por la hipótesis 2 (\(b < c\)), se reduce a \[c < e\] que, por la hipótesis 3 (\(c \leq d\)), se reduce a \[d < e\] que es cierto, por la hipótesis 4.

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c d e : ℝ)

-- 1ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
calc
  a ≤ b := h1
  _ < c := h2
  _ ≤ d := h3
  _ < e := h4

-- 2ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
by
  have h5 : a < c := lt_of_le_of_lt h1 h2
  have h6 : a < d := lt_of_lt_of_le h5 h3
  show a < e
  exact lt_trans h6 h4

-- 3ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
by
  apply lt_of_le_of_lt h1
  apply lt_trans h2
  apply lt_of_le_of_lt h3
  exact h4

-- El desarrollo de la prueba es
--
--    a b c d e : ℝ,
--    h1 : a ≤ b,
--    h2 : b < c,
--    h3 : c ≤ d,
--    h4 : d < e
--    ⊢ a < e
-- apply lt_of_le_of_lt h1,
--    ⊢ b < e
-- apply lt_trans h2,
--    ⊢ c < e
-- apply lt_of_le_of_lt h3,
--    ⊢ d < e
-- exact h4,
--    no goals

-- 4ª demostración
-- ===============

example
  (h1 : a ≤ b)
  (h2 : b < c)
  (h3 : c ≤ d)
  (h4 : d < e) :
  a < e :=
by linarith

-- Lemas usados
-- ============

-- #check (lt_of_le_of_lt : a ≤ b → b < c → a < c)
-- #check (lt_of_lt_of_le : a < b → b ≤ c → a < c)
-- #check (lt_trans : a < b → b < c → a < c)

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias