Skip to main content

Las funciones con inversa por la izquierda son inyectivas

Funciones

En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por

   LeftInverse (g : β → α) (f : α → β) : Prop :=
      ∀ x, g (f x) = x

y que \(f\) tenga inversa por la izquierda está definido por

   HasLeftInverse (f : α → β) : Prop :=
      ∃ finv : β → α, LeftInverse finv f

Finalmente, que \(f\) es inyectiva está definido por

   Injective (f : α → β) : Prop :=
      ∀ ⦃x y⦄, f x = f y → x = y

Demostrar con Lean4 que si \(f\) tiene inversa por la izquierda, entonces \(f\) es inyectiva.

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

import Mathlib.Tactic
open Function

universe u v
variable {α : Type u}
variable {β : Type v}
variable {f : α → β}

example
  (hf : HasLeftInverse f)
  : Injective f :=
by sorry

Read more…

La congruencia módulo 2 es una relación de equivalencia

Relación de equivalencia

Se define la relación \(R\) entre los números enteros de forma que \(x\) está relacionado con \(y\) si \(x-y\) es divisible por 2.

Demostrar con Lean4 que \(R\) es una relación de equivalencia.

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

import Mathlib.Tactic

def R (m n : ℤ) := 2 ∣ (m - n)

example : Equivalence R :=
by sorry

Read more…

Si uₙ está acotada y el límite de vₙ es 0, entonces el límite de uₙ·vₙ es 0

Límites

Demostrar con Lean4 que si \(u_n\) está acotada y el límite de \(v_n\) es \(0\), entonces el límite de \(u_n·v_n\) es \(0\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (u v : ℕ → ℝ)
variable (a : ℝ)

def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

def acotada (a : ℕ → ℝ) :=
  ∃ B, ∀ n, |a n| ≤ B

example
  (hU : acotada u)
  (hV : limite v 0)
  : limite (u*v) 0 :=
by sorry

Read more…

Si (∀n)[uₙ ≤ vₙ], entonces lim uₙ ≤ lim vₙ

Límites

En Lean4, una sucesión \(u_0, u_1, u_2, \dots\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el \(n\)-ésimo término de la sucesión.

Se define que \(a\) límite de la sucesión \(u\) como sigue

   def limite (u : ℕ → ℝ) (c : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

Demostrar que si \((∀ n)[u_n ≤ v_n]\), \(a\) es límite de \(u_n\) y \(c\) es límite de \(v_n\), entonces \(a ≤ c\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (u v : ℕ → ℝ)
variable (a c : ℝ)

def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| < ε

example
  (hu : limite u a)
  (hv : limite v c)
  (huv : ∀ n, u n ≤ v n)
  : a ≤ c :=
by sorry

Read more…

La paradoja del barbero

Lógica de primer orden

Demostrar con Lean4 la paradoja del barbero; es decir, que no existe un hombre que afeite a todos los que no se afeitan a sí mismo y sólo a los que no se afeitan a sí mismo.

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

import Mathlib.Tactic

variable (Hombre : Type)
variable (afeita : Hombre → Hombre → Prop)

example :
  ¬(∃ x : Hombre, ∀ y : Hombre, afeita x y ↔ ¬ afeita y y) :=
by sorry

Read more…

Las sucesiones convergentes están acotadas

Límites

Demostrar con Lean4 que si \(u_n\) es una sucesión convergente, entonces está acotada; es decir, \[ (∃ k ∈ ℕ)(∃ b ∈ ℝ)(∀ n ∈ ℕ)[n ≥ k → |u_n| ≤ b] \]

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
by sorry

Read more…

Un número es par si y solo si lo es su cuadrado

Divisibilidad

Demostrar con Lean4 que un número es par si y solo si lo es su cuadrado.

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

import Mathlib.Algebra.Group.Even
import Mathlib.Tactic

open Int

variable (n : ℤ)

example :
  Even (n^2) ↔ Even n :=
by sorry

Read more…

Los supremos de las sucesiones crecientes son sus límites

Límites

Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (u : ℕ → ℝ)
variable (S : ℝ)

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε

-- (supremo u S) expresa que el supremo de u es S.
def supremo (u : ℕ → ℝ) (S : ℝ) :=
  (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε

example
  (hu : Monotone u)
  (hS : supremo u S)
  : limite u S :=
by sorry

Read more…

Si `f(x) ≤ f(y) → x ≤ y`, entonces f es inyectiva

Funciones reales

Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que \[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \] entonces \(f\) es inyectiva.

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

import Mathlib.Data.Real.Basic
open Function

variable (f : ℝ → ℝ)

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : Injective f :=
by sorry

Read more…