Menu Close

Mes: noviembre 2022

Si f es par y g es impar, entonces f ∘ g es par

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).

Demostrar que si f es par y g es impar, entonces f ∘ g es par.

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

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
example
  (hf : par f)
  (hg : impar g)
  : par (f  g) :=
sorry

El producto de una función par por una impar es impar

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).

Demostrar que el producto de una función par por una impar es impar.

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

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
example
  (hf : par f)
  (hg : impar g)
  : impar (f * g) :=
sorry

El producto de dos funciones impares es par

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x) y es impar si, para todo x, f(-x) -f(x).

Demostrar que el producto de dos funciones impares es par.

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

import data.real.basic
variables (f g :   )
 
def par (f :   ) : Prop    :=  x, f x = f (-x)
def impar  (f :   ) : Prop :=  x, f x = -f (-x)
 
example
  (hf : impar f)
  (hg : impar g)
  : par (f * g) :=
sorry

La suma de dos funciones pares es par

La función f de ℝ en ℝ es par si, para todo x, f(-x) = f(x).

Demostrar que la suma de dos funciones pares es par.

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

import data.real.basic
 
variables (f g :   )
 
def par (f :   ) : Prop :=  x, f x = f (-x)
 
example
  (hf : par f)
  (hg : par g)
  : par (f + g) :=
sorry

Si f es monótona y c ≥ 0, entonces c·f es monótona

Demostrar que si f es monótona y c ≥ 0, entonces c·f es monótona.

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

import data.real.basic
 
variables (f :   )
variable  {c : }
 
example
  (mf : monotone f)
  (nnc : 0  c)
  : monotone (λ x, c * f x) :=
sorry

Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g

Demostrar que si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g.

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

import data.real.basic
 
def cota_superior (f :   ) (a : ) : Prop :=
 x, f x  a
 
def no_negativa (f :   ) : Prop :=
 x, 0  f x
 
variables (f g :   )
variables (a b : )
 
example
  (hfa : cota_superior f a)
  (hgb : cota_superior g b)
  (nng : no_negativa g)
  (nna : 0  a)
  : cota_superior (f * g) (a * b) :=
sorry

El producto de dos funciones no negativas es no negativa

Demostrar que el producto de dos funciones no negativas es no negativa.

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

import data.real.basic
variables (f g :   )
 
def no_negativa (f :   ) : Prop :=  x, 0  f x
 
example
  (nnf : no_negativa f)
  (nng : no_negativa g)
  : no_negativa (f * g) :=
sorry

La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g

Demostrar que la suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g.

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

import data.real.basic
 
-- (cota_inferior f a) se verifica si a es una cota inferior de f.
def cota_inferior (f :   ) (a : ) : Prop :=
 x, a  f x
 
variables (f g :   )
variables (a b : )
 
example
  (hfa : cota_inferior f a)
  (hgb : cota_inferior g b)
  : cota_inferior (λ x, f x + g x) (a + b) :=
sorry