Hay algún número real entre 2 y 3
Demostrar con Lean4 que hay algún número real entre 2 y 3.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import Mathlib.Data.Real.Basic example : ∃ x : ℝ, 2 < x ∧ x < 3 := by sorry |
La composición de dos funciones monótonas es monótona
Demostrar con Lean4 que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) example (mf : Monotone f) (mg : Monotone g) : Monotone (f ∘ g) := by sorry |
Read More «La composición de dos funciones monótonas es monótona»
La suma de dos funciones monótonas es monótona
Demostrar con Lean4 que la suma de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) example (mf : Monotone f) (mg : Monotone g) : Monotone (f + g) := by sorry |
Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces ab es una cota superior de fg
Sean \(f\) y \(g\) funciones de \(ℝ\) en \(ℝ\). Demostrar con Lean4 que si \(a\) es una cota superior no negativa de \(f\) y \(b\) es es una cota superior de la función no negativa \(g\), entonces \(ab\) es una cota superior de \(fg\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 |
import Mathlib.Data.Real.Basic -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) (nng : CotaInferior g 0) (nna : 0 ≤ a) : CotaSuperior (f * g) (a * b) := by sorry |
El producto de funciones no negativas es no negativo
Demostrar con Lean4 que si \(f\) y \(g\) son funciones no negativas de \(ℝ\) en \(ℝ\), entonces su producto es no negativo.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) example (nnf : CotaInferior f 0) (nng : CotaInferior g 0) : CotaInferior (f * g) 0 := by sorry |
Read More «El producto de funciones no negativas es no negativo»
La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces 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 Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by sorry |
Read More «La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g»
La suma de una cota superior de f y una cota superior de g es una cota superior de f+g
Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces 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 Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaSuperior f a) (hgb : CotaSuperior g b) : CotaSuperior (f + g) (a + b) := by sorry |
Read More «La suma de una cota superior de f y una cota superior de g es una cota superior de f+g»
En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε
Demostrar con Lean4, que en ℝ
\[ \left\{ 0 < ε, ε ≤ 1, |x| < ε, |y| < ε \right\} ⊢ |xy| < ε \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic example : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by sorry |
Read More «En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε"
En ℝ, |a| – |b| ≤ |a – b|
Demostrar con Lean4 que si \(a\) y \(b\) números reales, entonces
\[|a| – |b| \leq |a – b|\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Data.Real.Basic variable (a b : ℝ) example : |a| - |b| ≤ |a - b| := by sorry |
En ℝ, min(a,b)+c = min(a+c,b+c)
Demostrar con Lean4 que si \(a\), \(b\) y \(c\) números reales, entonces
\[\min(a,b)+c = \min(a+c,b+c)\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {a b c : ℝ} example : min a b + c = min (a + c) (b + c) := by sorry |