Análisis – Página 9

Límite con suma de constante

PorJosé A. Alonso 13 julio 20216 julio 2021

En Lean, una sucesión u₀, u₁, u₂, … 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 : (ℕ → ℝ) → ℝ → Prop :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

donde se usa la notación |x| para el valor absoluto de x

   notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

Demostrar que si el límite de la sucesión u(i) es a y c ∈ ℝ, entonces el límite de u(i)+c es a+c.

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

import data.real.basic
import tactic

variables {u : ℕ → ℝ}
variables {a c : ℝ}

notation `|`x`|` := abs x

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

example
  (h : limite u a)
  : limite (λ i, u i + c) (a + c) :=
sorry

import data.real.basic

import tactic

variables {u : ℕ → ℝ}

variables {a c : ℝ}

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example

(h : limite u a)

: limite (λ i, u i + c) (a + c) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variables {u : ℕ → ℝ}
variables {a c : ℝ}

notation `|`x`|` := abs x

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

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

example
  (h : limite u a)
  : limite (λ i, u i + c) (a + c) :=
begin
  intros ε hε,
  dsimp,
  cases h ε hε with k hk,
  use k,
  intros n hn,
  calc |u n + c - (a + c)|
       = |u n - a|         : by norm_num
   ... < ε                 : hk n hn,
end

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

example
  (h : limite u a)
  : limite (λ i, u i + c) (a + c) :=
begin
  intros ε hε,
  dsimp,
  cases h ε hε with k hk,
  use k,
  intros n hn,
  convert hk n hn using 2,
  ring,
end

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

example
  (h : limite u a)
  : limite (λ i, u i + c) (a + c) :=
begin
  intros ε hε,
  convert h ε hε,
  by norm_num,
end

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

example
  (h : limite u a)
  : limite (λ i, u i + c) (a + c) :=
λ ε hε, (by convert h ε hε; norm_num)

import data.real.basic

import tactic

variables {u : ℕ → ℝ}

variables {a c : ℝ}

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración

-- ===============

example

(h : limite u a)

: limite (λ i, u i + c) (a + c) :=

begin

intros ε hε,

dsimp,

cases h ε hε with k hk,

use k,

intros n hn,

calc |u n + c - (a + c)|

= |u n - a| : by norm_num

... < ε : hk n hn,

end

-- 2ª demostración

-- ===============

example

(h : limite u a)

: limite (λ i, u i + c) (a + c) :=

begin

intros ε hε,

dsimp,

cases h ε hε with k hk,

use k,

intros n hn,

convert hk n hn using 2,

ring,

end

-- 3ª demostración

-- ===============

example

(h : limite u a)

: limite (λ i, u i + c) (a + c) :=

begin

intros ε hε,

convert h ε hε,

by norm_num,

end

-- 4ª demostración

-- ===============

example

(h : limite u a)

: limite (λ i, u i + c) (a + c) :=

λ ε hε, (by convert h ε hε; norm_num)

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>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Limite_cuando_se_suma_una_constante
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma 
  assumes "limite u a"
  shows   "limite (λ i.  u i + c)  (a + c)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦u n + c - (a + c)¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then have "∃k. ∀n≥k. ¦u n - a¦ < ε" 
      using assms limite_def by simp
    then obtain k where "∀n≥k. ¦u n - a¦ < ε" 
      by (rule exE)
    then have "∀n≥k. ¦u n + c - (a + c)¦ < ε" 
      by simp 
    then show "∃k. ∀n≥k. ¦u n + c - (a + c)¦ < ε"
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma 
  assumes "limite u a"
  shows   "limite (λ i.  u i + c)  (a + c)"
  using assms limite_def
  by simp

end

theory Limite_cuando_se_suma_una_constante

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma

assumes "limite u a"

shows "limite (λ i. u i + c) (a + c)"

proof (unfold limite_def)

show "∀ε>0. ∃k. ∀n≥k. ¦u n + c - (a + c)¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

then have "∃k. ∀n≥k. ¦u n - a¦ < ε"

using assms limite_def by simp

then obtain k where "∀n≥k. ¦u n - a¦ < ε"

by (rule exE)

then have "∀n≥k. ¦u n + c - (a + c)¦ < ε"

by simp

then show "∃k. ∀n≥k. ¦u n + c - (a + c)¦ < ε"

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "limite u a"

