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

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

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 φ where hφ1 : "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¦"
      using hφ2 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