La suma de dos funciones acotadas superiormente también lo está
Demostrar con Lean4 que la suma de dos funciones acotadas superiormente también lo está.
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 11 12 |
import src.Suma_de_cotas_superiores variable {f g : ℝ → ℝ} -- (acotadaSup f) afirma que f tiene cota superior. def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a example (hf : acotadaSup f) (hg : acotadaSup g) : acotadaSup (f + g) := by sorry |
Read More «La suma de dos funciones acotadas superiormente también lo está»