28 noviembre 2022 – Calculemus

La suma de dos funciones acotadas superiormente también lo está

PorJosé A. Alonso 28 noviembre 202228 noviembre 2022

Demostrar que la suma de dos funciones acotadas superiormente también lo está.

Para ello, completar la siguiente teoría de Lean:

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

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