Menu Close

Etiqueta: L.exact

Asociatividad de la concatenación de listas

En Lean la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas

   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que la concatenación es asociativa; es decir,

   xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

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

import data.list.basic
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
sorry
Soluciones con Lean
import data.list.basic
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
-- 1ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : append.equations._eqn_1 (ys ++ zs)
     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (append.equations._eqn_1 ys) rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : append.equations._eqn_2 a as (ys ++ zs)
     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI
     ... = (a :: (as ++ ys)) ++ zs : (append.equations._eqn_2 a (as ++ ys) zs).symm
     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_2 a as ys).symm rfl, },
end
 
-- 2ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : nil_append (ys ++ zs)
     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (nil_append ys) rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : cons_append a as (ys ++ zs)
     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI
     ... = (a :: (as ++ ys)) ++ zs : (cons_append a (as ++ ys) zs).symm
     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (cons_append a as ys).symm rfl, },
end
 
-- 3ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : by rw nil_append
     ... = ([] ++ ys) ++ zs        : by rw nil_append, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : by rw cons_append
     ... = a :: ((as ++ ys) ++ zs) : by rw HI
     ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
     ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append, },
end
 
-- 4ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : rfl
     ... = ([] ++ ys) ++ zs        : rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : rfl
     ... = a :: ((as ++ ys) ++ zs) : by rw HI
     ... = (a :: (as ++ ys)) ++ zs : rfl
     ... = ((a :: as) ++ ys) ++ zs : rfl, },
end
 
-- 5ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : by simp
     ... = ([] ++ ys) ++ zs        : by simp, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : by simp
     ... = a :: ((as ++ ys) ++ zs) : congr_arg (cons a) HI
     ... = (a :: (as ++ ys)) ++ zs : by simp
     ... = ((a :: as) ++ ys) ++ zs : by simp, },
end
 
-- 6ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { by simp, },
  { by exact (cons_inj a).mpr HI, },
end
 
-- 7ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw nil_append, },
  { rw cons_append,
    rw HI,
    rw cons_append,
    rw cons_append, },
end
 
-- 8ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
list.rec_on xs
  ( show [] ++ (ys ++ zs) = ([] ++ ys) ++ zs,
      from calc
        [] ++ (ys ++ zs)
            = ys ++ zs         : by rw nil_append
        ... = ([] ++ ys) ++ zs : by rw nil_append )
  ( assume a as,
    assume HI : as ++ (ys ++ zs) = (as ++ ys) ++ zs,
    show (a :: as) ++ (ys  ++ zs) = ((a :: as) ++ ys) ++ zs,
      from calc
        (a :: as) ++ (ys ++ zs)
            = a :: (as ++ (ys ++ zs)) : by rw cons_append
        ... = a :: ((as ++ ys) ++ zs) : by rw HI
        ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
        ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append)
 
-- 9ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
list.rec_on xs
  (by simp)
  (by simp [*])
 
-- 10ª demostración
lemma conc_asoc_1 :
   xs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
| [] := by calc
    [] ++ (ys ++ zs)
        = ys ++ zs         : by rw nil_append
    ... = ([] ++ ys) ++ zs : by rw nil_append
| (a :: as) := by calc
    (a :: as) ++ (ys ++ zs)
        = a :: (as ++ (ys ++ zs)) : by rw cons_append
    ... = a :: ((as ++ ys) ++ zs) : by rw conc_asoc_1
    ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
    ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append
 
-- 11ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
-- by library_search
append_assoc xs ys zs
 
-- 12ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
by induction xs ; simp [*]
 
-- 13ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Asociatividad_de_la_concatenacion_de_listas
imports Main
begin
 
(* 1ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  have "[] @ (ys @ zs) = ys @ zs"
    by (simp only: append_Nil)
  also have "… = ([] @ ys) @ zs"
    by (simp only: append_Nil)
  finally show "[] @ (ys @ zs) = ([] @ ys) @ zs"
    by this
next
  fix x xs
  assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs"
  have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))"
    by (simp only: append_Cons)
  also have "… = x # ((xs @ ys) @ zs)"
    by (simp only: HI)
  also have "… = (x # (xs @ ys)) @ zs"
    by (simp only: append_Cons)
  also have "… = ((x # xs) @ ys) @ zs"
    by (simp only: append_Cons)
  finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs"
    by this