shows "limite (λ i. u i + c) (a + c)"

using assms limite_def

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>
[/expand]

Unicidad del límite de las sucesiones convergentes

PorJosé A. Alonso 12 julio 20214 julio 2021

En Lean, una sucesión u₀, u₁, u₂, … 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 : (ℕ → ℝ) → ℝ → Prop :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

donde se usa la notación |x| para el valor absoluto de x

   notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

Demostrar que cada sucesión tiene como máximo un límite.

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

import data.real.basic

variables {u : ℕ → ℝ}
variables {a b : ℝ}

notation `|`x`|` := abs x

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

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
sorry

import data.real.basic

variables {u : ℕ → ℝ}

variables {a b : ℝ}

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables {u : ℕ → ℝ}
variables {a b : ℝ}

notation `|`x`|` := abs x

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

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

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
begin
  by_contra h,
  wlog hab : a < b,
  { have : a < b ∨ a = b ∨ b < a := lt_trichotomy a b,
    tauto },
  set ε := b - a with hε,
  specialize ha (ε/2),
  have hε2 : ε/2 > 0 := by linarith,
  specialize ha hε2,
  cases ha 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

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

example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
begin
  by_contra h,
  wlog hab : a < b,
  { have : a < b ∨ a = b ∨ b < a := lt_trichotomy a b,
    tauto },
  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

import data.real.basic

variables {u : ℕ → ℝ}

variables {a b : ℝ}

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

-- 1ª demostración

-- ===============

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

begin

by_contra h,

wlog hab : a < b,

{ have : a < b ∨ a = b ∨ b < a := lt_trichotomy a b,

tauto },

set ε := b - a with hε,

specialize ha (ε/2),

have hε2 : ε/2 > 0 := by linarith,

specialize ha hε2,

cases ha 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

-- 2ª demostración

-- ===============

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

begin

by_contra h,

wlog hab : a < b,

{ have : a < b ∨ a = b ∨ b < a := lt_trichotomy a b,

tauto },

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

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>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Unicidad_del_limite_de_las_sucesiones_convergentes
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

lemma 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 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2" 
    using assms(2) limite_def ‹0 < ?ε/2› by 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

theorem
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1) by (rule aux)
next 
  show "b ≤ a" using assms(1) assms(2) by (rule aux)
qed

end

theory Unicidad_del_limite_de_las_sucesiones_convergentes

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

lemma 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 < ?ε/2› by blast

obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"

using assms(2) limite_def ‹0 < ?ε/2› by 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

theorem

assumes "limite u a"

"limite u b"

shows "a = b"

proof (rule antisym)

show "a ≤ b" using assms(2) assms(1) by (rule aux)

show "b ≤ a" using assms(1) assms(2) by (rule aux)

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>
[/expand]

Límite de sucesiones constantes

PorJosé A. Alonso 11 julio 20214 julio 2021

En Lean, una sucesión u₀, u₁, u₂, … 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 : (ℕ → ℝ) → ℝ → Prop :=
   λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

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

donde se usa la notación |x| para el valor absoluto de x

   notation `|`x`|` := abs x

1	notation `\|`x`\|` := abs x

Demostrar que el límite de la sucesión constante c es c.

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

import data.real.basic

variable (u : ℕ → ℝ)
variable (c : ℝ)

notation `|`x`|` := abs x

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

example :
  limite (λ n, c) c :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variable (c : ℝ)

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

example :

limite (λ n, c) c :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable (u : ℕ → ℝ)
variable (c : ℝ)

notation `|`x`|` := abs x

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

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

example :
  limite (λ n, c) c :=
begin
  unfold limite,
  intros ε hε,
  use 0,
  intros n hn,
  dsimp,
  simp,
  exact hε,
end

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

example :
  limite (λ n, c) c :=
begin
  intros ε hε,
  use 0,
  rintro n -,
  norm_num,
  assumption,
end

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

example :
  limite (λ n, c) c :=
begin
  intros ε hε,
  use 0,
  intros n hn,
  calc |(λ n, c) n - c|
       = |c - c|  : rfl
   ... = 0        : by simp
   ... < ε        : hε
end

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

example :
  limite (λ n, c) c :=
begin
  intros ε hε,
  by finish,
end

-- 5ª demostración
-- ===============

example :
  limite (λ n, c) c :=
λ ε hε, by finish

