julio 2021 – Página 2

Una función creciente e involutiva es la identidad

PorJosé A. Alonso 21 julio 2021

Sea una función f de ℝ en ℝ.

Se dice que f es creciente si para todo x e y tales que x ≤ y se tiene que f(x) ≤ f(y).
Se dice que f es involutiva si para todo x se tiene que f(f(x)) = x.

En Lean que f sea creciente se representa por monotone f y que sea involutiva por involutive f

Demostrar que si f es creciente e involutiva, entonces f es la identidad.

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

import data.real.basic
open function

variable (f : ℝ → ℝ)

example
  (hc : monotone f)
  (hi : involutive f)
  : f = id :=
sorry

import data.real.basic

open function

variable (f : ℝ → ℝ)

example

(hc : monotone f)

(hi : involutive f)

: f = id :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open function

variable (f : ℝ → ℝ)

-- 1ª demostración
example
  (hc : monotone f)
  (hi : involutive f)
  : f = id :=
begin
  unfold monotone involutive at *,
  funext,
  unfold id,
  cases (le_total (f x) x) with h1 h2,
  { apply antisymm h1,
    have h3 : f (f x) ≤ f x,
      { apply hc,
        exact h1, },
    rwa hi at h3, },
  { apply antisymm _ h2,
    have h4 : f x ≤ f (f x),
      { apply hc,
        exact h2, },
    rwa hi at h4, },
end

-- 2ª demostración
example
  (hc : monotone f)
  (hi : involutive f)
  : f = id :=
begin
  funext,
  cases (le_total (f x) x) with h1 h2,
  { apply antisymm h1,
    have h3 : f (f x) ≤ f x := hc h1,
    rwa hi at h3, },
  { apply antisymm _ h2,
    have h4 : f x ≤ f (f x) := hc h2,
    rwa hi at h4, },
end

-- 3ª demostración
example
  (hc : monotone f)
  (hi : involutive f)
  : f = id :=
begin
  funext,
  cases (le_total (f x) x) with h1 h2,
  { apply antisymm h1,
    calc x
         = f (f x) : (hi x).symm
     ... ≤ f x     : hc h1 },
  { apply antisymm _ h2,
    calc f x
         ≤ f (f x) : hc h2
     ... = x       : hi x },
end

import data.real.basic

open function

variable (f : ℝ → ℝ)

-- 1ª demostración

example

(hc : monotone f)

(hi : involutive f)

: f = id :=

begin

unfold monotone involutive at *,

funext,

unfold id,

cases (le_total (f x) x) with h1 h2,

{ apply antisymm h1,

have h3 : f (f x) ≤ f x,

{ apply hc,

exact h1, },

rwa hi at h3, },

{ apply antisymm _ h2,

have h4 : f x ≤ f (f x),

{ apply hc,

exact h2, },

rwa hi at h4, },

end

-- 2ª demostración

example

(hc : monotone f)

(hi : involutive f)

: f = id :=

begin

funext,

cases (le_total (f x) x) with h1 h2,

{ apply antisymm h1,

have h3 : f (f x) ≤ f x := hc h1,

rwa hi at h3, },

{ apply antisymm _ h2,

have h4 : f x ≤ f (f x) := hc h2,

rwa hi at h4, },

end

-- 3ª demostración

example

(hc : monotone f)

(hi : involutive f)

: f = id :=

begin

funext,

cases (le_total (f x) x) with h1 h2,

{ apply antisymm h1,

calc x

= f (f x) : (hi x).symm

... ≤ f x : hc h1 },

{ apply antisymm _ h2,

calc f x

≤ f (f x) : hc h2

... = x : hi x },

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 Una_funcion_creciente_e_involutiva_es_la_identidad
imports Main HOL.Real
begin

definition involutiva :: "(real ⇒ real) ⇒ bool"
  where "involutiva f ⟷ (∀x. f (f x) = x)"

