30 noviembre 2022 – Calculemus

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

PorJosé A. Alonso 30 noviembre 20224 diciembre 2022

Demostrar que si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está.

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

import data.real.basic

variables {f : ℝ → ℝ}                    
variables {a c : ℝ}                      

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

-- (acotada_sup f) se verifica si f tiene cota superior.
def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

example
  (hf : acotada_sup f)
  (h : c ≥ 0)
  : acotada_sup (λ x, c * f x) :=
sorry

import data.real.basic

variables {f : ℝ → ℝ}

variables {a c : ℝ}

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

def cota_superior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a

-- (acotada_sup f) se verifica si f tiene cota superior.

def acotada_sup (f : ℝ → ℝ) := ∃ a, cota_superior f a

example

(hf : acotada_sup f)

(h : c ≥ 0)

: acotada_sup (λ x, c * f x) :=

sorry