Skip to main content

La sucesión 1, -1, 1, -1, ... no es convergente

Límites

En Lean, una sucesión \(a₀, a₁, a₂, ...\) se puede representar mediante una función \((a : ℕ → ℝ)\) de forma que \(a(n)\) es \(aₙ\).

Se define que \(L\) es el límite de la sucesión \(a\), por

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

También se define que \(a\) es convergente por

def SucConv (a : ℕ → ℝ) : Prop :=
  ∃ L, LimSuc a L

Demostrar que si para todo \(n\), \(aₙ = (-1)^n\), entonces la sucesión \(a\) no es convergente.

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

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

variable {a : ℕ → ℝ}

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

def SucConv (a : ℕ → ℝ) : Prop :=
  ∃ L, LimSuc a L

example
  (ha : ∀ n, a n = (-1) ^ n)
  : ¬ SucConv a :=
by sorry

Read more…

La sucesión aₙ = 1/n converge a 0

Límites

En Lean, una sucesión \(a₀, a₁, a₂, ...\) se puede representar mediante una función \((a : ℕ → ℝ)\) de forma que \(a(n)\) es \(aₙ\).

Se define que \(L\) es el límite de la sucesión \(a\), por

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

Demostrar que si para todo \(n\), \(aₙ = \frac{1}{n}\), entonces la sucesión \(a\) converge a \(0\).

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

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

variable (a : ℕ → ℝ)

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

example
  (ha : ∀ n, a n = 1 / n)
  : LimSuc a 0 :=
by sorry

Read more…

Propiedad arquimediana de los números reales

Números reales

Demostrar la propiedad arquimediana de los números reales; es decir, que para cualquier \(ε ∈ ℝ\) con \(0 < ε\), existe \(N ∈ ℕ\) tal que \(1/ε < N\).

Para ello, completar la siguiente teoría de Lean 4:

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

variable {ε : ℝ}
variable (h : 0 < ε)

example : ∃ (N : ℕ), 1 / ε < N :=
by sorry

Read more…

La sucesión constante aₙ = L converge a L

Límites

En Lean, una sucesión \(a₀, a₁, a₂, ...\) se puede representar mediante una función \((a : ℕ → ℝ)\) de forma que \(a(n)\) es \(aₙ\).

Se define que \(L\) es el límite de la sucesión \(a\), por

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

Demostrar que si para todo \(n\), \(aₙ = L\), entonces la sucesión \(a\) converge a \(L\).

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

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

variable (a : ℕ → ℝ)
variable (L : ℝ)

def LimSuc (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

example
  (h : ∀ n, a n = L)
  : LimSuc a L :=
by sorry

Read more…

Demostraciones de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v] \]

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

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : s ∪ f ⁻¹' v ⊆ f ⁻¹' (f '' s ∪ v) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen_inversa
imports Main
begin

lemma "s ∪ f -` v ⊆ f -` (f ` s ∪ v)"
sorry

end

Read more…

Demostraciones de "f[s] ∩ v = f[s ∩ f⁻¹[v]​]​"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ v = f[s ∩ f⁻¹[v]] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : (f '' s) ∩ v = f '' (s ∩ f ⁻¹' v) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen_inversa
imports Main
begin

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
sorry

end

Read more…

Demostraciones de "f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable (α β : Type _)
variable (f : α → β)
variable (s : Set α)
variable (v : Set β)

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Union_con_la_imagen
imports Main
begin

lemma "f ` (s ∪ f -` v) ⊆ f ` s ∪ v"
sorry

end

Read more…

Demostraciones de "f[s] ∩ t = f[s ∩ f⁻¹[t]]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[ f[s] ∩ t = f[s ∩ f⁻¹[t]] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s : Set α)
variable (t : Set β)

example : (f '' s) ∩ t = f '' (s ∩ f ⁻¹' t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Interseccion_con_la_imagen
imports Main
begin

lemma "(f ` s) ∩ v = f ` (s ∩ f -` v)"
sorry

end

Read more…

Demostraciones de "f[s] \ f[t] ⊆ f[s \ t]"

Funciones

Demostrar con Lean4 y con Isabelle/HOL que \[f[s] \setminus f[t] ⊆ f[s \setminus t] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_diferencia_de_conjuntos
imports Main
begin

lemma "f ` s - f ` t ⊆ f ` (s - t)"
sorry

end

Read more…

Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]

Funciones

Demostrar con Lean4 y con Isabelle/HOL que si \(f\) es inyectiva, entonces \[ f[s] ∩ f[t] ⊆ f[s ∩ t] \]

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

import Mathlib.Data.Set.Function

open Set Function

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example
  (h : Injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
by sorry

y la siguiente teoría de Isabelle/HOL:

theory Imagen_de_la_interseccion_de_aplicaciones_inyectivas
imports Main
begin

lemma
  assumes "inj f"
  shows "f ` s ∩ f ` t ⊆ f ` (s ∩ t)"
sorry

end

Read more…