Demostrar que si f es monótona y c ≥ 0, entonces c·f es monótona.
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 : ℝ → ℝ) variable {c : ℝ} example (mf : monotone f) (nnc : 0 ≤ c) : monotone (λ x, c * f x) := sorry |
Read More «Si f es monótona y c ≥ 0, entonces c·f es monótona»
Demostrar que la suma de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import data.real.basic variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (f + g) := sorry |
Demostrar 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 a·b 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 15 16 17 18 |
import data.real.basic def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x variables (f g : ℝ → ℝ) variables (a b : ℝ) example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := sorry |
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| < ε"
Demostrar que si X es un espacio métrico y x, y ∈ X, entonces
|
1 |
0 ≤ dist x y |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import topology.metric_space.basic variables {X : Type*} [metric_space X] variables x y : X example : 0 ≤ dist x y := sorry |
Read More «Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0»
Demostrar que si R es un anillo ordenado y a, b, c ∈ R tales que
|
1 2 |
a ≤ b 0 ≤ c |
entonces
|
1 |
a * c ≤ b * c |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b c: R example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := sorry |
Soluciones con Lean
|
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 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b c: R -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := begin have h3 : 0 ≤ b - a := sub_nonneg.mpr h1, have h4 : 0 ≤ (b - a) * c := mul_nonneg h3 h2, have h5 : (b - a) * c = b * c - a * c := sub_mul b a c, have h6 : 0 ≤ b * c - a * c := eq.trans_ge h5 h4, show a * c ≤ b * c, by exact sub_nonneg.mp h6, end -- 2ª demostración -- =============== open_locale classical example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := begin by_cases h3 : b ≤ a, { have h3a : a = b := le_antisymm h1 h3, show a * c ≤ b * c, by rw h3a }, { by_cases h4 : c = 0, { calc a * c = a * 0 : by rw h4 ... = 0 : by rw mul_zero ... ≤ 0 : le_refl 0 ... = b * 0 : by rw mul_zero ... = b * c : by {congr ; rw h4}}, { apply le_of_lt, apply mul_lt_mul_of_pos_right, { show a < b, by exact lt_of_le_not_le h1 h3 }, { show 0 < c, by exact lt_of_le_of_ne h2 (ne.symm h4) }}}, end -- 3ª demostración example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := -- by library_search mul_le_mul_of_nonneg_right h1 h2 |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
Demostrar que si R es un anillo ordenado y a, b ∈ R, entonces
|
1 |
0 ≤ b - a → a ≤ b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : 0 ≤ b - a → a ≤ b := sorry |
Read More «Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b»