noviembre 2022 – Página 2

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

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

PorJosé A. Alonso 9 noviembre 20229 noviembre 2022

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

import data.real.basic

variables (f : ℝ → ℝ)

variable {c : ℝ}

example

(mf : monotone f)

(nnc : 0 ≤ c)

: monotone (λ x, c * f x) :=

sorry

La suma de dos funciones monótonas es monótona

PorJosé A. Alonso 8 noviembre 20228 noviembre 2022

Demostrar que la suma 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

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

PorJosé A. Alonso 7 noviembre 20226 noviembre 2022

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

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

PorJosé A. Alonso 4 noviembre 2022

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

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

PorJosé A. Alonso 3 noviembre 2022

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

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