La suma de dos funciones acotadas superiormente también lo está
Demostrar que la suma de dos funciones acotadas superiormente también lo está.
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 |
import data.real.basic variables {f g : ℝ → ℝ} variables {a b : ℝ} -- (cota_superior f a) se verifica si a es una cota superior de f. def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a -- (acotada_sup f) afirma que f tiene cota superior. def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a example (hf : acotada_sup f) (hg : acotada_sup g) : acotada_sup (f + g) := 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 |
import data.real.basic variables {f g : ℝ → ℝ} variables {a b : ℝ} -- (cota_superior f a) se verifica si a es una cota superior de f. def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a -- (acotada_sup f) afirma que f tiene cota superior. def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a -- Lema auxiliar -- ============= lemma cota_superior_suma (hfa : cota_superior f a) (hgb : cota_superior g b) : cota_superior (f + g) (a + b) := λ x, add_le_add (hfa x) (hgb x) -- 1ª demostración -- =============== example (hf : acotada_sup f) (hg : acotada_sup g) : acotada_sup (f + g) := begin cases hf with a hfa, cases hg with b hgb, have h3 : cota_superior (f + g) (a + b) := cota_superior_suma hfa hgb, have h4 : ∃ z, ∀ x, (f + g) x ≤ z, by exact Exists.intro (a + b) h3, show acotada_sup (f + g), by exact h4, end -- 2ª demostración -- =============== example (hf : acotada_sup f) (hg : acotada_sup g) : acotada_sup (f + g) := begin cases hf with a hfa, cases hg with b hfb, use a + b, apply cota_superior_suma hfa hfb, end -- 3ª demostración -- =============== example (hf : acotada_sup f) (hg : acotada_sup g) : acotada_sup (f + g) := begin rcases hf with ⟨a, hfa⟩, rcases hg with ⟨b, hfb⟩, exact ⟨a + b, cota_superior_suma hfa hfb⟩ end -- 4ª demostración -- =============== example : acotada_sup f → acotada_sup g → acotada_sup (f + g) := begin rintros ⟨a, hfa⟩ ⟨b, hfb⟩, exact ⟨a + b, cota_superior_suma hfa hfb⟩, end -- 5ª demostración -- =============== example : acotada_sup f → acotada_sup g → acotada_sup (f + g) := λ ⟨a, hfa⟩ ⟨b, hfb⟩, ⟨a + b, cota_superior_suma hfa hfb⟩ |
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. 31.