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 |
Read More «La suma de dos funciones acotadas superiormente también lo está»