Menu Close

Día: 3 de noviembre de 2022

La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g

Demostrar que la suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g.

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

import data.real.basic
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f :   ) (a : ) : Prop :=
 x, a  f x
 
variables (f g :   )
variables (a b : )
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
sorry