octubre 2023 – 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

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

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 a es una cota superior de s y a ≤ b, entonces b es una cota superior de s

PorJosé A. Alonso 23 octubre 202318 octubre 2023

Demostrar con Lean4 que si \(a\) es una cota superior de \(s\) y \(a ≤ b\), entonces \(b\) es una cota superior de \(s\).

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (s : Set α)
variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.
def CotaSupConj (s : Set α) (a : α) :=
  ∀ {x}, x ∈ s → x ≤ a

example
  (h1 : CotaSupConj s a)
  (h2 : a ≤ b)
  : CotaSupConj s b :=
by sorry

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]

variable (s : Set α)

variable (a b : α)

-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.

def CotaSupConj (s : Set α) (a : α) :=

∀ {x}, x ∈ s → x ≤ a

example

(h1 : CotaSupConj s a)

(h2 : a ≤ b)

: CotaSupConj s b :=

by sorry

Si r ⊆ s y s ⊆ t, entonces r ⊆ t

PorJosé A. Alonso 20 octubre 202317 octubre 2023

Demostrar con Lean4 que si \(r ⊆ s\) y \(s ⊆ t\), entonces \(r ⊆ t\).

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

import Mathlib.Tactic

open Set

variable {α : Type _}
variable (r s t : Set α)

example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
by sorry

import Mathlib.Tactic

open Set

variable {α : Type _}

variable (r s t : Set α)

example

(rs : r ⊆ s)

(st : s ⊆ t)

: r ⊆ t :=

by sorry

Para cualquier conjunto s, s ⊆ s

PorJosé A. Alonso 19 octubre 202317 octubre 2023

Demostrar con Lean4 que para cualquier conjunto \(s\), \(s ⊆ s\).

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

import Mathlib.Tactic

variable {α : Type _}
variable (s : Set α)

example : s ⊆ s :=
by sorry

import Mathlib.Tactic

variable {α : Type _}

variable (s : Set α)

example : s ⊆ s :=

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