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 |
Read More «En ℝ, si 2a ≤ 3b, 1 ≤ a y c = 2, entonces c + a ≤ 5b»
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 |
Read More «En ℝ, si a ≤ b, b < c, c ≤ d y d < e, entonces a < e"
Demostrar con Lean4 que los números reales tienen la siguiente propiedad
|
1 |
(c * b) * a = b * (a * c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c : ℝ) : (c * b) * a = b * (a * c) := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades:
\begin{align}
(cb)a
&= (bc)a &&\text{[por la conmutativa]} \\
&= b(ca) &&\text{[por la asociativa]} \\
&= b(ac) &&\text{[por la conmutativa]}
\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 25 26 27 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic -- 1ª demostración example (a b c : ℝ) : (c * b) * a = b * (a * c) := calc (c * b) * a = (b * c) * a := by rw [mul_comm c b] _ = b * (c * a) := by rw [mul_assoc] _ = b * (a * c) := by rw [mul_comm c a] -- 2ª demostración example (a b c : ℝ) : (c * b) * a = b * (a * c) := by rw [mul_comm c b] rw [mul_assoc] rw [mul_comm c a] -- 3ª demostración example (a b c : ℝ) : (c * b) * a = b * (a * c) := by ring |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
Demostrar con Lean4 que los números reales tienen la siguiente propiedad
|
1 |
(a * b) * c = b * (a * c) |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic example (a b c : ℝ) : (a * b) * c = b * (a * c) := by sorry |
Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align*}
(ab)c &= (ba)c &&\text{[por la conmutativa]} \\
&= b(ac) &&\text{[por la asociativa]}
\end{align*}
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 |
import Mathlib.Tactic import Mathlib.Data.Real.Basic -- 1ª demostración example (a b c : ℝ) : (a * b) * c = b * (a * c) := calc (a * b) * c = (b * a) * c := by rw [mul_comm a b] _ = b * (a * c) := by rw [mul_assoc b a c] -- 2ª demostración example (a b c : ℝ) : (a * b) * c = b * (a * c) := by rw [mul_comm a b] rw [mul_assoc b a c] -- 3ª demostración example (a b c : ℝ) : (a * b) * c = b * (a * c) := by ring |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
Demostrar que el producto de dos funciones no negativas es no negativa.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.real.basic variables (f g : ℝ → ℝ) def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x example (nnf : no_negativa f) (nng : no_negativa g) : no_negativa (f * g) := sorry |
Read More «El producto de dos funciones no negativas es no negativa»
Demostrar que la suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.real.basic -- (cota_inferior f a) se verifica si a es una cota inferior de f. def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variables (f g : ℝ → ℝ) variables (a b : ℝ) example (hfa : cota_inferior f a) (hgb : cota_inferior g b) : cota_inferior (λ x, f x + g x) (a + b) := sorry |
Read More «La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g»
Demostrar que la suma de una cota superior de f y una cota superior de g es una cota superior de f+g.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.real.basic -- (cota_superior f a) se verifica si a es una cota superior de f. def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variables (f g : ℝ → ℝ) variables (a b : ℝ) example (hfa : cota_superior f a) (hgb : cota_superior g b) : cota_superior (λ x, f x + g x) (a + b) := sorry |
Read More «La suma de una cota superior de f y una cota superior de g es una cota superior de f+g»
Demostrar que si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.real.basic tactic example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := sorry |
Read More «Si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε"
Sean a y b números reales. Demostrar que
|
1 |
|a| - |b| ≤ |a - b| |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import data.real.basic variables a b : ℝ example : |a| - |b| ≤ |a - b| := sorry |
Sean a, b y c números reales. Demostrar que
|
1 |
min a b + c = min (a + c) (b + c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.real.basic variables a b c : ℝ example : min a b + c = min (a + c) (b + c) := sorry |
Read More «Si a, b, c ∈ ℝ, entonces min a b + c = min (a + c) (b + c)»