El producto de dos funciones no negativas es no negativa
Demostrar que el producto de dos funciones no negativas es no negativa.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
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 |
Read More «El producto de dos funciones no negativas es no negativa»