Menu Close

Día: 15 noviembre 2022

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