Funciones reales – Calculemus

La suma de dos funciones acotadas inferiormente también lo está

PorJosé A. Alonso 31 octubre 202330 octubre 2023

Demostrar con Lean4 que la suma de dos funciones acotadas inferiormente también lo está.

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

import src.Suma_de_cotas_inferiores
variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.
def acotadaInf (f : ℝ → ℝ) :=
  ∃ a, CotaInferior f a

example
  (hf : acotadaInf f)
  (hg : acotadaInf g)
  : acotadaInf (f + g) :=
by sorry

import src.Suma_de_cotas_inferiores

variable {f g : ℝ → ℝ}

-- (acotadaInf f) afirma que f tiene cota inferior.

def acotadaInf (f : ℝ → ℝ) :=

∃ a, CotaInferior f a

example

(hf : acotadaInf f)

(hg : acotadaInf g)

: acotadaInf (f + g) :=

by sorry

La suma de dos funciones acotadas superiormente también lo está

PorJosé A. Alonso 30 octubre 202323 octubre 2023

Demostrar con Lean4 que la suma de dos funciones acotadas superiormente también lo está.

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

import src.Suma_de_cotas_superiores
variable {f g : ℝ → ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.
def acotadaSup (f : ℝ → ℝ) :=
  ∃ a, CotaSuperior f a

example
  (hf : acotadaSup f)
  (hg : acotadaSup g)
  : acotadaSup (f + g) :=
by sorry

import src.Suma_de_cotas_superiores

variable {f g : ℝ → ℝ}

-- (acotadaSup f) afirma que f tiene cota superior.

def acotadaSup (f : ℝ → ℝ) :=

∃ a, CotaSuperior f a

example

(hf : acotadaSup f)

(hg : acotadaSup g)

: acotadaSup (f + g) :=

by sorry

Si c ≠ 0, entonces la función (x ↦ cx) es inyectiva

PorJosé A. Alonso 25 octubre 202318 octubre 2023

Demostrar con Lean4 que si \(c ≠ 0\), entonces la función \(x ↦ cx\) es inyectiva.

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

import Mathlib.Data.Real.Basic
open Function
variable {c : ℝ}

example
  (h : c ≠ 0)
  : Injective ((c * .)) :=
by sorry

import Mathlib.Data.Real.Basic

open Function

variable {c : ℝ}

example

(h : c ≠ 0)

: Injective ((c * .)) :=

by sorry

La función (x ↦ x + c) es inyectiva

PorJosé A. Alonso 24 octubre 202318 octubre 2023

Demostrar con Lean4 que la función \(x ↦ x + c\) es inyectiva.

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

import Mathlib.Data.Real.Basic
open Function

variable {c : ℝ}

example : Injective ((. + c)) :=
by sorry

import Mathlib.Data.Real.Basic

open Function

variable {c : ℝ}

example : Injective ((. + c)) :=

by sorry

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