2 noviembre 2023 – Calculemus

Si c ≥ 0 y f está acotada superiormente, entonces c·f también lo está

PorJosé A. Alonso 2 noviembre 202326 octubre 2023

Demostrar con Lean4 que si \(c ≥ 0\) y \(f\) está acotada superiormente, entonces \(c·f\) también lo está.

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

import src.Cota_superior_de_producto_por_escalar

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

-- (acotadaSup f) afirma que f tiene cota superior.
def acotadaSup (f : ℝ → ℝ) :=
  ∃ a, CotaSuperior f a

example
  (hf : acotadaSup f)
  (hc : c ≥ 0)
  : acotadaSup (fun x ↦ c * f x) :=
by sorry

import src.Cota_superior_de_producto_por_escalar

variable {f : ℝ → ℝ}

variable {c : ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.

def acotadaSup (f : ℝ → ℝ) :=

∃ a, CotaSuperior f a

example

(hf : acotadaSup f)

(hc : c ≥ 0)

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

by sorry