(* 1ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "mono f"
          "involutiva f"
  shows   "f = id"
proof (unfold fun_eq_iff; intro allI)
  fix x
  have "x ≤ f x ∨ f x ≤ x"
    by (rule linear)
  then have "f x = x"
  proof (rule disjE)
    assume "x ≤ f x"
    then have "f x ≤ f (f x)"
      using assms(1) by (simp only: monoD)
    also have "… = x"
      using assms(2) by (simp only: involutiva_def)
    finally have "f x ≤ x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by (simp only: antisym)
  next
    assume "f x ≤ x"
    have "x = f (f x)"
      using assms(2) by (simp only: involutiva_def)
    also have "... ≤ f x"
      using ‹f x ≤ x› assms(1) by (simp only: monoD)
    finally have "x ≤ f x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by (simp only: monoD)
  qed
  then show "f x = id x"
    by (simp only: id_apply)
qed

(* 2ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "mono f"
          "involutiva f"
  shows   "f = id"
proof
  fix x
  have "x ≤ f x ∨ f x ≤ x"
    by (rule linear)
  then have "f x = x"
  proof
    assume "x ≤ f x"
    then have "f x ≤ f (f x)"
      using assms(1) by (simp only: monoD)
    also have "… = x"
      using assms(2) by (simp only: involutiva_def)
    finally have "f x ≤ x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by auto
  next
    assume "f x ≤ x"
    have "x = f (f x)"
      using assms(2) by (simp only: involutiva_def)
    also have "... ≤ f x"
      by (simp add: ‹f x ≤ x› assms(1) monoD)
    finally have "x ≤ f x"
      by this
    show "f x = x"
      using ‹f x ≤ x› ‹x ≤ f x› by auto
  qed
  then show "f x = id x"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "mono f"
          "involutiva f"
  shows   "f = id"
proof
  fix x
  have "x ≤ f x ∨ f x ≤ x"
    by (rule linear)
  then have "f x = x"
  proof
    assume "x ≤ f x"
    then have "f x ≤ x"
      by (metis assms involutiva_def mono_def)
    then show "f x = x"
      using ‹x ≤ f x› by auto
  next
    assume "f x ≤ x"
    then have "x ≤ f x"
      by (metis assms involutiva_def mono_def)
    then show "f x = x"
      using ‹f x ≤ x› by auto
  qed
  then show "f x = id x"
    by simp
qed

end

100

101

102

103

104

105

106

107

108

theory Una_funcion_creciente_e_involutiva_es_la_identidad

imports Main HOL.Real

begin

definition involutiva :: "(real ⇒ real) ⇒ bool"

where "involutiva f ⟷ (∀x. f (f x) = x)"

(* 1ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "mono f"

"involutiva f"

shows "f = id"

proof (unfold fun_eq_iff; intro allI)

fix x

have "x ≤ f x ∨ f x ≤ x"

by (rule linear)

then have "f x = x"

proof (rule disjE)

assume "x ≤ f x"

then have "f x ≤ f (f x)"

using assms(1) by (simp only: monoD)

also have "… = x"

using assms(2) by (simp only: involutiva_def)

finally have "f x ≤ x"

by this

show "f x = x"

using ‹f x ≤ x› ‹x ≤ f x› by (simp only: antisym)

assume "f x ≤ x"

have "x = f (f x)"

using assms(2) by (simp only: involutiva_def)

also have "... ≤ f x"

using ‹f x ≤ x› assms(1) by (simp only: monoD)

finally have "x ≤ f x"

by this

show "f x = x"

using ‹f x ≤ x› ‹x ≤ f x› by (simp only: monoD)

qed

then show "f x = id x"

by (simp only: id_apply)

qed

(* 2ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "mono f"

"involutiva f"

shows "f = id"

proof

fix x

have "x ≤ f x ∨ f x ≤ x"

by (rule linear)

then have "f x = x"

proof

assume "x ≤ f x"

then have "f x ≤ f (f x)"

using assms(1) by (simp only: monoD)

also have "… = x"

using assms(2) by (simp only: involutiva_def)

finally have "f x ≤ x"

by this

show "f x = x"

using ‹f x ≤ x› ‹x ≤ f x› by auto

assume "f x ≤ x"

have "x = f (f x)"

using assms(2) by (simp only: involutiva_def)

also have "... ≤ f x"

by (simp add: ‹f x ≤ x› assms(1) monoD)

finally have "x ≤ f x"

by this

show "f x = x"

using ‹f x ≤ x› ‹x ≤ f x› by auto

qed

then show "f x = id x"

by simp

qed

(* 3ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "mono f"

"involutiva f"

shows "f = id"

proof

fix x

have "x ≤ f x ∨ f x ≤ x"

by (rule linear)

then have "f x = x"

proof

assume "x ≤ f x"

then have "f x ≤ x"

by (metis assms involutiva_def mono_def)

then show "f x = x"

using ‹x ≤ f x› by auto

assume "f x ≤ x"

then have "x ≤ f x"

by (metis assms involutiva_def mono_def)

then show "f x = x"

using ‹f x ≤ x› by auto

qed

then show "f x = id x"

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

La composición de una función creciente y una decreciente es decreciente

PorJosé A. Alonso 20 julio 202119 julio 2021

Sea una función f de ℝ en ℝ. Se dice que f es creciente si para todo x e y tales que x ≤ y se tiene que f(x) ≤ f(y). Se dice que f es decreciente si para todo x e y tales que x ≤ y se tiene que f(x) ≥ f(y).

Demostrar que si f es creciente y g es decreciente, entonces (g ∘ f) es decreciente.

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

import data.real.basic

variables (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=
∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=
∀ {x y}, x ≤ y → f x ≥ f y

example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
sorry

import data.real.basic

variables (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=

∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=

∀ {x y}, x ≤ y → f x ≥ f y

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=
∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=
∀ {x y}, x ≤ y → f x ≥ f y

-- 1ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
begin
  intros x y hxy,
  calc (g ∘ f) x
       = g (f x)   : rfl
   ... ≥ g (f y)   : hg (hf hxy)
   ... = (g ∘ f) y : rfl,
end

-- 2ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
begin
  unfold creciente decreciente at *,
  intros x y h,
  unfold function.comp,
  apply hg,
  apply hf,
  exact h,
end

-- 3ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
begin
  intros x y h,
  apply hg,
  apply hf,
  exact h,
end

-- 4ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
begin
  intros x y h,
  apply hg,
  exact hf h,
end

-- 5ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
begin
  intros x y h,
  exact hg (hf h),
end

-- 6ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
λ x y h, hg (hf h)

-- 7ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
assume x y,
assume h : x ≤ y,
have h1 : f x ≤ f y,
  from hf h,
show (g ∘ f) x ≥ (g ∘ f) y,
  from hg h1

-- 8ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
assume x y,
assume h : x ≤ y,
show (g ∘ f) x ≥ (g ∘ f) y,
  from hg (hf h)

-- 9ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
λ x y h, hg (hf h)

-- 10ª demostración
example
  (hf : creciente f)
  (hg : decreciente g)
  : decreciente (g ∘ f) :=
-- by hint
by tauto

100

101

102

103

104

105

106

107

108

109

110

111

112

113

import data.real.basic

variables (f g : ℝ → ℝ)

def creciente (f : ℝ → ℝ) : Prop :=

∀ {x y}, x ≤ y → f x ≤ f y

def decreciente (f : ℝ → ℝ) : Prop :=

∀ {x y}, x ≤ y → f x ≥ f y

-- 1ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

begin

intros x y hxy,

calc (g ∘ f) x

= g (f x) : rfl

... ≥ g (f y) : hg (hf hxy)

... = (g ∘ f) y : rfl,

end

-- 2ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

begin

unfold creciente decreciente at *,

intros x y h,

unfold function.comp,

apply hg,

apply hf,

exact h,

end

-- 3ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

begin

intros x y h,

apply hg,

apply hf,

exact h,

end

-- 4ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

begin

intros x y h,

apply hg,

exact hf h,

end

-- 5ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

begin

intros x y h,

exact hg (hf h),

end

-- 6ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

λ x y h, hg (hf h)

-- 7ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

assume x y,

assume h : x ≤ y,

have h1 : f x ≤ f y,

from hf h,

show (g ∘ f) x ≥ (g ∘ f) y,

from hg h1

-- 8ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

assume x y,

assume h : x ≤ y,

show (g ∘ f) x ≥ (g ∘ f) y,

from hg (hf h)

-- 9ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

λ x y h, hg (hf h)

-- 10ª demostración

example

(hf : creciente f)

(hg : decreciente g)

: decreciente (g ∘ f) :=

-- by hint

by tauto

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 La_composicion_de_una_funcion_creciente_y_una_decreciente_es_decreciente
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes f g :: "real ⇒ real"
  assumes "mono f"
          "antimono g"
  shows   "antimono (g ∘ f)"
proof (rule antimonoI)
  fix x y :: real
  assume "x ≤ y"
  have "(g ∘ f) y = g (f y)"
    by (simp only: o_apply)
  also have "… ≤ g (f x)"
    using assms ‹x ≤ y›
    by (meson antimonoE monoE)
  also have "… = (g ∘ f) x"
    by (simp only: o_apply)
  finally show "(g ∘ f) x ≥ (g ∘ f) y"
    by this
qed

(* 2ª demostración *)
lemma
  fixes f g :: "real ⇒ real"
  assumes "mono f"
          "antimono g"
  shows   "antimono (g ∘ f)"
proof (rule antimonoI)
  fix x y :: real
  assume "x ≤ y"
  have "(g ∘ f) y = g (f y)"    by simp
  also have "… ≤ g (f x)"       by (meson ‹x ≤ y› assms antimonoE monoE)
  also have "… = (g ∘ f) x"     by simp
  finally show "(g ∘ f) x ≥ (g ∘ f) y" .
qed

(* 3ª demostración *)
lemma
  assumes "mono f"
          "antimono g"
  shows   "antimono (g ∘ f)"
  by (metis assms mono_def antimono_def comp_apply)

end

theory La_composicion_de_una_funcion_creciente_y_una_decreciente_es_decreciente

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes f g :: "real ⇒ real"

assumes "mono f"

"antimono g"

shows "antimono (g ∘ f)"

proof (rule antimonoI)

fix x y :: real

assume "x ≤ y"

have "(g ∘ f) y = g (f y)"

by (simp only: o_apply)

also have "… ≤ g (f x)"

using assms ‹x ≤ y›

by (meson antimonoE monoE)

also have "… = (g ∘ f) x"

by (simp only: o_apply)

finally show "(g ∘ f) x ≥ (g ∘ f) y"

by this

qed

(* 2ª demostración *)

lemma

fixes f g :: "real ⇒ real"

assumes "mono f"

"antimono g"

shows "antimono (g ∘ f)"

proof (rule antimonoI)

fix x y :: real

assume "x ≤ y"

have "(g ∘ f) y = g (f y)" by simp

also have "… ≤ g (f x)" by (meson ‹x ≤ y› assms antimonoE monoE)

also have "… = (g ∘ f) x" by simp

finally show "(g ∘ f) x ≥ (g ∘ f) y" .

qed

(* 3ª demostración *)

lemma

assumes "mono f"

"antimono g"

shows "antimono (g ∘ f)"

by (metis assms mono_def antimono_def comp_apply)

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]

La composición de crecientes es creciente

PorJosé A. Alonso 19 julio 202118 julio 2021

Se dice que una función f de ℝ en ℝ es creciente si para todo x e y tales que x ≤ y se tiene que f(x) ≤ f(y).

En Lean que f sea creciente se representa por monotone f.

Demostrar que la composición de dos funciones crecientes es una función creciente.

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

import data.real.basic

variables (f g : ℝ → ℝ)

example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
sorry

import data.real.basic

variables (f g : ℝ → ℝ)

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (f g : ℝ → ℝ)

-- 1ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
begin
  intros x y hxy,
  calc (g ∘ f) x
       = g (f x)   : rfl
   ... ≤ g (f y)   : hg (hf hxy)
   ... = (g ∘ f) y : rfl,
end

-- 2ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
begin
  unfold monotone at *,
  intros x y h,
  unfold function.comp,
  apply hg,
  apply hf,
  exact h,
end

-- 3ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
begin
  intros x y h,
  apply hg,
  apply hf,
  exact h,
end

-- 4ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
begin
  intros x xy h,
  apply hg,
  exact hf h,
end

-- 5ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
begin
  intros x y h,
  exact hg (hf h),
end

-- 6ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
λ x y h, hg (hf h)

-- 7ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
begin
  intros x y h,
  specialize hf h,
  exact hg hf,
end

-- 8ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
assume x y,
assume h1 : x ≤ y,
have h2 : f x ≤ f y,
  from hf h1,
show (g ∘ f) x ≤ (g ∘ f) y, from
  calc (g ∘ f) x
       = g (f x)   : rfl
   ... ≤ g (f y)   : hg h2
   ... = (g ∘ f) y : by refl

-- 9ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
-- by hint
by tauto

-- 10ª demostración
example
  (hf : monotone f)
  (hg : monotone g)
  : monotone (g ∘ f) :=
-- by library_search
monotone.comp hg hf

100

101

102

103

104

105

106

107

108

109

110

111

112

import data.real.basic

variables (f g : ℝ → ℝ)

-- 1ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

begin

intros x y hxy,

calc (g ∘ f) x

= g (f x) : rfl

... ≤ g (f y) : hg (hf hxy)

... = (g ∘ f) y : rfl,

end

-- 2ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

begin

unfold monotone at *,

intros x y h,

unfold function.comp,

apply hg,

apply hf,

exact h,

end

-- 3ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

begin

intros x y h,

apply hg,

apply hf,

exact h,

end

-- 4ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

begin

intros x xy h,

apply hg,

exact hf h,

end

-- 5ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

begin

intros x y h,

exact hg (hf h),

end

-- 6ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

λ x y h, hg (hf h)

-- 7ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

begin

intros x y h,

specialize hf h,

exact hg hf,

end

-- 8ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

assume x y,

assume h1 : x ≤ y,

have h2 : f x ≤ f y,

from hf h1,

show (g ∘ f) x ≤ (g ∘ f) y, from

calc (g ∘ f) x

= g (f x) : rfl

... ≤ g (f y) : hg h2

... = (g ∘ f) y : by refl

-- 9ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

-- by hint

by tauto

-- 10ª demostración

example

(hf : monotone f)

(hg : monotone g)

: monotone (g ∘ f) :=

-- by library_search

monotone.comp hg hf

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 La_composicion_de_crecientes_es_creciente
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes f g :: "real ⇒ real"
  assumes "mono f"
          "mono g"
  shows   "mono (g ∘ f)"
proof (rule monoI)
  fix x y :: real
  assume "x ≤ y"
  have "(g ∘ f) x = g (f x)"
    by (simp only: o_apply)
  also have "… ≤ g (f y)"
    using assms ‹x ≤ y›
    by (simp only: monoD)
  also have "… = (g ∘ f) y"
    by (simp only: o_apply)
  finally show "(g ∘ f) x ≤ (g ∘ f) y"
    by this
qed

(* 2ª demostración *)
lemma
  fixes f g :: "real ⇒ real"
  assumes "mono f"
          "mono g"
  shows   "mono (g ∘ f)"
proof (rule monoI)
  fix x y :: real
  assume "x ≤ y"
  have "(g ∘ f) x = g (f x)"   by simp
  also have "… ≤ g (f y)"      by (simp add: ‹x ≤ y› assms monoD)
  also have "… = (g ∘ f) y"    by simp
  finally show "(g ∘ f) x ≤ (g ∘ f) y" .
qed

(* 3ª demostración *)
lemma
  assumes "mono f"
          "mono g"
  shows   "mono (g ∘ f)"
  by (metis assms comp_def mono_def)

end

theory La_composicion_de_crecientes_es_creciente

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes f g :: "real ⇒ real"

assumes "mono f"

"mono g"

shows "mono (g ∘ f)"

proof (rule monoI)

fix x y :: real

assume "x ≤ y"

have "(g ∘ f) x = g (f x)"

by (simp only: o_apply)

also have "… ≤ g (f y)"

using assms ‹x ≤ y›

by (simp only: monoD)

also have "… = (g ∘ f) y"

by (simp only: o_apply)

finally show "(g ∘ f) x ≤ (g ∘ f) y"

by this

qed

(* 2ª demostración *)

lemma

fixes f g :: "real ⇒ real"

assumes "mono f"

"mono g"

shows "mono (g ∘ f)"

proof (rule monoI)

fix x y :: real

assume "x ≤ y"

have "(g ∘ f) x = g (f x)" by simp

also have "… ≤ g (f y)" by (simp add: ‹x ≤ y› assms monoD)

also have "… = (g ∘ f) y" by simp

finally show "(g ∘ f) x ≤ (g ∘ f) y" .

qed

(* 3ª demostración *)

lemma

assumes "mono f"

"mono g"

shows "mono (g ∘ f)"

by (metis assms comp_def mono_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]

Teorema del emparedado

PorJosé A. Alonso 18 julio 202118 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 el teorema del emparedado; es decir, que si para todo n, u(n) ≤ v(n) ≤ w(n) y u(n) tiene el mismo límite que w(n), entonces v(n) también tiene dicho límite.

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

import data.real.basic

variables (u v w : ℕ → ℝ)
variable  (a : ℝ)

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

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

example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
sorry

import data.real.basic

variables (u v w : ℕ → ℝ)

variable (a : ℝ)

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

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

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

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (u v w : ℕ → ℝ)
variable  (a : ℝ)

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

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

-- Nota. En la demostración se usará el siguiente lema:
lemma max_ge_iff
  {p q r : ℕ}
  : r ≥ max p q ↔ r ≥ p ∧ r ≥ q :=
max_le_iff

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

example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
begin
  intros ε hε,
  cases hu ε hε with N hN, clear hu,
  cases hw ε hε with N' hN', clear hw hε,
  use max N N',
  intros n hn,
  rw max_ge_iff at hn,
  specialize hN n hn.1,
  specialize hN' n hn.2,
  specialize h n,
  specialize h' n,
  clear hn,
  rw abs_le at *,
  split,
  { calc -ε
         ≤ u n - a : hN.1
     ... ≤ v n - a : by linarith, },
  { calc v n - a
         ≤ w n - a : by linarith
     ... ≤ ε       : hN'.2, },
end

-- 2ª demostración
example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
begin
  intros ε hε,
  cases hu ε hε with N hN, clear hu,
  cases hw ε hε with N' hN', clear hw hε,
  use max N N',
  intros n hn,
  rw max_ge_iff at hn,
  specialize hN n (by linarith),
  specialize hN' n (by linarith),
  specialize h n,
  specialize h' n,
  rw abs_le at *,
  split,
  { linarith, },
  { linarith, },
end

-- 3ª demostración
example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
begin
  intros ε hε,
  cases hu ε hε with N hN, clear hu,
  cases hw ε hε with N' hN', clear hw hε,
  use max N N',
  intros n hn,
  rw max_ge_iff at hn,
  specialize hN n (by linarith),
  specialize hN' n (by linarith),
  specialize h n,
  specialize h' n,
  rw abs_le at *,
  split ; linarith,
end

-- 4ª demostración
example
  (hu : limite u a)
  (hw : limite w a)
  (h : ∀ n, u n ≤ v n)
  (h' : ∀ n, v n ≤ w n) :
  limite v a :=
assume ε,
assume hε : ε > 0,
exists.elim (hu ε hε)
  ( assume N,
    assume hN : ∀ (n : ℕ), n ≥ N → |u n - a| ≤ ε,
    exists.elim (hw ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |w n - a| ≤ ε,
        show ∃ N, ∀ n, n ≥ N → |v n - a| ≤ ε, from
          exists.intro (max N N')
            ( assume n,
              assume hn : n ≥ max N N',
              have h1 : n ≥ N ∧ n ≥ N',
                from max_ge_iff.mp hn,
              have h2 : -ε ≤ v n - a,
                { have h2a : |u n - a| ≤ ε,
                    from hN n h1.1,
                  calc -ε
                       ≤ u n - a : and.left (abs_le.mp h2a)
                   ... ≤ v n - a : by linarith [h n], },
              have h3 : v n - a ≤ ε,
                { have h3a : |w n - a| ≤ ε,
                    from hN' n h1.2,
                  calc v n - a
                       ≤ w n - a : by linarith [h' n]
                   ... ≤ ε       : and.right (abs_le.mp h3a), },
              show |v n - a| ≤ ε,
                from abs_le.mpr (and.intro h2 h3))))

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

import data.real.basic

variables (u v w : ℕ → ℝ)

variable (a : ℝ)

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

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

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

-- Nota. En la demostración se usará el siguiente lema:

lemma max_ge_iff

{p q r : ℕ}

: r ≥ max p q ↔ r ≥ p ∧ r ≥ q :=

max_le_iff

-- 1ª demostración

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

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

begin

intros ε hε,

cases hu ε hε with N hN, clear hu,

cases hw ε hε with N' hN', clear hw hε,

use max N N',

intros n hn,

rw max_ge_iff at hn,

specialize hN n hn.1,

specialize hN' n hn.2,

specialize h n,

specialize h' n,

clear hn,

rw abs_le at *,

split,

{ calc -ε

≤ u n - a : hN.1

... ≤ v n - a : by linarith, },

{ calc v n - a

≤ w n - a : by linarith

... ≤ ε : hN'.2, },

end

-- 2ª demostración

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

begin

intros ε hε,

cases hu ε hε with N hN, clear hu,

cases hw ε hε with N' hN', clear hw hε,

use max N N',

intros n hn,

rw max_ge_iff at hn,

specialize hN n (by linarith),

specialize hN' n (by linarith),

specialize h n,

specialize h' n,

rw abs_le at *,

split,

{ linarith, },

end

-- 3ª demostración

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

begin

intros ε hε,

cases hu ε hε with N hN, clear hu,

cases hw ε hε with N' hN', clear hw hε,

use max N N',

intros n hn,

rw max_ge_iff at hn,

specialize hN n (by linarith),

specialize hN' n (by linarith),

specialize h n,

specialize h' n,

rw abs_le at *,

split ; linarith,

end

-- 4ª demostración

example

(hu : limite u a)

(hw : limite w a)

(h : ∀ n, u n ≤ v n)

(h' : ∀ n, v n ≤ w n) :

limite v a :=

assume ε,

assume hε : ε > 0,

exists.elim (hu ε hε)

( assume N,

assume hN : ∀ (n : ℕ), n ≥ N → |u n - a| ≤ ε,

exists.elim (hw ε hε)

( assume N',

assume hN' : ∀ (n : ℕ), n ≥ N' → |w n - a| ≤ ε,

show ∃ N, ∀ n, n ≥ N → |v n - a| ≤ ε, from

exists.intro (max N N')

( assume n,

assume hn : n ≥ max N N',

have h1 : n ≥ N ∧ n ≥ N',

from max_ge_iff.mp hn,

have h2 : -ε ≤ v n - a,

{ have h2a : |u n - a| ≤ ε,

from hN n h1.1,

calc -ε

≤ u n - a : and.left (abs_le.mp h2a)

... ≤ v n - a : by linarith [h n], },

have h3 : v n - a ≤ ε,

{ have h3a : |w n - a| ≤ ε,

from hN' n h1.2,

calc v n - a

≤ w n - a : by linarith [h' n]

... ≤ ε : and.right (abs_le.mp h3a), },

show |v n - a| ≤ ε,

from abs_le.mpr (and.intro h2 h3))))

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 Teorema_del_emparedado
imports Main HOL.Real
begin

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

lemma
  assumes "limite u a"
          "limite w a"
          "∀n. u n ≤ v n"
          "∀n. v n ≤ w n"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume hε : "0 < ε"
  obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"
    using assms(1) hε limite_def
    by auto
  obtain N' where hN' : "∀n≥N'. ¦w n - a¦ < ε"
    using assms(2) hε limite_def
    by auto
  have "∀n≥max N N'. ¦v n - a¦ < ε"
  proof (intro allI impI)
    fix n
    assume hn : "n≥max N N'"
    have "v n - a < ε"
    proof -
      have "v n - a ≤ w n - a"
        using assms(4) by simp
      also have "… ≤ ¦w n - a¦"
        by simp
      also have "… < ε"
        using hN' hn by auto
      finally show "v n - a < ε" .
    qed
    moreover
    have "-(v n - a) < ε"
    proof -
      have "-(v n - a) ≤ -(u n - a)"
        using assms(3) by auto
      also have "… ≤ ¦u n - a¦"
        by simp
      also have "… < ε"
        using hN hn by auto
      finally show "-(v n - a) < ε" .
    qed
    ultimately show "¦v n - a¦ < ε"
      by (simp only: abs_less_iff)
  qed
  then show "∃k. ∀n≥k. ¦v n - a¦ < ε"
    by (rule exI)
qed

end

theory Teorema_del_emparedado

imports Main HOL.Real

begin

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

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

lemma

assumes "limite u a"

"limite w a"

"∀n. u n ≤ v n"

"∀n. v n ≤ w n"

shows "limite v a"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume hε : "0 < ε"

obtain N where hN : "∀n≥N. ¦u n - a¦ < ε"

using assms(1) hε limite_def

by auto

obtain N' where hN' : "∀n≥N'. ¦w n - a¦ < ε"

using assms(2) hε limite_def

by auto

have "∀n≥max N N'. ¦v n - a¦ < ε"

proof (intro allI impI)

fix n

assume hn : "n≥max N N'"

have "v n - a < ε"

proof -

have "v n - a ≤ w n - a"

using assms(4) by simp

also have "… ≤ ¦w n - a¦"

by simp

also have "… < ε"

using hN' hn by auto

finally show "v n - a < ε" .

qed

moreover

have "-(v n - a) < ε"

proof -

have "-(v n - a) ≤ -(u n - a)"

using assms(3) by auto

also have "… ≤ ¦u n - a¦"

by simp

also have "… < ε"

using hN hn by auto

finally show "-(v n - a) < ε" .

qed

ultimately show "¦v n - a¦ < ε"

by (simp only: abs_less_iff)

qed

then show "∃k. ∀n≥k. ¦v n - a¦ < ε"

by (rule exI)

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]

Producto de sucesiones convergentes a cero

PorJosé A. Alonso 17 julio 202117 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 las sucesiones u(n) y v(n) convergen a cero, entonces u(n)·v(n) también converge a cero.

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

import data.real.basic
import tactic

variables {u v : ℕ → ℝ}
variables {: ℝ}

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

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
sorry

import data.real.basic

import tactic

variables {u v : ℕ → ℝ}

variables {: ℝ}

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

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

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variables {u v : ℕ → ℝ}
variables {: ℝ}

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

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

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
begin
  intros ε hε,
  cases hu ε hε with U hU,
  cases hv 1 zero_lt_one with V hV,
  set N := max U V with hN,
  use N,
  intros n hn,
  specialize hU n (le_of_max_le_left hn),
  specialize hV n (le_of_max_le_right hn),
  rw sub_zero at *,
  calc |(u * v) n|
       = |u n * v n|   : rfl
   ... = |u n| * |v n| : abs_mul (u n) (v n)
   ... < ε * 1         : mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))
   ... = ε             : mul_one ε,
end

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
begin
  intros ε hε,
  cases hu ε hε with U hU,
  cases hv 1 (by linarith) with V hV,
  set N := max U V with hN,
  use N,
  intros n hn,
  specialize hU n (le_of_max_le_left hn),
  specialize hV n (le_of_max_le_right hn),
  rw sub_zero at *,
  calc |(u * v) n|
       = |u n * v n|   : rfl
   ... = |u n| * |v n| : abs_mul (u n) (v n)
   ... < ε * 1         : by { apply mul_lt_mul'' hU hV ; simp [abs_nonneg] }
   ... = ε             : mul_one ε,
end

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

example
  (hu : limite u 0)
  (hv : limite v 0)
  : limite (u * v) 0 :=
begin
  intros ε hε,
  cases hu ε hε with U hU,
  cases hv 1 (by linarith) with V hV,
  set N := max U V with hN,
  use N,
  intros n hn,
  have hUN : U ≤ N := le_max_left U V,
  have hVN : V ≤ N := le_max_right U V,
  specialize hU n (by linarith),
  specialize hV n (by linarith),
  rw sub_zero at ⊢ hU hV,
  rw pi.mul_apply,
  rw abs_mul,
  convert mul_lt_mul'' hU hV _ _, simp,
  all_goals {apply abs_nonneg},
end

import data.real.basic

import tactic

variables {u v : ℕ → ℝ}

variables {: ℝ}

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

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

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

-- 1ª demostración

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

begin

intros ε hε,

cases hu ε hε with U hU,

cases hv 1 zero_lt_one with V hV,

set N := max U V with hN,

use N,

intros n hn,

specialize hU n (le_of_max_le_left hn),

specialize hV n (le_of_max_le_right hn),

rw sub_zero at *,

calc |(u * v) n|

= |u n * v n| : rfl

... = |u n| * |v n| : abs_mul (u n) (v n)

... < ε * 1 : mul_lt_mul'' hU hV (abs_nonneg (u n)) (abs_nonneg (v n))

... = ε : mul_one ε,

end

-- 2ª demostración

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

begin

intros ε hε,

cases hu ε hε with U hU,

cases hv 1 (by linarith) with V hV,

set N := max U V with hN,

use N,

intros n hn,

specialize hU n (le_of_max_le_left hn),

specialize hV n (le_of_max_le_right hn),

rw sub_zero at *,

calc |(u * v) n|

= |u n * v n| : rfl

... = |u n| * |v n| : abs_mul (u n) (v n)

... < ε * 1 : by { apply mul_lt_mul'' hU hV ; simp [abs_nonneg] }

... = ε : mul_one ε,

end

-- 3ª demostración

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

example

(hu : limite u 0)

(hv : limite v 0)

: limite (u * v) 0 :=

begin

intros ε hε,

cases hu ε hε with U hU,

cases hv 1 (by linarith) with V hV,

set N := max U V with hN,

use N,

intros n hn,

have hUN : U ≤ N := le_max_left U V,

have hVN : V ≤ N := le_max_right U V,

specialize hU n (by linarith),

specialize hV n (by linarith),

rw sub_zero at ⊢ hU hV,

rw pi.mul_apply,

rw abs_mul,

convert mul_lt_mul'' hU hV _ _, simp,

all_goals {apply abs_nonneg},

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 Producto_de_sucesiones_convergentes_a_cero
imports Main HOL.Real
begin

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

lemma
  assumes "limite u 0"
          "limite v 0"
  shows   "limite (λ n. u n * v n) 0"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume  hε : "0 < ε"
  then obtain U where hU : "∀n≥U. ¦u n - 0¦ < ε"
    using assms(1) limite_def
    by auto
  obtain V where hV : "∀n≥V. ¦v n - 0¦ < 1"
    using hε assms(2) limite_def
    by fastforce
  have "∀n≥max U V. ¦u n * v n - 0¦ < ε"
  proof (intro allI impI)
    fix n
    assume hn : "max U V ≤ n"
    then have "U ≤ n"
      by simp
    then have "¦u n - 0¦ < ε"
      using hU by blast
    have hnV : "V ≤ n"
      using hn by simp
    then have "¦v n - 0¦ < 1"
      using hV by blast
    have "¦u n * v n - 0¦ = ¦(u n - 0) * (v n - 0)¦"
      by simp
    also have "… = ¦u n - 0¦ * ¦v n - 0¦"
      by (simp add: abs_mult)
    also have "… < ε * 1"
      using ‹¦u n - 0¦ < ε› ‹¦v n - 0¦ < 1›
      by (rule abs_mult_less)
    also have "… = ε"
      by simp
    finally show "¦u n * v n - 0¦ < ε"
      by this
  qed
  then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"
    by (rule exI)
qed

end

theory Producto_de_sucesiones_convergentes_a_cero

imports Main HOL.Real

begin

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

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

lemma

assumes "limite u 0"

"limite v 0"

shows "limite (λ n. u n * v n) 0"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume hε : "0 < ε"

then obtain U where hU : "∀n≥U. ¦u n - 0¦ < ε"

using assms(1) limite_def

by auto

obtain V where hV : "∀n≥V. ¦v n - 0¦ < 1"

using hε assms(2) limite_def

by fastforce

have "∀n≥max U V. ¦u n * v n - 0¦ < ε"

proof (intro allI impI)

fix n

assume hn : "max U V ≤ n"

then have "U ≤ n"

by simp

then have "¦u n - 0¦ < ε"

using hU by blast

have hnV : "V ≤ n"

using hn by simp

then have "¦v n - 0¦ < 1"

using hV by blast

have "¦u n * v n - 0¦ = ¦(u n - 0) * (v n - 0)¦"

by simp

also have "… = ¦u n - 0¦ * ¦v n - 0¦"

by (simp add: abs_mult)

also have "… < ε * 1"

using ‹¦u n - 0¦ < ε› ‹¦v n - 0¦ < 1›

by (rule abs_mult_less)

also have "… = ε"

by simp

finally show "¦u n * v n - 0¦ < ε"

by this

qed

then show "∃k. ∀n≥k. ¦u n * v n - 0¦ < ε"

by (rule exI)

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]

El límite de u(n) es a si y solo si el de u(n)-a es 0

PorJosé A. Alonso 16 julio 20218 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 u(n) es a si y solo si el de u(n)-a es 0.

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

import data.real.basic
import tactic

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

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

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

example
  : limite u a ↔ limite (λ i, u i - a) 0 :=
sorry

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

variables {a c x : ℝ}

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

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

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

example

: limite u a ↔ limite (λ i, u i - a) 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

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

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

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

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

example
  : limite u a ↔ limite (λ i, u i - a) 0 :=
begin
  split,
  { intros h ε hε,
    convert h ε hε,
    norm_num, },
  { intros h ε hε,
    convert h ε hε,
    norm_num, },
end

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

example
  : limite u a ↔ limite (λ i, u i - a) 0 :=
begin
  split;
  { intros h ε hε,
    convert h ε hε,
    norm_num, },
end

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

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

lemma CNS_limite_con_suma
  (c : ℝ)
  : limite u a ↔ limite (λ i, u i + c) (a + c) :=
begin
  split,
  { apply limite_con_suma },
  { intro h,
    convert limite_con_suma (-c) h; simp, },
end

example
  (u : ℕ → ℝ)
  (a : ℝ)
  : limite u a ↔ limite (λ i, u i - a) 0 :=
begin
  convert CNS_limite_con_suma (-a),
  simp,
end

import data.real.basic

import tactic

variable {u : ℕ → ℝ}

variables {a c x : ℝ}

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

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

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

-- 1ª demostración

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

example

: limite u a ↔ limite (λ i, u i - a) 0 :=

begin

split,

{ intros h ε hε,

convert h ε hε,

norm_num, },

{ intros h ε hε,

convert h ε hε,

norm_num, },

end

-- 2ª demostración

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

example

: limite u a ↔ limite (λ i, u i - a) 0 :=

begin

split;

{ intros h ε hε,

convert h ε hε,

norm_num, },

end

-- 3ª demostración

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

lemma limite_con_suma

(c : ℝ)

(h : limite u a)

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

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

lemma CNS_limite_con_suma

(c : ℝ)

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

begin

split,

{ apply limite_con_suma },

{ intro h,

convert limite_con_suma (-c) h; simp, },

end

example

(u : ℕ → ℝ)

(a : ℝ)

: limite u a ↔ limite (λ i, u i - a) 0 :=

begin

convert CNS_limite_con_suma (-a),

simp,

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 "El_limite_de_u_es_a_syss_el_de_u-a_es_0"
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 u a ⟷ limite (λ i. u i - a) 0"
proof -
  have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)"
    by (rule limite_def)
  also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"
    by simp
  also have "… ⟷ limite (λ i. u i - a) 0"
    by (rule limite_def[symmetric])
  finally show "limite u a ⟷ limite (λ i. u i - a) 0"
    by this
qed

(* 2ª demostración *)

lemma
  "limite u a ⟷ limite (λ i. u i - a) 0"
proof -
  have "limite u a ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - a¦ < ε)"
    by (simp only: limite_def)
  also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"
    by simp
  also have "… ⟷ limite (λ i. u i - a) 0"
    by (simp only: limite_def)
  finally show "limite u a ⟷ limite (λ i. u i - a) 0"
    by this
qed

(* 3ª demostración *)

lemma
  "limite u a ⟷ limite (λ i. u i - a) 0"
  using limite_def
  by simp

end

theory "El_limite_de_u_es_a_syss_el_de_u-a_es_0"

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 u a ⟷ limite (λ i. u i - a) 0"

proof -

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

by (rule limite_def)

also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"

by simp

also have "… ⟷ limite (λ i. u i - a) 0"

by (rule limite_def[symmetric])

finally show "limite u a ⟷ limite (λ i. u i - a) 0"

by this

qed

(* 2ª demostración *)

lemma

"limite u a ⟷ limite (λ i. u i - a) 0"

proof -

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

by (simp only: limite_def)

also have "… ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦(u n - a) - 0¦ < ε)"

by simp

also have "… ⟷ limite (λ i. u i - a) 0"

by (simp only: limite_def)

finally show "limite u a ⟷ limite (λ i. u i - a) 0"

by this

qed

(* 3ª demostración *)

lemma

"limite u a ⟷ limite (λ i. u i - a) 0"

using 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]

Límite multiplicado por una constante

PorJosé A. Alonso 15 julio 20217 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 u(i) es a, entonces el de c·u(i) es c·a.

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

import data.real.basic
import tactic

variables (u v : ℕ → ℝ)
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 (λ n, c * (u n)) (c * a) :=
sorry

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

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 (λ n, c * (u n)) (c * a) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variables (u v : ℕ → ℝ)
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 (λ n, c * (u n)) (c * a) :=
begin
  by_cases hc : c = 0,
  { subst hc,
    intros ε hε,
    by finish, },
  { intros ε hε,
    have hc' : 0 < |c| := abs_pos.mpr hc,
    have hεc : 0 < ε / |c| := div_pos hε hc',
    specialize h (ε/|c|) hεc,
    cases h with N hN,
    use N,
    intros n hn,
    specialize hN n hn,
    dsimp only,
    rw ← mul_sub,
    rw abs_mul,
    rw ← lt_div_iff' hc',
    exact hN, }
end

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

example
  (h : limite u a)
  : limite (λ n, c * (u n)) (c * a) :=
begin
  by_cases hc : c = 0,
  { subst hc,
    intros ε hε,
    by finish, },
  { intros ε hε,
    have hc' : 0 < |c| := by finish,
    have hεc : 0 < ε / |c| := div_pos hε hc',
    cases h (ε/|c|) hεc with N hN,
    use N,
    intros n hn,
    specialize hN n hn,
    dsimp only,
    rw [← mul_sub, abs_mul, ← lt_div_iff' hc'],
    exact hN, }
end

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

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 (λ n, c * (u n)) (c * a) :=

begin

by_cases hc : c = 0,

{ subst hc,

intros ε hε,

by finish, },

{ intros ε hε,

have hc' : 0 < |c| := abs_pos.mpr hc,

have hεc : 0 < ε / |c| := div_pos hε hc',

specialize h (ε/|c|) hεc,

cases h with N hN,

use N,

intros n hn,

specialize hN n hn,

dsimp only,

rw ← mul_sub,

rw abs_mul,

rw ← lt_div_iff' hc',

exact hN, }

end

-- 2ª demostración

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

example

(h : limite u a)

: limite (λ n, c * (u n)) (c * a) :=

begin

by_cases hc : c = 0,

{ subst hc,

intros ε hε,

by finish, },

{ intros ε hε,

have hc' : 0 < |c| := by finish,

have hεc : 0 < ε / |c| := div_pos hε hc',

cases h (ε/|c|) hεc with N hN,

use N,

intros n hn,

specialize hN n hn,

dsimp only,

rw [← mul_sub, abs_mul, ← lt_div_iff' hc'],

exact hN, }

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 Limite_multiplicado_por_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¦ < ε)"

lemma
  assumes "limite u a"
  shows   "limite (λ n. c * u n) (c * a)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦c * u n - c * a¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε"
    proof (cases "c = 0")
      assume "c = 0"
      then show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε"
        by (simp add: ‹0 < ε›)
    next
      assume "c ≠ 0"
      then have "0 < ¦c¦"
        by simp
      then have "0 < ε/¦c¦"
        by (simp add: ‹0 < ε›)
      then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε/¦c¦"
        using assms limite_def
        by auto
      have "∀n≥N. ¦c * u n - c * a¦ < ε"
      proof (intro allI impI)
        fix n
        assume "n ≥ N"
        have "¦c * u n - c * a¦ = ¦c * (u n - a)¦"
          by argo
        also have "… = ¦c¦ * ¦u n - a¦"
          by (simp only: abs_mult)
        also have "… < ¦c¦ * (ε/¦c¦)"
          using hN ‹n ≥ N› ‹0 < ¦c¦›
          by (simp only: mult_strict_left_mono)
        finally show "¦c * u n - c * a¦ < ε"
          using ‹0 < ¦c¦›
          by auto
      qed
      then show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε"
        by (rule exI)
    qed
  qed
qed

end

theory Limite_multiplicado_por_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¦ < ε)"

lemma

assumes "limite u a"

shows "limite (λ n. c * u n) (c * a)"

proof (unfold limite_def)

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

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

show "∃k. ∀n≥k. ¦c * u n - c * a¦ < ε"

proof (cases "c = 0")

assume "c = 0"

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

by (simp add: ‹0 < ε›)

assume "c ≠ 0"

then have "0 < ¦c¦"

by simp

then have "0 < ε/¦c¦"

by (simp add: ‹0 < ε›)

then obtain N where hN : "∀n≥N. ¦u n - a¦ < ε/¦c¦"

using assms limite_def

by auto

have "∀n≥N. ¦c * u n - c * a¦ < ε"

proof (intro allI impI)

fix n

assume "n ≥ N"

have "¦c * u n - c * a¦ = ¦c * (u n - a)¦"

by argo

also have "… = ¦c¦ * ¦u n - a¦"

by (simp only: abs_mult)

also have "… < ¦c¦ * (ε/¦c¦)"

using hN ‹n ≥ N› ‹0 < ¦c¦›

by (simp only: mult_strict_left_mono)

finally show "¦c * u n - c * a¦ < ε"

using ‹0 < ¦c¦›

by auto

qed

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

by (rule exI)

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 la suma de sucesiones convergentes

PorJosé A. Alonso 14 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 el límite de la suma de dos sucesiones convergentes es la suma de los límites de dichas sucesiones.

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

import data.real.basic

variables (u v : ℕ → ℝ)
variables (a b : ℝ)

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

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
sorry

import data.real.basic

variables (u v : ℕ → ℝ)

variables (a b : ℝ)

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

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

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

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (u v : ℕ → ℝ)
variables (a b : ℝ)

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

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

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  have hε2 : 0 < ε / 2,
    { linarith },
  cases hu (ε / 2) hε2 with Nu hNu,
  cases hv (ε / 2) hε2 with Nv hNv,
  clear hu hv hε2 hε,
  use max Nu Nv,
  intros n hn,
  have hn₁ : n ≥ Nu,
    { exact le_of_max_le_left hn },
  specialize hNu n hn₁,
  have hn₂ : n ≥ Nv,
    { exact le_of_max_le_right hn },
  specialize hNv n hn₂,
  clear hn hn₁ hn₂ Nu Nv,
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|  : by refl
   ... = |(u n - a) + (v n -  b)| : by {congr, ring}
   ... ≤ |u n - a| + |v n -  b|   : by apply abs_add
   ... < ε / 2 + ε / 2            : by linarith
   ... = ε                        : by apply add_halves,
end

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  have hn₁ : n ≥ Nu := le_of_max_le_left hn,
  specialize hNu n hn₁,
  have hn₂ : n ≥ Nv := le_of_max_le_right hn,
  specialize hNv n hn₂,
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|  : by refl
   ... = |(u n - a) + (v n -  b)| : by {congr, ring}
   ... ≤ |u n - a| + |v n -  b|   : by apply abs_add
   ... < ε / 2 + ε / 2            : by linarith
   ... = ε                        : by apply add_halves,
end

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

lemma max_ge_iff
  {α : Type*}
  [linear_order α]
  {p q r : α}
  : r ≥ max p q  ↔ r ≥ p ∧ r ≥ q :=
max_le_iff

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  cases max_ge_iff.mp hn with hn₁ hn₂,
  have cota₁ : |u n - a| < ε/2 := hNu n hn₁,
  have cota₂ : |v n - b| < ε/2 := hNv n hn₂,
  calc |(u + v) n - (a + b)|
       = |u n + v n - (a + b)|   : by rfl
   ... = |(u n - a) + (v n - b)| : by { congr, ring }
   ... ≤ |u n - a| + |v n - b|   : by apply abs_add
   ... < ε                       : by linarith,
end

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  cases max_ge_iff.mp hn with hn₁ hn₂,
  calc |(u + v) n - (a + b)|
       = |u n + v n - (a + b)|   : by refl
   ... = |(u n - a) + (v n - b)| : by { congr, ring }
   ... ≤ |u n - a| + |v n - b|   : by apply abs_add
   ... < ε/2 + ε/2               : add_lt_add (hNu n hn₁) (hNv n hn₂)
   ... = ε                       : by simp
end

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with Nu hNu,
  cases hv (ε/2) (by linarith) with Nv hNv,
  use max Nu Nv,
  intros n hn,
  rw max_ge_iff at hn,
  calc |(u + v) n - (a + b)|
       = |u n + v n - (a + b)|   : by refl
   ... = |(u n - a) + (v n - b)| : by { congr, ring }
   ... ≤ |u n - a| + |v n - b|   : by apply abs_add
   ... < ε                       : by linarith [hNu n (by linarith), hNv n (by linarith)],
end

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

example
  (hu : limite u a)
  (hv : limite v b)
  : limite (u + v) (a + b) :=
begin
  intros ε Hε,
  cases hu (ε/2) (by linarith) with L HL,
  cases hv (ε/2) (by linarith) with M HM,
  set N := max L M with hN,
  use N,
  have HLN : N ≥ L := le_max_left _ _,
  have HMN : N ≥ M := le_max_right _ _,
  intros n Hn,
  have H3 : |u n - a| < ε/2 := HL n (by linarith),
  have H4 : |v n - b| < ε/2 := HM n (by linarith),
  calc |(u + v) n - (a + b)|
       = |(u n + v n) - (a + b)|   : by refl
   ... = |(u n - a) + (v n - b)|   : by { congr, ring }
   ... ≤ |(u n - a)| + |(v n - b)| : by apply abs_add
   ... < ε/2 + ε/2                 : by linarith
   ... = ε                         : by ring
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

import data.real.basic

variables (u v : ℕ → ℝ)

variables (a b : ℝ)

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

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

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

-- 1ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

begin

intros ε hε,

have hε2 : 0 < ε / 2,

{ linarith },

cases hu (ε / 2) hε2 with Nu hNu,

cases hv (ε / 2) hε2 with Nv hNv,

clear hu hv hε2 hε,

use max Nu Nv,

intros n hn,

have hn₁ : n ≥ Nu,

{ exact le_of_max_le_left hn },

specialize hNu n hn₁,

have hn₂ : n ≥ Nv,

{ exact le_of_max_le_right hn },

specialize hNv n hn₂,

clear hn hn₁ hn₂ Nu Nv,

calc |(u + v) n - (a + b)|

= |(u n + v n) - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by {congr, ring}

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε / 2 + ε / 2 : by linarith

... = ε : by apply add_halves,

end

-- 2ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

have hn₁ : n ≥ Nu := le_of_max_le_left hn,

specialize hNu n hn₁,

have hn₂ : n ≥ Nv := le_of_max_le_right hn,

specialize hNv n hn₂,

calc |(u + v) n - (a + b)|

= |(u n + v n) - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by {congr, ring}

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε / 2 + ε / 2 : by linarith

... = ε : by apply add_halves,

end

-- 3ª demostración

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

lemma max_ge_iff

{α : Type*}

[linear_order α]

{p q r : α}

: r ≥ max p q ↔ r ≥ p ∧ r ≥ q :=

max_le_iff

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

cases max_ge_iff.mp hn with hn₁ hn₂,

have cota₁ : |u n - a| < ε/2 := hNu n hn₁,

have cota₂ : |v n - b| < ε/2 := hNv n hn₂,

calc |(u + v) n - (a + b)|

= |u n + v n - (a + b)| : by rfl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε : by linarith,

end

-- 4ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

cases max_ge_iff.mp hn with hn₁ hn₂,

calc |(u + v) n - (a + b)|

= |u n + v n - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε/2 + ε/2 : add_lt_add (hNu n hn₁) (hNv n hn₂)

... = ε : by simp

end

-- 5ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

begin

intros ε hε,

cases hu (ε/2) (by linarith) with Nu hNu,

cases hv (ε/2) (by linarith) with Nv hNv,

use max Nu Nv,

intros n hn,

rw max_ge_iff at hn,

calc |(u + v) n - (a + b)|

= |u n + v n - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |u n - a| + |v n - b| : by apply abs_add

... < ε : by linarith [hNu n (by linarith), hNv n (by linarith)],

end

-- 6ª demostración

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

example

(hu : limite u a)

(hv : limite v b)

: limite (u + v) (a + b) :=

begin

intros ε Hε,

cases hu (ε/2) (by linarith) with L HL,

cases hv (ε/2) (by linarith) with M HM,

set N := max L M with hN,

use N,

have HLN : N ≥ L := le_max_left _ _,

have HMN : N ≥ M := le_max_right _ _,

intros n Hn,

have H3 : |u n - a| < ε/2 := HL n (by linarith),

have H4 : |v n - b| < ε/2 := HM n (by linarith),

calc |(u + v) n - (a + b)|

= |(u n + v n) - (a + b)| : by refl

... = |(u n - a) + (v n - b)| : by { congr, ring }

... ≤ |(u n - a)| + |(v n - b)| : by apply abs_add

... < ε/2 + ε/2 : by linarith

... = ε : by ring

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 Limite_de_la_suma_de_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¦ < ε)"

(* 1ª demostración *)

lemma
  assumes "limite u a"
          "limite v b"
  shows   "limite (λ n. u n + v n) (a + b)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then have "0 < ε/2"
      by simp
    then have "∃k. ∀n≥k. ¦u n - a¦ < ε/2"
      using assms(1) limite_def by blast
    then obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"
      by (rule exE)
    then have "∃k. ∀n≥k. ¦v n - b¦ < ε/2"
      using ‹0 < ε/2› assms(2) limite_def by blast
    then obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"
      by (rule exE)
    have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"
    proof (intro allI impI)
      fix n :: nat
      assume "n ≥ max Nu Nv"
      have "¦(u n + v n) - (a + b)¦ = ¦(u n - a) + (v n - b)¦"
        by simp
      also have "… ≤ ¦u n - a¦ + ¦v n - b¦"
        by simp
      also have "… < ε/2 + ε/2"
        using hNu hNv ‹max Nu Nv ≤ n› by fastforce
      finally show "¦(u n + v n) - (a + b)¦ < ε"
        by simp
    qed
    then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε "
      by (rule exI)
  qed
qed

(* 2ª demostración *)

lemma
  assumes "limite u a"
          "limite v b"
  shows   "limite (λ n. u n + v n) (a + b)"
proof (unfold limite_def)
  show "∀ε>0. ∃k. ∀n≥k. ¦(u n + v n) - (a + b)¦ < ε"
  proof (intro allI impI)
    fix ε :: real
    assume "0 < ε"
    then have "0 < ε/2" by simp
    obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"
      using ‹0 < ε/2› assms(1) limite_def by blast
    obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"
      using ‹0 < ε/2› assms(2) limite_def by blast
    have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"
      using hNu hNv
      by (smt (verit, ccfv_threshold) field_sum_of_halves max.boundedE)
    then show "∃k. ∀n≥k. ¦u n + v n - (a + b)¦ < ε "
      by blast
  qed
qed

end

theory Limite_de_la_suma_de_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¦ < ε)"

(* 1ª demostración *)

lemma

assumes "limite u a"

"limite v b"

shows "limite (λ n. u n + v n) (a + b)"

proof (unfold limite_def)

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

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2"

by simp

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

using assms(1) limite_def by blast

then obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"

by (rule exE)

then have "∃k. ∀n≥k. ¦v n - b¦ < ε/2"

using ‹0 < ε/2› assms(2) limite_def by blast

then obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"

by (rule exE)

have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"

proof (intro allI impI)

fix n :: nat

assume "n ≥ max Nu Nv"

have "¦(u n + v n) - (a + b)¦ = ¦(u n - a) + (v n - b)¦"

by simp

also have "… ≤ ¦u n - a¦ + ¦v n - b¦"

by simp

also have "… < ε/2 + ε/2"

using hNu hNv ‹max Nu Nv ≤ n› by fastforce

finally show "¦(u n + v n) - (a + b)¦ < ε"

by simp

qed

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

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "limite u a"

"limite v b"

shows "limite (λ n. u n + v n) (a + b)"

proof (unfold limite_def)

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

proof (intro allI impI)

fix ε :: real

assume "0 < ε"

then have "0 < ε/2" by simp

obtain Nu where hNu : "∀n≥Nu. ¦u n - a¦ < ε/2"

using ‹0 < ε/2› assms(1) limite_def by blast

obtain Nv where hNv : "∀n≥Nv. ¦v n - b¦ < ε/2"

using ‹0 < ε/2› assms(2) limite_def by blast

have "∀n≥max Nu Nv. ¦(u n + v n) - (a + b)¦ < ε"

using hNu hNv

by (smt (verit, ccfv_threshold) field_sum_of_halves max.boundedE)

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

by blast

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 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]