Calculemus

Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf

PorJosé A. Alonso 1 noviembre 202326 octubre 2023

Demostrar con Lean4 que si \(a\) es una cota superior de \(f\) y \(c ≥ 0\), entonces \(ca\) es una cota superior de \(cf\).

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 : ℝ → ℝ}
variable {c : ℝ}

example
  (hfa : CotaSuperior f a)
  (h : c ≥ 0)
  : CotaSuperior (fun x ↦ c * f x) (c * a) :=
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 : ℝ → ℝ}

variable {c : ℝ}

example

(hfa : CotaSuperior f a)

(h : c ≥ 0)

: CotaSuperior (fun x ↦ c * f x) (c * a) :=

by sorry

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

Hay algún número real entre 2 y 3

PorJosé A. Alonso 27 octubre 202319 octubre 2023

Demostrar con Lean4 que hay algún número real entre 2 y 3.

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

import Mathlib.Data.Real.Basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
by sorry

import Mathlib.Data.Real.Basic

example : ∃ x : ℝ, 2 < x ∧ x < 3 :=

by sorry

La composición de funciones inyectivas es inyectiva

PorJosé A. Alonso 26 octubre 202319 octubre 2023

Demostrar con Lean4 que la composición de funciones inyectivas es inyectiva.

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

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}
variable {f : α → β} {g : β → γ}

example
  (hg : Injective g)
  (hf : Injective f) :
  Injective (g ∘ f) :=
by sorry

import Mathlib.Tactic

open Function

variable {α : Type _} {β : Type _} {γ : Type _}

variable {f : α → β} {g : β → γ}

example

(hg : Injective g)

(hf : Injective f) :

Injective (g ∘ f) :=

by sorry