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
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 |
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 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 |
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 : ℝ) -- 1ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin have h1 : ∀ x, f x * g x ≤ a * b, { intro x, have h2 : f x ≤ a := hfa x, have h3 : g x ≤ b := hgb x, have h4 : 0 ≤ g x := nng x, show f x * g x ≤ a * b, by exact mul_le_mul h2 h3 h4 nna, }, show cota_superior (f * g) (a * b), by exact h1, end -- 2ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin intro x, change f x * g x ≤ a * b, apply mul_le_mul, apply hfa, apply hgb, apply nng, apply nna end -- 3ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin dunfold cota_superior no_negativa at *, intro x, have h1:= hfa x, have h2:= hgb x, have h3:= nng x, exact mul_le_mul h1 h2 h3 nna, end -- 4ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := begin dunfold cota_superior no_negativa at *, intro x, specialize hfa x, specialize hgb x, specialize nng x, exact mul_le_mul hfa hgb nng nna, end -- 5ª demostración -- =============== example (hfa : cota_superior f a) (hgb : cota_superior g b) (nng : no_negativa g) (nna : 0 ≤ a) : cota_superior (f * g) (a * b) := λ x, mul_le_mul (hfa x) (hgb x) (nng x) nna |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 27.
