29 noviembre 2022 – Calculemus

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

PorJosé A. Alonso 29 noviembre 2022

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

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

import data.real.basic

variables {f g : ℝ → ℝ}
variables {a b : ℝ}

-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

-- (acotada_inf f) se verifica si f tiene cota inferior.
def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a

example
  (hf : acotada_inf f)
  (hg : acotada_inf g)
  : acotada_inf (f + g) :=
sorry

import data.real.basic

variables {f g : ℝ → ℝ}

variables {a b : ℝ}

-- (cota_inferior f a) se verifica si a es una cota inferior de f.

def cota_inferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x

-- (acotada_inf f) se verifica si f tiene cota inferior.

def acotada_inf (f : ℝ → ℝ) := ∃ a, cota_inferior f a

example

(hf : acotada_inf f)

(hg : acotada_inf g)

: acotada_inf (f + g) :=

sorry