-- 6ª demostración
-- ===============

example :
  limite (λ n, c) c :=
assume ε,
assume hε : ε > 0,
exists.intro 0
  ( assume n,
    assume hn : n ≥ 0,
    show |(λ n, c) n - c| < ε, from
      calc |(λ n, c) n - c|
           = |c - c|  : rfl
       ... = 0        : by simp
       ... < ε        : hε)

import data.real.basic

variable (u : ℕ → ℝ)

variable (c : ℝ)

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u a, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε

-- 1ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

unfold limite,

intros ε hε,

use 0,

intros n hn,

dsimp,

simp,

exact hε,

end

-- 2ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

intros ε hε,

use 0,

rintro n -,

norm_num,

assumption,

end

-- 3ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

intros ε hε,

use 0,

intros n hn,

calc |(λ n, c) n - c|

= |c - c| : rfl

... = 0 : by simp

... < ε : hε

end

-- 4ª demostración

-- ===============

example :

limite (λ n, c) c :=

begin

intros ε hε,

by finish,

end

-- 5ª demostración

-- ===============

example :

limite (λ n, c) c :=

λ ε hε, by finish

-- 6ª demostración

-- ===============

example :

limite (λ n, c) c :=

assume ε,

assume hε : ε > 0,

exists.intro 0

( assume n,

assume hn : n ≥ 0,

show |(λ n, c) n - c| < ε, from

calc |(λ n, c) n - c|

= |c - c| : rfl

... = 0 : by simp

... < ε : hε)

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>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

(* ---------------------------------------------------------------------
-- En Isabelle/HOL, una sucesión u₀, u₁, u₂, ... 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
--    definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
--      where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"
--
-- Demostrar que el límite de la sucesión constante c es c.
-- ------------------------------------------------------------------ *)

theory Limite_de_sucesiones_constantes
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma "limite (λ n. c) c"
proof (unfold limite_def)
  show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" 
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    have "∀n≥0::nat. ¦c - c¦ < ε" 
    proof (intro allI impI)
      fix n :: nat
      assume "0 ≤ n"
      have "c - c = 0" 
        by (simp only: diff_self)
      then have "¦c - c¦ = 0" 
        by (simp only: abs_eq_0_iff)
      also have "… < ε"
        by (simp only: ‹0 < ε›) 
      finally show "¦c - c¦ < ε" 
        by this
    qed
    then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" 
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma "limite (λ n. c) c"
proof (unfold limite_def)
  show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε" 
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    have "∀n≥0::nat. ¦c - c¦ < ε"          by (simp add: ‹0 < ε›)   
    then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI)
  qed
qed

(* 3ª demostración *)

lemma "limite (λ n. c) c" 
  unfolding limite_def
  by simp

(* 4ª demostración *)

lemma "limite (λ n. c) c" 
  by (simp add: limite_def)

end

(* ---------------------------------------------------------------------

-- En Isabelle/HOL, una sucesión u₀, u₁, u₂, ... 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

-- definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

-- where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

-- Demostrar que el límite de la sucesión constante c es c.

-- ------------------------------------------------------------------ *)

theory Limite_de_sucesiones_constantes

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"

(* 1ª demostración *)

lemma "limite (λ n. c) c"

proof (unfold limite_def)

show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

have "∀n≥0::nat. ¦c - c¦ < ε"

proof (intro allI impI)

fix n :: nat

assume "0 ≤ n"

have "c - c = 0"

by (simp only: diff_self)

then have "¦c - c¦ = 0"

by (simp only: abs_eq_0_iff)

also have "… < ε"

by (simp only: ‹0 < ε›)

finally show "¦c - c¦ < ε"

by this

qed

then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε"

by (rule exI)

qed

(* 2ª demostración *)

lemma "limite (λ n. c) c"

proof (unfold limite_def)

show "∀ε>0. ∃k::nat. ∀n≥k. ¦c - c¦ < ε"

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

have "∀n≥0::nat. ¦c - c¦ < ε" by (simp add: ‹0 < ε›)

then show "∃k::nat. ∀n≥k. ¦c - c¦ < ε" by (rule exI)

qed

(* 3ª demostración *)

lemma "limite (λ n. c) c"

unfolding limite_def

by simp

(* 4ª demostración *)

lemma "limite (λ n. c) c"

by (simp add: limite_def)

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>
[/expand]