11 octubre 2023 – Calculemus

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