Menu Close

ForMatUS: Pruebas en Lean de “Hay infinitos términos arbitrariamente próximos a los puntos de acumulación”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 14 pruebas en Lean de la propiedad

Si a es un punto de acumulación de la sucesión u, entonces

∀ ε > 0, ∀ N, ∃ n ≥ N, |u n – a| ≤ ε

usando los estilos declarativo, aplicativo y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
 
variable  {u :   }
variables {a : }
variable  {φ :   }
 
-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------
 
notation `|`x`|` := abs x
 
def limite : (  )    Prop :=
λ u c,  ε > 0,  N,  n  N, |u n - c|  ε
 
def extraccion : (  )  Prop
| φ :=  n m, n < m  φ n < φ m
 
lemma id_mne_extraccion
  (h : extraccion φ)
  :  n, n  φ n :=
begin
  intros n,
  induction n with m HI,
  { linarith },
  { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },
end
 
lemma extraccion_mye
  (h : extraccion φ)
  :  N N',  n  N', φ n  N :=
λ N N',
  ⟨max N N', le_max_right N N',
             le_trans (le_max_left N N')
             (id_mne_extraccion h (max N N'))⟩
 
-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    punto_acumulacion : (ℕ → ℝ) → ℝ → Prop
-- tal que (punto_acumulacion u a) expresa que a es un
-- punto de acumulación de u; es decir, que es el
-- límite de alguna subsucesión de u.
-- ----------------------------------------------------
 
def punto_acumulacion : (  )    Prop
| u a :=  φ, extraccion φ  limite (u  φ) a
 
-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que si a es un punto de
-- acumulación de u, entonces
--    ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε
-- ----------------------------------------------------
 
-- 1ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
begin
  intros ε hε N,
  -- unfold punto_acumulacion at h,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  -- unfold limite at hφ2,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  -- clear hφ1 hφ2,
  use φ m,
  split,
  { exact hm', },
  { exact hN' m hm, },
end
 
-- 2ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  use φ m,
  exact ⟨hm', hN' m hm⟩,
end
 
-- 3ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end
 
-- 4ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  use φ m ; finish
end
 
-- 5ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        have h1 :  n  N', φ n  N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm :  (H : m  N'), φ m  N,
            exists.elim hm
              ( assume hm1 : m  N',
                assume hm2 : φ m  N,
                have h2 : |u (φ m) - a|  ε,
                  from hN' m hm1,
                show  n  N, |u n - a|  ε,
                  from exists.intro (φ m) (exists.intro hm2 h2)))))
 
-- 6ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        have h1 :  n  N', φ n  N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm :  (H : m  N'), φ m  N,
            exists.elim hm
              ( assume hm1 : m  N',
                assume hm2 : φ m  N,
                have h2 : |u (φ m) - a|  ε,
                  from hN' m hm1,
                show  n  N, |u n - a|  ε,
                  from ⟨φ m, hm2, h2⟩))))
 
-- 7ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        have h1 :  n  N', φ n  N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm :  (H : m  N'), φ m  N,
            exists.elim hm
              ( assume hm1 : m  N',
                assume hm2 : φ m  N,
                have h2 : |u (φ m) - a|  ε,
                  from hN' m hm1,
                ⟨φ m, hm2, h2⟩))))
 
-- 8ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        have h1 :  n  N', φ n  N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm :  (H : m  N'), φ m  N,
            exists.elim hm
              ( assume hm1 : m  N',
                assume hm2 : φ m  N,
                ⟨φ m, hm2, hN' m hm1⟩))))
 
-- 9ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        have h1 :  n  N', φ n  N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm :  (H : m  N'), φ m  N,
            exists.elim hm
              (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))
 
-- 10ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        have h1 :  n  N', φ n  N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))
 
-- 11ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' :  (n : ), n  N'  |(u  φ) n - a|  ε,
        exists.elim (extraccion_mye hφ.1 N N')
          (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))
 
-- 12ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ  limite (u  φ) a,
    exists.elim (hφ.2 ε hε)
      (λ N' hN', exists.elim (extraccion_mye hφ.1 N N')
        (λ m hm, exists.elim hm
          (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))
 
-- 13ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  (λ φ hφ, exists.elim (hφ.2 ε hε)
    (λ N' hN', exists.elim (extraccion_mye hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))
 
-- 14ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  n  N, |u n - a|  ε :=
λ ε hε N, exists.elim h
  (λ φ hφ, exists.elim (hφ.2 ε hε)
    (λ N' hN', exists.elim (extraccion_mye hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))
ForMatUS