José A. AlonsoDemostrar que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean:
import data.real.basic variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := sorry |
Demostrar que la composición de dos funciones monótonas es monótona.
Para ello, completar la siguiente teoría de Lean:
import data.real.basic variables (f g : ℝ → ℝ) example (mf : monotone f) (mg : monotone g) : monotone (f ∘ g) := sorry |