qed
 
(* 2ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  have "[] @ (ys @ zs) = ys @ zs" by simp
  also have "… = ([] @ ys) @ zs" by simp
  finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" .
next
  fix x xs
  assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs"
  have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by simp
  also have "… = x # ((xs @ ys) @ zs)" by simp
  also have "… = (x # (xs @ ys)) @ zs" by simp
  also have "… = ((x # xs) @ ys) @ zs" by simp
  finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" .
qed
 
(* 3ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  show "[] @ (ys @ zs) = ([] @ ys) @ zs" by simp
next
  fix x xs
  assume "xs @ (ys @ zs) = (xs @ ys) @ zs"
  then show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by simp
qed
 
(* 4ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed
 
(* 5ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by (rule append_assoc [symmetric])
 
(* 6ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by (induct xs) simp_all
 
(* 7ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by simp
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

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

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

Para extraer una subsucesión se aplica una función de extracción queconserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ 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 : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) 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 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 Lean:

import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
variable  {φ :   }
 
notation `|`x`|` := abs x
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
def limite (u :   ) (l : ) : Prop :=
   ε > 0,  N,  n  N, |u n - l| < ε
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
def suc_cauchy (u :   ) :=
   ε > 0,  N,  p  N,  q  N, |u p - u q| < ε
 
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
variable  {φ :   }
 
notation `|`x`|` := abs x
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
def limite (u :   ) (l : ) : Prop :=
   ε > 0,  N,  n  N, |u n - l| < ε
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
def suc_cauchy (u :   ) :=
   ε > 0,  N,  p  N,  q  N, |u p - u q| < ε
 
lemma aux1
  (h : extraccion φ)
  :  n, n  φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
lemma aux2
  (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')
                             (aux1 h (max N N'))⟩⟩
 
lemma cerca_acumulacion
  (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 aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end
 
-- 1ª demostración
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold limite,
  intros ε hε,
  unfold suc_cauchy at hu,
  cases hu (ε/2) (half_pos hε) with N hN,
  use N,
  have ha' :  N'  N, |u N' - a| < ε/2,
    apply cerca_acumulacion ha (ε/2) (half_pos hε),
  cases ha' with N' h,
  cases h with hNN' hN',
  intros n hn,
  calc   |u n - a|
       = |(u n - u N') + (u N' - a)| : by ring_nf
   ...  |u n - u N'| + |u N' - a|   : abs_add (u n - u N') (u N' - a)
   ... < ε/2 + |u N' - a|            : add_lt_add_right (hN n hn N' hNN') _
   ... < ε/2 + ε/2                   : add_lt_add_left hN' (ε / 2)
   ... = ε                           : add_halves ε
end
 
-- 2ª demostración
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with N hN,
  use N,
  have ha' :  N'  N, |u N' - a| < ε/2,
    apply cerca_acumulacion ha (ε/2) (by linarith),
  rcases ha' with ⟨N', hNN', hN'⟩,
  intros n hn,
  calc  |u n - a|
      = |(u n - u N') + (u N' - a)| : by ring_nf
  ...  |u n - u N'| + |u N' - a|   : by simp [abs_add]
  ... < ε                           : by linarith [hN n hn N' hNN'],
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory "Si_a_es_un_punto_de_acumulacion_de_la_sucesion_de_Cauchy_u,_entonces_a_es_el_limite_de_u"
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"
 
definition suc_cauchy :: "(nat ⇒ real) ⇒ bool"
  where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"
 
(* Lemas auxiliares *)
 
lemma aux1 :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
lemma aux2 :
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  have "max N N' ≥ N' ∧ φ (max N N') ≥ N"
    by (meson assms aux1 max.bounded_iff max.cobounded2)
  then show "∃k ≥ N'. φ k ≥ N"
    by blast
qed
 
lemma cerca_acumulacion :
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using2 limite_def ‹ε > 0by auto
  obtain m where "m ≥ N' ∧ φ m ≥ N"
    using aux2 hφ1 by blast
  then show "∃k≥N. ¦u k - a¦ < ε"
    using hN' by auto
qed
 
(* Demostración *)
lemma
  assumes "suc_cauchy u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then have "ε/2 > 0"
    by simp
  then obtain N where hN : "∀m≥N. ∀n≥N. ¦u m - u n¦ < ε/2"
    using assms(1) suc_cauchy_def
    by blast
  have "∀k≥N. ¦u k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume hk : "k ≥ N"
    obtain N' where hN'1 : "N' ≥ N" and
                    hN'2 : "¦u N' - a¦ < ε/2"
      using assms(2) cerca_acumulacion ‹ε/2 > 0by blast
    have "¦u k - a¦ = ¦(u k - u N') + (u N'  - a)¦"
      by simp
    also have "… ≤ ¦u k - u N'¦ + ¦u N'  - a¦"
      by simp
    also have "… < ε/2 + ¦u N'  - a¦"
      using hk hN hN'1 by auto
    also have "… < ε/2 + ε/2"
      using hN'2 by auto
    also have "… = ε"
      by simp
    finally show "¦u k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦u k - a¦ < ε"
    by auto
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

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

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ 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 : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

Demostrar 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 Lean:

import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
def convergente (u :   ) :=
   a, limite u a
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
 
def extraccion (φ :   ) :=
   n m, n < m  φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
def convergente (u :   ) :=
   a, limite u a
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
-- Lemas auxiliares
-- ================
 
lemma unicidad_limite_aux
  {a b: }
  (ha : limite u a)
  (hb : limite u b)
  : b  a :=
begin
  by_contra h,
  set ε := b - a with hε,
  cases ha (ε/2) (by linarith) with A hA,
  cases hb (ε/2) (by linarith) with B hB,
  set N := max A B with hN,
  have hAN : A  N := le_max_left A B,
  have hBN : B  N := le_max_right A B,
  specialize hA N hAN,
  specialize hB N hBN,
  rw abs_lt at hA hB,
  linarith,
end
 
lemma unicidad_limite
  {a b: }
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (unicidad_limite_aux hb ha)
            (unicidad_limite_aux ha hb)
 
lemma limite_subsucesion_aux
  {φ :   }
  (h : extraccion φ)
  :  n, n  φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
lemma limite_subsucesion
  {φ :   }
  {a : }
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u  φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros k hk,
  calc |(u  φ) k - a|
       = |u (φ k) - a| : rfl
   ... < ε             : hN (φ k) _,
  calc φ k
        k : limite_subsucesion_aux hφ k
   ...  N : hk,
end
 
-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold convergente at hu,
  cases hu with b hb,
  convert hb,
  unfold punto_acumulacion at ha,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  have hφ₃ : limite (u  φ) b,
    from limite_subsucesion hb hφ₁,
  exact unicidad_limite hφ₂ hφ₃,
end
 
-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  apply unicidad_limite hφ₂ _,
  exact limite_subsucesion hb hφ₁,
end
 
-- 2ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁),
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"
 
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"
 
definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"
 
(* Lemas auxiliares *)
 
lemma unicidad_limite_aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed
 
lemma unicidad_limite :
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1)
    by (rule unicidad_limite_aux)
next
  show "b ≤ a" using assms(1) assms(2)
    by (rule unicidad_limite_aux)
qed
 
lemma limite_subsucesion_aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
lemma limite_subsucesion :
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: limite_subsucesion_aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed
 
(* Demostración *)
lemma
  assumes "convergente u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof -
  obtain b where hb : "limite u b"
    using assms(1) convergente_def by auto
  obtain φ where1 : "extraccion φ" and
                 hφ2 : "limite (u ∘ φ) a"
    using assms(2) punto_acumulacion_def  by auto
  have "limite (u ∘ φ) b"
    using1 hb limite_subsucesion subsucesion_def by blast
  with2 have "a = b"
    by (rule unicidad_limite)
  then show "limite u a"
    using hb by simp
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

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

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, 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 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 Lean:

import data.real.basic
open nat
 
variables {u v :   }
variable  {a : }
variable  {φ :   }
 
def extraccion (φ :   ):=
   n m, n < m  φ n < φ m
 
def subsucesion (v u :   ) :=
   φ, extraccion φ  v = u  φ
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variables {u v :   }
variable  {a : }
variable  {φ :   }
 
def extraccion (φ :   ):=
   n m, n < m  φ n < φ m
 
def subsucesion (v u :   ) :=
   φ, extraccion φ  v = u  φ
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
-- En la demostración se usará el siguiente lema.
lemma aux
  (h : extraccion φ)
  :  n, n  φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
-- 1ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  unfold limite,
  intros ε hε,
  unfold limite at ha,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  unfold subsucesion at hv,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  apply hN,
  apply le_trans hn,
  exact aux hφ1 n,
end
 
-- 2ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  apply hN,
  exact le_trans hn (aux hφ1 n),
end
 
-- 3ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  exact hN (φ n) (le_trans hn (aux hφ1 n)),
end
 
-- 4ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  use N,
  exact λ n hn, hN (φ n) (le_trans hn (aux hφ1 n)),
end
 
-- 5ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  exact ⟨N, λ n hn, hN (φ n) (le_trans hn (aux hφ1 n))⟩,
end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
(* En la demostración se usará el siguiente lema *)
lemma aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
(* Demostración *)
lemma
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

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

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, 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 Lean 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 Lean:

import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
variable  {φ :   }
 
def extraccion (φ :   ):=
   n m, n < m  φ n < φ m
 
notation `|`x`|` := abs x
 
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| < ε :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable  {u :   }
variables {a : }
variable  {φ :   }
 
def extraccion (φ :   ):=
   n m, n < m  φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u :   ) (a : ) :=
   ε > 0,  N,  k  N, |u k - a| < ε
 
def punto_acumulacion (u :   ) (a : ) :=
   φ, extraccion φ  limite (u  φ) a
 
-- En la demostración se usarán los siguientes lemas.
 
lemma aux1
  (h : extraccion φ)
  :  n, n  φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
lemma aux2
  (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')
                             (aux1 h (max N N'))⟩⟩
 
-- 1ª demostración
example
  (h : punto_acumulacion u a)
  :  ε > 0,  N,  k  N, |u k - a| < ε :=
begin
  intros ε hε N,
  unfold punto_acumulacion at h,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  unfold limite at2,
  cases hφ2 ε hε with N' hN',
  rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  clear hφ12,
  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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 (aux2 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 (aux2 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 (aux2 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 (aux2 hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory "Si_a_es_un_punto_de_acumulacion_de_u,_entonces_a_tiene_puntos_cercanos"
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"
 
(* En la demostración se usarán los siguientes lemas *)
lemma aux1 :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
lemma aux2 :
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  have "max N N' ≥ N' ∧ φ (max N N') ≥ N"
    by (meson assms aux1 max.bounded_iff max.cobounded2)
  then show "∃k ≥ N'. φ k ≥ N"
    by blast
qed
 
(* 1ª demostración *)
lemma
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using2 limite_def ‹ε > 0by auto
  obtain m where hm1 : "m ≥ N'" and hm2 : "φ m ≥ N"
    using aux2 hφ1 by blast
  have "φ m ≥ N ∧ ¦u (φ m) - a¦ < ε"
    using hN' hm1 hm2 by force
  then show "∃k≥N. ¦u k - a¦ < ε"
    by auto
qed
 
(* 2ª demostración *)
lemma
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using2 limite_def ‹ε > 0by auto
  obtain m where "m ≥ N' ∧ φ m ≥ N"
    using aux2 hφ1 by blast
  then show "∃k≥N. ¦u k - a¦ < ε"
    using hN' by auto
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>