Menu Close

Día: 7 noviembre 2022

Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g

José A. Alonso-

Demostrar que si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g.

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

import data.real.basic
 
def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop :=
∀ x, f x ≤ a
 
def no_negativa (f : ℝ → ℝ) : Prop :=
∀ x, 0 ≤ f x
 
variables (f g : ℝ → ℝ)
variables (a b : ℝ)
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0 ≤ a)
  : cota_superior (f * g) (a * b) :=
sorry
Soluciones →