noviembre 2022 – Página 3

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

PorJosé A. Alonso 17 noviembre 202217 noviembre 2022

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

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

PorJosé A. Alonso 15 noviembre 202215 noviembre 2022

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

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

PorJosé A. Alonso 14 noviembre 202214 noviembre 2022

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

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

PorJosé A. Alonso 11 noviembre 202211 noviembre 2022

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

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

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

PorJosé A. Alonso 10 noviembre 202210 noviembre 2022

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

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

import data.real.basic

variables (f g : ℝ → ℝ)

example
  (mf : monotone f)
  (mg : monotone g)
  : monotone (f ∘ g) :=
sorry

import data.real.basic

variables (f g : ℝ → ℝ)

example

(mf : monotone f)

(mg : monotone g)

: monotone (f ∘ g) :=

sorry