Funciones monótonas

La composición de dos funciones monótonas es monótona

PorJosé A. Alonso 12 octubre 202310 octubre 2023

Demostrar con Lean4 que la composición de dos funciones monótonas es monótona.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f ∘ g) :=
by sorry

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

example

(mf : Monotone f)

(mg : Monotone g)

: Monotone (f ∘ g) :=

by sorry

Si c es no negativo y f es monótona, entonces cf es monótona

PorJosé A. Alonso 11 octubre 202310 octubre 2023

Demostrar con Lean4 que si \(c\) es no negativo y \(f\) es monótona, entonces \(cf\) es monótona.

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

import Mathlib.Data.Real.Basic

variable (f : ℝ → ℝ)
variable {c : ℝ}

example
  (mf : Monotone f)
  (nnc : 0 ≤ c)
  : Monotone (fun x ↦ c * f x) :=
by sorry

import Mathlib.Data.Real.Basic

variable (f : ℝ → ℝ)

variable {c : ℝ}

example

(mf : Monotone f)

(nnc : 0 ≤ c)

: Monotone (fun x ↦ c * f x) :=

by sorry