octubre 2023 – Página 2

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

Si c es no negativo y f es monótona, entonces cf es monótona

PorJosé A. Alonso 11 octubre 202310 octubre 2023

Demostrar con Lean4 que si \(c\) es no negativo y \(f\) es monótona, entonces \(cf\) es monótona.

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

import Mathlib.Data.Real.Basic

variable (f : ℝ → ℝ)
variable {c : ℝ}

example
  (mf : Monotone f)
  (nnc : 0 ≤ c)
  : Monotone (fun x ↦ c * f x) :=
by sorry

import Mathlib.Data.Real.Basic

variable (f : ℝ → ℝ)

variable {c : ℝ}

example

(mf : Monotone f)

(nnc : 0 ≤ c)

: Monotone (fun x ↦ c * f x) :=

by sorry

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

PorJosé A. Alonso 10 octubre 202310 octubre 2023

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

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 ab es una cota superior de fg

PorJosé A. Alonso 9 octubre 20239 octubre 2023

Sean \(f\) y \(g\) funciones de \(ℝ\) en \(ℝ\). Demostrar con Lean4 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 \(ab\) es una cota superior de \(fg\).

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

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.
def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

-- (CotaInferior f a) expresa que a es una cota inferior de f.
def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

variable (f g : ℝ → ℝ)
variable (a b : ℝ)

example
  (hfa : CotaSuperior f a)
  (hgb : CotaSuperior g b)
  (nng : CotaInferior g 0)
  (nna : 0 ≤ a)
  : CotaSuperior (f * g) (a * b) :=
by sorry

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.

def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, f x ≤ a

-- (CotaInferior f a) expresa que a es una cota inferior de f.

def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, a ≤ f x

variable (f g : ℝ → ℝ)

variable (a b : ℝ)

example

(hfa : CotaSuperior f a)

(hgb : CotaSuperior g b)

(nng : CotaInferior g 0)

(nna : 0 ≤ a)

: CotaSuperior (f * g) (a * b) :=

by sorry

El producto de funciones no negativas es no negativo

PorJosé A. Alonso 6 octubre 202310 octubre 2023

Demostrar con Lean4 que si \(f\) y \(g\) son funciones no negativas de \(ℝ\) en \(ℝ\), entonces su producto es no negativo.

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

import Mathlib.Data.Real.Basic

-- (CotaInferior f a) expresa que a es una cota inferior de f.
def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

variable (f g : ℝ → ℝ)

example
  (nnf : CotaInferior f 0)
  (nng : CotaInferior g 0)
  : CotaInferior (f * g) 0 :=
by
sorry

import Mathlib.Data.Real.Basic

-- (CotaInferior f a) expresa que a es una cota inferior de f.

def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, a ≤ f x

variable (f g : ℝ → ℝ)

example

(nnf : CotaInferior f 0)

(nng : CotaInferior g 0)

: CotaInferior (f * g) 0 :=

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 5 octubre 202316 septiembre 2023

Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces 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 Lean4:

import Mathlib.Data.Real.Basic

-- (CotaInferior f a) expresa que a es una cota inferior de f.
def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, a ≤ f x

variable (f g : ℝ → ℝ)
variable (a b : ℝ)

example
  (hfa : CotaInferior f a)
  (hgb : CotaInferior g b)
  : CotaInferior (f + g) (a + b) :=
by sorry

import Mathlib.Data.Real.Basic

-- (CotaInferior f a) expresa que a es una cota inferior de f.

def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, a ≤ f x

variable (f g : ℝ → ℝ)

variable (a b : ℝ)

example

(hfa : CotaInferior f a)

(hgb : CotaInferior g b)

: CotaInferior (f + g) (a + b) :=

by sorry

La suma de una cota superior de f y una cota superior de g es una cota superior de f+g

PorJosé A. Alonso 4 octubre 202313 septiembre 2023

Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces la suma de una cota superior de \(f\) y una cota superior de \(g\) es una cota superior de \(f+g\).

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

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.
def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=
  ∀ x, f x ≤ a

variable (f g : ℝ → ℝ)
variable (a b : ℝ)

example
  (hfa : CotaSuperior f a)
  (hgb : CotaSuperior g b)
  : CotaSuperior (f + g) (a + b) :=
by sorry

import Mathlib.Data.Real.Basic

-- (CotaSuperior f a) se verifica si a es una cota superior de f.

def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop :=

∀ x, f x ≤ a

variable (f g : ℝ → ℝ)

variable (a b : ℝ)

example

(hfa : CotaSuperior f a)

(hgb : CotaSuperior g b)

: CotaSuperior (f + g) (a + b) :=

by sorry