noviembre 2023 – Página 3

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

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