En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b
Demostrar con Lean4 que si \(a\), \(b\) y \(c\) son números reales tales que \(2a \leq 3b\), \(1 \leq a\) y \(c = 2\), entonces \(c + a \leq 5b\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Data.Real.Basic variable (a b c : ℝ) example (h1 : 2 * a ≤ 3 * b) (h2 : 1 ≤ a) (h3 : c = 2) : c + a ≤ 5 * b := sorry |
Demostración en lenguaje natural
Por la siguiente cadena de desigualdades
\begin{align}
c + a &= 2 + a &&\text{[por la hipótesis 3 (\(c = 2\))]} \\
&\leq 2·a + a &&\text{[por la hipótesis 2 (\(1 \leq a\))]} \\
&= 3·a \\
&\leq 9/2·b &&\text{[por la hipótesis 1 (\(2·a \leq 3·b\))]} \\
&\leq 5·b
\end{align}
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 |
import Mathlib.Data.Real.Basic variable (a b c : ℝ) -- 1ª demostración example (h1 : 2 * a ≤ 3 * b) (h2 : 1 ≤ a) (h3 : c = 2) : c + a ≤ 5 * b := calc c + a = 2 + a := by rw [h3] _ ≤ 2 * a + a := by linarith only [h2] _ = 3 * a := by linarith only [] _ ≤ 9/2 * b := by linarith only [h1] _ ≤ 5 * b := by linarith -- 2ª demostración example (h1 : 2 * a ≤ 3 * b) (h2 : 1 ≤ a) (h3 : c = 2) : c + a ≤ 5 * b := 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.
