31 octubre 2023 – Calculemus

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

PorJosé A. Alonso 31 octubre 202330 octubre 2023

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

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

import src.Suma_de_cotas_inferiores
variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.
def acotadaInf (f : ℝ → ℝ) :=
  ∃ a, CotaInferior f a

example
  (hf : acotadaInf f)
  (hg : acotadaInf g)
  : acotadaInf (f + g) :=
by sorry

import src.Suma_de_cotas_inferiores

variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.

def acotadaInf (f : ℝ → ℝ) :=

∃ a, CotaInferior f a

example

(hf : acotadaInf f)

(hg : acotadaInf g)

: acotadaInf (f + g) :=

by sorry