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 |
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 |
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»
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»
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»
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| < ε"
Demostrar con Lean4 que en los espacios métricos, \(d(x,y) ≥ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Topology.MetricSpace.Basic variable {X : Type _} [MetricSpace X] variable (x y : X) example : 0 ≤ d x y := by sorry |
Demostrar con Lean4 que, en los anillos ordenados,
\[ \{a ≤ b, 0 ≤ c\} ⊢ ac ≤ bc \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := by sorry |
Read More «En los anillos ordenados, {a ≤ b, 0 ≤ c} ⊢ ac ≤ bc»
Demostrar con Lean4 que en los anillos ordenados
\[ 0 ≤ b – a → a ≤ b \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : 0 ≤ b - a → a ≤ b := by sorry |
Demostrar con Lean4 que en los anillos ordenados se verifica que
\[ a ≤ b → 0 ≤ b – a \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Algebra.Order.Ring.Defs variable {R : Type _} [StrictOrderedRing R] variable (a b c : R) example : a ≤ b → 0 ≤ b - a := by sorry |