Skip to main content

Las sucesiones divergentes positivas no tienen límites finitos

Límites

En Lean4, una sucesión \(u_0, u_1, u_2, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(uₙ\).

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

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

La sucesión \(u\) diverge positivamente cuando, para cada número real \(A\), se puede encontrar un número natural \(m\) tal que si \(n ≥ m\), entonces \(uₙ > A\). En Lean se puede definir por

   def diverge_positivamente (u : ℕ → ℝ) :=
     ∀ A, ∃ m, ∀ n ≥ m, u n > A

Demostrar que si \(u\) diverge positivamente, entonces ningún número real es límite de \(u\).

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

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

variable {u : ℕ → ℝ}

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

def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A

example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
by sorry

Read more…

Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

Límites

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

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \(u_0, u_2, u_4, u_6, ...\) se ha obtenido con la función de extracción \(f\) tal que \(f(n) = 2n\).

En Lean4, se puede definir que \(f\) es una función de extracción por

   def extraccion (f : ℕ → ℕ) :=
     ∀ n m, n < m → f n < f m

que a es un límite de u por

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

que a es un punto de acumulación de u por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ f, extraccion f ∧ limite (u ∘ f) a

que la sucesión u es de Cauchy por

   def suc_cauchy (u : ℕ → ℝ) :=
     ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

Demostrar con Lean4 que si \(u\) es una sucesión de Cauchy y \(a\) es un punto de acumulación de \(u\), entonces \(a\) es el límite de \(u\).

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

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

open Nat

variable {u : ℕ → ℝ}
variable {a : ℝ}

example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
by sorry

Read more…

El punto de acumulación de las sucesiones convergente es su límite

Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(f\) tal que \(f(n) = 2n\).

En Lean4, se puede definir que \(f\) es una función de extracción por

   def extraccion (f : ℕ → ℕ) :=
     ∀ n m, n < m → f n < f m

que \(a\) es un límite de \(u\) por

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

que \(u\) es convergente por

   def convergente (u : ℕ → ℝ) :=
     ∃ a, limite u a

que \(a\) es un punto de acumulación de \(u\) por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ f, extraccion f ∧ limite (u ∘ f) a

Demostrar con Lean4 que si \(u\) es una sucesión convergente y \(a\) es un punto de acumulación de \(u\), entonces \(a\) es un límite de \(u\).

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

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

open Nat

variable {u : ℕ → ℝ}
variable {a : ℝ}

def extraccion (f : ℕ → ℕ) :=
  ∀ n m, n < m → f n < f m

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

def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ f, extraccion f ∧ limite (u ∘ f) a

example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
by sorry

Read more…

Las subsucesiones tienen el mismo límite que la sucesión

Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_3, u_4, u_6, ... \] se ha obtenido con la función de extracción \(φ\) tal que \(φ(n) = 2n\).

En Lean4, se puede definir que \(φ\) es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

que \(v\) es una subsucesión de \(u\) por

   def subsucesion (v u : ℕ → ℝ) :=
     ∃ φ, extraccion φ ∧ v = u ∘ φ

y que \(a\) es un límite de \(u\) por

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

Demostrar con Lean4 que las subsucesiones de una sucesión convergente tienen el mismo límite que la sucesión.

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

import Mathlib.Data.Real.Basic
open Nat

variable {u v : ℕ → ℝ}
variable {a : ℝ}
variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ

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

example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
by sorry

Read more…

Si a es un punto de acumulación de u, entonces (∀ε>0)(∀n∈ℕ)(∃k≥n)[u(k)−a| < ε]

Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(φ\) tal que \(φ(n) = 2n\).

En Lean4, se puede definir que \(φ\) es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

También se puede definir que \(a\) es un límite de \(u\) por

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

Los puntos de acumulación de una sucesión son los límites de sus subsucesiones. En Lean4 se puede definir por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

