18 octubre 2023 – Calculemus

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

PorJosé A. Alonso 18 octubre 202310 octubre 2023

Demostrar con Lean4 que si \(f\) es par y \(g\) es impar, entonces \(f ∘ g\) es par.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.
def esPar (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = f (-x)

-- (esImpar f) expresa que f es impar.
def esImpar  (f : ℝ → ℝ) : Prop :=
  ∀ x, f x = - f (-x)

example
  (h1 : esPar f)
  (h2 : esImpar g)
  : esPar (f ∘ g) :=
by sorry

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

-- (esPar f) expresa que f es par.

def esPar (f : ℝ → ℝ) : Prop :=

∀ x, f x = f (-x)

-- (esImpar f) expresa que f es impar.

def esImpar (f : ℝ → ℝ) : Prop :=

∀ x, f x = - f (-x)

example

(h1 : esPar f)

(h2 : esImpar g)

: esPar (f ∘ g) :=

by sorry