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:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Data.Real.Basic 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
|
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 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 |
import Mathlib.Data.Real.Basic 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 |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 14.
