José A. Alonso

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

En ℝ, {0 < ε, ε ≤ 1, |x| < ε, |y| < ε} ⊢ |xy| < ε

PorJosé A. Alonso 3 octubre 202313 septiembre 2023

Demostrar con Lean4, que en ℝ
\[ \left\{ 0 < ε, ε ≤ 1, |x| < ε, |y| < ε \right\} ⊢ |xy| < ε \] Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic

example :
  ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=
by sorry

import Mathlib.Data.Real.Basic

example :

∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε :=

by sorry