1 noviembre 2023 – Calculemus

Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf

PorJosé A. Alonso 1 noviembre 202326 octubre 2023

Demostrar con Lean4 que si \(a\) es una cota superior de \(f\) y \(c ≥ 0\), entonces \(ca\) es una cota superior de \(cf\).

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

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.
def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

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

example
  (hfa : CotaSuperior f a)
  (h : c ≥ 0)
  : CotaSuperior (fun x ↦ c * f x) (c * a) :=
by sorry

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.

def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, f x ≤ a

variable {f : ℝ → ℝ}

variable {c : ℝ}

example

(hfa : CotaSuperior f a)

(h : c ≥ 0)

: CotaSuperior (fun x ↦ c * f x) (c * a) :=

by sorry