José A. AlonsoDemostrar que el producto de dos funciones no negativas es no negativa.
Para ello, completar la siguiente teoría de Lean:
import data.real.basic variables (f g : ℝ → ℝ) def no_negativa (f : ℝ → ℝ) : Prop := ∀ x, 0 ≤ f x example (nnf : no_negativa f) (nng : no_negativa g) : no_negativa (f * g) := sorry |