Demostrar que si \(a\) es un punto de acumulación de \(u\), entonces \[ (∀ ε > 0)(∀ n ∈ ℕ)(∃ k ≥ n)[|u(k) - a| < ε \]

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

import Mathlib.Data.Real.Basic
open Nat

variable {u : ℕ → ℝ}
variable {a : ℝ}
variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

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

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ n, ∃ k ≥ n, |u k - a| < ε :=
by sorry

Read more…

Las funciones de extracción no están acotadas

Sucesiones

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(ϕ\) tal que \(ϕ(n) = 2n\).

En Lean4, se puede definir que \(ϕ\) es una función de extracción por

   def extraccion (ϕ : ℕ → ℕ) :=
     ∀ n m, n < m → ϕ n < ϕ m

Demostrar que las funciones de extracción no están acotadas; es decir, que si \(ϕ\) es una función de extracción, entonces \[ (∀ N, N')(∃ n ≥ N')[ϕ(n) ≥ N] \]

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

import Mathlib.Tactic
open Nat

variable {ϕ : ℕ → ℕ}

def extraccion (ϕ : ℕ → ℕ) :=
  ∀ n m, n < m → ϕ n < ϕ m

example
  (h : extraccion ϕ)
  : ∀ N N', ∃ n ≥ N', ϕ n ≥ N :=
by sorry

Read more…

Relación entre los índices de las subsucesiones y de la sucesión

Sucesiones

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(ϕ\) tal que \(ϕ(n) = 2n\).

En Lean4, se puede definir que \(ϕ\) es una función de extracción por

   def extraccion (ϕ : ℕ → ℕ) :=
     ∀ {n m}, n < m → ϕ n < ϕ m

Demostrarcon Lean4 que si \(ϕ\) es una función de extracción, entonces \[ (∀ n)[n ≤ ϕ(n) \]

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

import Mathlib.Tactic
open Nat

variable {ϕ : ℕ → ℕ}

def extraccion (ϕ : ℕ → ℕ) :=
  ∀ {n m}, n < m → ϕ n < ϕ m

example :
  extraccion ϕ → ∀ n, n ≤ ϕ n :=
by sorry

Read more…

Las particiones definen relaciones de equivalencia

Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia \(P\) de subconjuntos de \(X\) es una partición de \(X\) si cada elemento de \(X\) pertenece a un único conjunto de \(P\) y todos los elementos de \(P\) son no vacíos. Se puede definir en Lean4 por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar con Lean4 que si \(P\) es una partición de \(X\), entonces la relación definida por \(P\) es una relación de equivalencia.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : Equivalence (relacion P) :=
by sorry

Read more…

Las particiones definen relaciones transitivas

Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia \(P\) de subconjuntos de \(X\) es una partición de \(X\) si cada elemento de \(X\) pertenece a un único conjunto de \(P\) y todos los elementos de \(P\) son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar con Lean4 que si \(P\) es una partición de \(X\), entonces la relación definida por \(P\) es transitiva.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : Transitive (relacion P) :=
by sorry

Read more…

Las familias de conjuntos definen relaciones simétricas

Relaciones de equivalencia

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Demostrar con Lean4 que si \(P\) es una familia de subconjuntos de \(X\), entonces la relación definida por \(P\) es simétrica.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

-- 1ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  rcases hxy with ⟨A, h1⟩
  -- A : Set X
  -- h1 : A ∈ P ∧ x ∈ A ∧ y ∈ A
  have h2 : A ∈ P ∧ y ∈ A ∧ x ∈ A := by tauto
  exact ⟨A, h2⟩

-- 2ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  unfold Symmetric
  -- ⊢ ∀ ⦃x y : X⦄, relacion P x y → relacion P y x
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  unfold relacion at *
  -- hxy : ∃ A, A ∈ P ∧ x ∈ A ∧ y ∈ A
  -- ⊢ ∃ A, A ∈ P ∧ y ∈ A ∧ x ∈ A
  rcases hxy with ⟨A, hAP, ⟨hxA, hyA⟩⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  -- hyA : y ∈ A
  use A

-- 3ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  rcases hxy with ⟨A, hAP, ⟨hxA, hyA⟩⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  -- hyA : y ∈ A
  use A

-- 4ª demostración
-- ===============

example : Symmetric (relacion P) :=
by
  intros x y hxy
  -- x y : X
  -- hxy : relacion P x y
  -- ⊢ relacion P y x
  rcases hxy with ⟨A, hAP, ⟨hxA, hyA⟩⟩
  -- A : Set X
  -- hAP : A ∈ P
  -- hxA : x ∈ A
  -- hyA : y ∈ A
  exact ⟨A, ⟨hAP, hyA, hxA⟩⟩

Read more…