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

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

PorJosé A. Alonso 17 octubre 202310 octubre 2023

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

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)
  : esImpar (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)

: esImpar (f * g) :=

by sorry

El producto de dos funciones impares es par

PorJosé A. Alonso 16 octubre 202310 octubre 2023

Demostrar con Lean4 que el producto de dos funciones impares 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 : esImpar 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 : esImpar f)

(h2 : esImpar g)

: esPar (f * g) :=

by sorry

La suma de dos funciones pares es par

PorJosé A. Alonso 13 octubre 202310 octubre 2023

Demostrar con Lean4 que la suma de dos funciones pares 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)

example
  (h1 : esPar f)
  (h2 : esPar 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)

example

(h1 : esPar f)

(h2 : esPar g)

: esPar (f + g) :=

by sorry

La composición de dos funciones monótonas es monótona

PorJosé A. Alonso 12 octubre 202310 octubre 2023

Demostrar con Lean4 que la composición de dos funciones monótonas es monótona.

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

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

example
  (mf : Monotone f)
  (mg : Monotone g)
  : Monotone (f ∘ g) :=
by sorry

import Mathlib.Data.Real.Basic

variable (f g : ℝ → ℝ)

example

(mf : Monotone f)

(mg : Monotone g)

: Monotone (f ∘ g) :=

by sorry