Menu Close

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

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

Soluciones con 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
 
-- Lema auxiliar
-- ============
 
lemma cota_superior_mul
  (hfa : cota_superior f a)
  (h : c  0)
  : cota_superior (λ x, c * f x) (c * a) :=
λ x, mul_le_mul_of_nonneg_left (hfa x) h
 
-- 1ª demostración
-- ===============
 
example
  (hf : acotada_sup f)
  (h : c  0)
  : acotada_sup (λ x, c * f x) :=
begin
  cases hf with a ha,
  have h1 : cota_superior (λ x, c * f x) (c * a) := cota_superior_mul ha h,
  have h2 :  z,  x, (λ x, c * f x) x  z,
    by exact Exists.intro (c * a) h1,
  show acotada_sup (λ x, c * f x),
    by exact h2,
end
 
-- 2ª demostración
-- ===============
 
example
  (hf : acotada_sup f)
  (h : c  0)
  : acotada_sup (λ x, c * f x) :=
begin
  cases hf with a ha,
  use c * a,
  apply cota_superior_mul ha h,
end
 
-- 3ª demostración
-- ===============
 
example
  (hf : acotada_sup f)
  (h : c  0)
  : acotada_sup (λ x, c * f x) :=
begin
  rcases hf with ⟨a, ha⟩,
  exact ⟨c * a, cota_superior_mul ha h⟩,
end
 
-- 4ª demostración
-- ===============
 
example
  (h : c  0)
  : acotada_sup f  acotada_sup (λ x, c * f x) :=
begin
  rintro ⟨a, ha⟩,
  exact ⟨c * a, cota_superior_mul ha h⟩,
end
 
-- 5ª demostración
-- ===============
 
example
  (h : c  0)
  : acotada_sup f  acotada_sup (λ x, c * f x) :=
λ ⟨a, ha⟩, ⟨c * a, cota_superior_mul ha h⟩

Se puede interactuar con la prueba anterior en esta sesión con Lean.

Referencias

Escribe un comentario