Análisis – Página 4

Las sucesiones acotadas por cero son nulas

PorJosé A. Alonso 31 julio 202129 julio 2021

Demostrar que las sucesiones acotadas por cero son nulas.

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

import data.real.basic
import tactic

variable (u : ℕ → ℝ)

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

example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
sorry

import data.real.basic

import tactic

variable (u : ℕ → ℝ)

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

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

variable (u : ℕ → ℝ)

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

-- 1ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  rw ← abs_eq_zero,
  specialize h n,
  apply le_antisymm,
  { exact h, },
  { exact abs_nonneg (u n), },
end

-- 2ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  rw ← abs_eq_zero,
  specialize h n,
  exact le_antisymm h (abs_nonneg (u n)),
end

-- 3ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  rw ← abs_eq_zero,
  exact le_antisymm (h n) (abs_nonneg (u n)),
end

-- 4ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
begin
  intro n,
  exact abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n))),
end

-- 5ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
λ n, abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n)))

-- 6ª demostración
example
  (h : ∀ n, |u n| ≤ 0)
  : ∀ n, u n = 0 :=
by finish

import data.real.basic

import tactic

variable (u : ℕ → ℝ)

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

-- 1ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

rw ← abs_eq_zero,

specialize h n,

apply le_antisymm,

{ exact h, },

{ exact abs_nonneg (u n), },

end

-- 2ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

rw ← abs_eq_zero,

specialize h n,

exact le_antisymm h (abs_nonneg (u n)),

end

-- 3ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

rw ← abs_eq_zero,

exact le_antisymm (h n) (abs_nonneg (u n)),

end

-- 4ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

begin

intro n,

exact abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n))),

end

-- 5ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

λ n, abs_eq_zero.mp (le_antisymm (h n) (abs_nonneg (u n)))

-- 6ª demostración

example

(h : ∀ n, |u n| ≤ 0)

: ∀ n, u n = 0 :=

by finish

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

(* 1ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
proof (rule allI)
  fix n
  have "¦a n¦ = 0"
  proof (rule antisym)
    show "¦a n¦ ≤ 0"
      using assms by (rule allE)
  next
    show " 0 ≤ ¦a n¦"
      by (rule abs_ge_zero)
  qed
  then show "a n = 0"
    by (simp only: abs_eq_0_iff)
qed

(* 2ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
proof (rule allI)
  fix n
  have "¦a n¦ = 0"
  proof (rule antisym)
    show "¦a n¦ ≤ 0" try
      using assms by (rule allE)
  next
    show " 0 ≤ ¦a n¦"
      by simp
  qed
  then show "a n = 0"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
proof (rule allI)
  fix n
  have "¦a n¦ = 0"
    using assms by auto
  then show "a n = 0"
    by simp
qed

(* 4ª demostración *)
lemma
  fixes a :: "nat ⇒ real"
  assumes "∀n. ¦a n¦ ≤ 0"
  shows   "∀n. a n = 0"
using assms by auto

end

theory Las_sucesiones_acotadas_por_cero_son_nulas

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

proof (rule allI)

fix n

have "¦a n¦ = 0"

proof (rule antisym)

show "¦a n¦ ≤ 0"

using assms by (rule allE)

show " 0 ≤ ¦a n¦"

by (rule abs_ge_zero)

qed

then show "a n = 0"

by (simp only: abs_eq_0_iff)

qed

(* 2ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

proof (rule allI)

fix n

have "¦a n¦ = 0"

proof (rule antisym)

show "¦a n¦ ≤ 0" try

using assms by (rule allE)

show " 0 ≤ ¦a n¦"

by simp

qed

then show "a n = 0"

by simp

qed

(* 3ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

proof (rule allI)

fix n

have "¦a n¦ = 0"

using assms by auto

then show "a n = 0"

by simp

qed

(* 4ª demostración *)

lemma

fixes a :: "nat ⇒ real"

assumes "∀n. ¦a n¦ ≤ 0"

shows "∀n. a n = 0"

using assms by auto

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 sucesión menor que otra sucesión

PorJosé A. Alonso 30 julio 202129 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 aₙ → l, bₙ → m y aₙ ≤ bₙ para todo n, entonces l ≤ m.

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 (u : ℕ → ℝ) (c : ℝ) :=
∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| < ε

example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
sorry

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

variables (a c : ℝ)

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

def limite (u : ℕ → ℝ) (c : ℝ) :=

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

example

(hu : limite u a)

(hv : limite v c)

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

: a ≤ c :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
import tactic

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

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

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

-- 1ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hεac,
  have hε : 0 < ε :=
    half_pos (sub_pos.mpr hlt),
  cases hu ε hε with Nu HNu,
  cases hv ε hε with Nv HNv,
  let N := max Nu Nv,
  have HNu' : Nu ≤ N := le_max_left Nu Nv,
  have HNv' : Nv ≤ N := le_max_right Nu Nv,
  have Ha : |u N - a| < ε := HNu N HNu',
  have Hc : |v N - c| < ε := HNv N HNv',
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  calc a - c
       = (a - u N) + (u N - c)   : by ring
   ... ≤ (a - u N) + (v N - c)   : by simp [HN]
   ... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))
   ... ≤ |a - u N| + |v N - c|   : abs_add (a - u N) (v N - c)
   ... = |u N - a| + |v N - c|   : by simp only [abs_sub]
   ... < ε + ε                   : add_lt_add Ha Hc
   ... = a - c                   : add_halves (a - c),
end

-- 2ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hε,
  cases hu ε (by linarith) with Nu HNu,
  cases hv ε (by linarith) with Nv HNv,
  let N := max Nu Nv,
  have Ha : |u N - a| < ε :=
    HNu N (le_max_left Nu Nv),
  have Hc : |v N - c| < ε :=
    HNv N (le_max_right Nu Nv),
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  calc a - c
       = (a - u N) + (u N - c)   : by ring
   ... ≤ (a - u N) + (v N - c)   : by simp [HN]
   ... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))
   ... ≤ |a - u N| + |v N - c|   : abs_add (a - u N) (v N - c)
   ... = |u N - a| + |v N - c|   : by simp only [abs_sub]
   ... < ε + ε                   : add_lt_add Ha Hc
   ... = a - c                   : add_halves (a - c),
end

-- 3ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hε,
  cases hu ε (by linarith) with Nu HNu,
  cases hv ε (by linarith) with Nv HNv,
  let N := max Nu Nv,
  have Ha : |u N - a| < ε :=
    HNu N (le_max_left Nu Nv),
  have Hc : |v N - c| < ε :=
    HNv N (le_max_right Nu Nv),
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  calc a - c
       = (a - u N) + (u N - c)   : by ring
   ... ≤ (a - u N) + (v N - c)   : by simp [HN]
   ... ≤ |(a - u N) + (v N - c)| : by simp [le_abs_self]
   ... ≤ |a - u N| + |v N - c|   : by simp [abs_add]
   ... = |u N - a| + |v N - c|   : by simp [abs_sub]
   ... < ε + ε                   : add_lt_add Ha Hc
   ... = a - c                   : by simp,
end

-- 4ª demostración
example
  (hu : limite u a)
  (hv : limite v c)
  (hle : ∀ n, u n ≤ v n)
  : a ≤ c :=
begin
  apply le_of_not_lt,
  intro hlt,
  set ε := (a - c) /2 with hε,
  cases hu ε (by linarith) with Nu HNu,
  cases hv ε (by linarith) with Nv HNv,
  let N := max Nu Nv,
  have Ha : |u N - a| < ε :=
    HNu N (le_max_left Nu Nv),
  have Hc : |v N - c| < ε :=
    HNv N (le_max_right Nu Nv),
  have HN : u N ≤ v N := hle N,
  apply lt_irrefl (a - c),
  rw abs_lt at Ha Hc,
  linarith,
end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

import data.real.basic

import tactic

variables (u v : ℕ → ℝ)

variables (a c : ℝ)

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

def limite (u : ℕ → ℝ) (c : ℝ) :=

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

-- 1ª demostración

example

(hu : limite u a)

(hv : limite v c)

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

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hεac,

have hε : 0 < ε :=

half_pos (sub_pos.mpr hlt),

cases hu ε hε with Nu HNu,

cases hv ε hε with Nv HNv,

let N := max Nu Nv,

have HNu' : Nu ≤ N := le_max_left Nu Nv,

have HNv' : Nv ≤ N := le_max_right Nu Nv,

have Ha : |u N - a| < ε := HNu N HNu',

have Hc : |v N - c| < ε := HNv N HNv',

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

calc a - c

= (a - u N) + (u N - c) : by ring

... ≤ (a - u N) + (v N - c) : by simp [HN]

... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))

... ≤ |a - u N| + |v N - c| : abs_add (a - u N) (v N - c)

... = |u N - a| + |v N - c| : by simp only [abs_sub]

... < ε + ε : add_lt_add Ha Hc

... = a - c : add_halves (a - c),

end

-- 2ª demostración

example

(hu : limite u a)

(hv : limite v c)

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

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hε,

cases hu ε (by linarith) with Nu HNu,

cases hv ε (by linarith) with Nv HNv,

let N := max Nu Nv,

have Ha : |u N - a| < ε :=

HNu N (le_max_left Nu Nv),

have Hc : |v N - c| < ε :=

HNv N (le_max_right Nu Nv),

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

calc a - c

= (a - u N) + (u N - c) : by ring

... ≤ (a - u N) + (v N - c) : by simp [HN]

... ≤ |(a - u N) + (v N - c)| : le_abs_self ((a - u N) + (v N - c))

... ≤ |a - u N| + |v N - c| : abs_add (a - u N) (v N - c)

... = |u N - a| + |v N - c| : by simp only [abs_sub]

... < ε + ε : add_lt_add Ha Hc

... = a - c : add_halves (a - c),

end

-- 3ª demostración

example

(hu : limite u a)

(hv : limite v c)

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

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hε,

cases hu ε (by linarith) with Nu HNu,

cases hv ε (by linarith) with Nv HNv,

let N := max Nu Nv,

have Ha : |u N - a| < ε :=

HNu N (le_max_left Nu Nv),

have Hc : |v N - c| < ε :=

HNv N (le_max_right Nu Nv),

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

calc a - c

= (a - u N) + (u N - c) : by ring

... ≤ (a - u N) + (v N - c) : by simp [HN]

... ≤ |(a - u N) + (v N - c)| : by simp [le_abs_self]

... ≤ |a - u N| + |v N - c| : by simp [abs_add]

... = |u N - a| + |v N - c| : by simp [abs_sub]

... < ε + ε : add_lt_add Ha Hc

... = a - c : by simp,

end

-- 4ª demostración

example

(hu : limite u a)

(hv : limite v c)

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

: a ≤ c :=

begin

apply le_of_not_lt,

intro hlt,

set ε := (a - c) /2 with hε,

cases hu ε (by linarith) with Nu HNu,

cases hv ε (by linarith) with Nv HNv,

let N := max Nu Nv,

have Ha : |u N - a| < ε :=

HNu N (le_max_left Nu Nv),

have Hc : |v N - c| < ε :=

HNv N (le_max_right Nu Nv),

have HN : u N ≤ v N := hle N,

apply lt_irrefl (a - c),

rw abs_lt at Ha Hc,

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 Limite_de_sucesion_menor_que_otra_sucesion
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 c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  have "a - c < a - c"
  proof -
    have "a - c = (a - u ?N) + (u ?N - c)"
      by simp
    also have "… ≤ (a - u ?N) + (v ?N - c)"
      using assms(3) by auto
    also have "… ≤ ¦(a - u ?N) + (v ?N - c)¦"
      by (rule abs_ge_self)
    also have "… ≤ ¦a - u ?N¦ + ¦v ?N - c¦"
      by (rule abs_triangle_ineq)
    also have "… = ¦u ?N - a¦ + ¦v ?N - c¦"
      by (simp only: abs_minus_commute)
    also have "… < ?ε + ?ε"
      using Ha Hc by (simp only: add_strict_mono)
    also have "… = a - c"
      by (rule field_sum_of_halves)
    finally show "a - c < a - c"
      by this
  qed
  have "¬ a - c < a - c"
    by (rule less_irrefl)
  then show False
    using ‹a - c < a - c› by (rule notE)
qed

(* 2ª demostración *)
lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"
    by argo
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"
    by argo
  have "a - c < a - c"
    using assms(3) Ha' Hc'
    by (smt (verit, best) field_sum_of_halves)
  have "¬ a - c < a - c"
    by simp
  then show False
    using ‹a - c < a - c› by simp
qed

(* 3ª demostración *)
lemma
  assumes "limite u a"
          "limite v c"
          "∀n. u n ≤ v n"
  shows   "a ≤ c"
proof (rule leI ; intro notI)
  assume "c < a"
  let ?ε = "(a - c) /2"
  have "0 < ?ε"
    using ‹c < a› by simp
  obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"
    using assms(1) limite_def ‹0 < ?ε› by blast
  obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"
    using assms(2) limite_def ‹0 < ?ε› by blast
  let ?N = "max Nu Nv"
  have "?N ≥ Nu"
    by simp
  then have Ha : "¦u ?N - a¦ < ?ε"
    using HNu by simp
  then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"
    by argo
  have "?N ≥ Nv"
    by simp
  then have Hc : "¦v ?N - c¦ < ?ε"
    using HNv by simp
  then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"
    by argo
  show False
    using assms(3) Ha' Hc'
    by (smt (verit, best) field_sum_of_halves)
qed

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

theory Limite_de_sucesion_menor_que_otra_sucesion

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 c"

"∀n. u n ≤ v n"

shows "a ≤ c"

proof (rule leI ; intro notI)

assume "c < a"

let ?ε = "(a - c) /2"

have "0 < ?ε"

using ‹c < a› by simp

obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"

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

obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"

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

let ?N = "max Nu Nv"

have "?N ≥ Nu"

by simp

then have Ha : "¦u ?N - a¦ < ?ε"

using HNu by simp

have "?N ≥ Nv"

by simp

then have Hc : "¦v ?N - c¦ < ?ε"

using HNv by simp

have "a - c < a - c"

proof -

have "a - c = (a - u ?N) + (u ?N - c)"

by simp

also have "… ≤ (a - u ?N) + (v ?N - c)"

using assms(3) by auto

also have "… ≤ ¦(a - u ?N) + (v ?N - c)¦"

by (rule abs_ge_self)

also have "… ≤ ¦a - u ?N¦ + ¦v ?N - c¦"

by (rule abs_triangle_ineq)

also have "… = ¦u ?N - a¦ + ¦v ?N - c¦"

by (simp only: abs_minus_commute)

also have "… < ?ε + ?ε"

using Ha Hc by (simp only: add_strict_mono)

also have "… = a - c"

by (rule field_sum_of_halves)

finally show "a - c < a - c"

by this

qed

have "¬ a - c < a - c"

by (rule less_irrefl)

then show False

using ‹a - c < a - c› by (rule notE)

qed

(* 2ª demostración *)

lemma

assumes "limite u a"

"limite v c"

"∀n. u n ≤ v n"

shows "a ≤ c"

proof (rule leI ; intro notI)

assume "c < a"

let ?ε = "(a - c) /2"

have "0 < ?ε"

using ‹c < a› by simp

obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"

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

obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"

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

let ?N = "max Nu Nv"

have "?N ≥ Nu"

by simp

then have Ha : "¦u ?N - a¦ < ?ε"

using HNu by simp

then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"

by argo

have "?N ≥ Nv"

by simp

then have Hc : "¦v ?N - c¦ < ?ε"

using HNv by simp

then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"

by argo

have "a - c < a - c"

using assms(3) Ha' Hc'

by (smt (verit, best) field_sum_of_halves)

have "¬ a - c < a - c"

by simp

then show False

using ‹a - c < a - c› by simp

qed

(* 3ª demostración *)

lemma

assumes "limite u a"

"limite v c"

"∀n. u n ≤ v n"

shows "a ≤ c"

proof (rule leI ; intro notI)

assume "c < a"

let ?ε = "(a - c) /2"

have "0 < ?ε"

using ‹c < a› by simp

obtain Nu where HNu : "∀n≥Nu. ¦u n - a¦ < ?ε"

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

obtain Nv where HNv : "∀n≥Nv. ¦v n - c¦ < ?ε"

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

let ?N = "max Nu Nv"

have "?N ≥ Nu"

by simp

then have Ha : "¦u ?N - a¦ < ?ε"

using HNu by simp

then have Ha' : "u ?N - a < ?ε ∧ -(u ?N - a) < ?ε"

by argo

have "?N ≥ Nv"

by simp

then have Hc : "¦v ?N - c¦ < ?ε"

using HNv by simp

then have Hc' : "v ?N - c < ?ε ∧ -(v ?N - c) < ?ε"

by argo

show False

using assms(3) Ha' Hc'

by (smt (verit, best) field_sum_of_halves)

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]

Las sucesiones convergentes están acotadas

PorJosé A. Alonso 25 julio 202124 julio 2021

Demostrar que si u es una sucesión convergente, entonces está acotada; es decir,

    ∃ k b, ∀ n, n ≥ k → |u n| ≤ b

1	∃ k b, ∀ n, n ≥ k → \|u n\| ≤ b

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

import data.real.basic

variable {u : ℕ → ℝ}
variable {a : ℝ}

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

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
sorry

import data.real.basic

variable {u : ℕ → ℝ}

variable {a : ℝ}

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

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

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

-- (convergente u) expresa que u es convergente.

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable {u : ℕ → ℝ}
variable {a : ℝ}

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

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - c| ≤ ε

-- (convergente u) expresa que u es convergente.
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

-- 1ª demostración
example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
begin
  cases h with a ua,
  cases ua 1 zero_lt_one with k h,
  use [k, 1 + |a|],
  intros n hn,
  specialize h n hn,
  calc |u n|
       = |u n - a + a|   : congr_arg abs (eq_add_of_sub_eq rfl)
   ... ≤ |u n - a| + |a| : abs_add (u n - a) a
   ... ≤ 1 + |a|         : add_le_add_right h _
end

-- 2ª demostración
example
  (h : convergente u)
  : ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=
begin
  cases h with a ua,
  cases ua 1 zero_lt_one with k h,
  use [k, 1 + |a|],
  intros n hn,
  specialize h n hn,
  calc |u n|
       = |u n - a + a|   : by ring_nf
   ... ≤ |u n - a| + |a| : abs_add (u n - a) a
   ... ≤ 1 + |a|         : by linarith,
end

import data.real.basic

variable {u : ℕ → ℝ}

variable {a : ℝ}

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

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

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

-- (convergente u) expresa que u es convergente.

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

-- 1ª demostración

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

begin

cases h with a ua,

cases ua 1 zero_lt_one with k h,

use [k, 1 + |a|],

intros n hn,

specialize h n hn,

calc |u n|

= |u n - a + a| : congr_arg abs (eq_add_of_sub_eq rfl)

... ≤ |u n - a| + |a| : abs_add (u n - a) a

... ≤ 1 + |a| : add_le_add_right h _

end

-- 2ª demostración

example

(h : convergente u)

: ∃ k b, ∀ n, n ≥ k → |u n| ≤ b :=

begin

cases h with a ua,

cases ua 1 zero_lt_one with k h,

use [k, 1 + |a|],

intros n hn,

specialize h n hn,

calc |u n|

= |u n - a + a| : by ring_nf

... ≤ |u n - a| + |a| : abs_add (u n - a) a

... ≤ 1 + |a| : by 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 Acotacion_de_convergentes
imports Main HOL.Real
begin

(* (limite u c) expresa que el límite de u es c. *)
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (convergente u) expresa que u es convergente. *)
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"

(* 1ª demostración *)
lemma
  assumes "convergente u"
  shows   "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
proof -
  obtain a where "limite u a"
    using assms convergente_def by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"
    using limite_def zero_less_one by blast
  have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"
  proof (intro allI impI)
    fix n
    assume hn : "n ≥ k"
    have "¦u n¦ = ¦u n - a + a¦"    by simp
    also have "… ≤ ¦u n - a¦ + ¦a¦" by simp
    also have "… ≤ 1 + ¦a¦"         by (simp add: hk hn)
    finally show "¦u n¦ ≤ 1 + ¦a¦"  .
  qed
  then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
    by (intro exI)
qed

(* 2ª demostración *)
lemma
  assumes "convergente u"
  shows   "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
proof -
  obtain a where "limite u a"
    using assms convergente_def 
    by blast
  then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"
    using limite_def zero_less_one 
    by blast
  have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"
    using hk 
    by fastforce
  then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"
    by auto
qed

end

theory Acotacion_de_convergentes

imports Main HOL.Real

begin

(* (limite u c) expresa que el límite de u es c. *)

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

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (convergente u) expresa que u es convergente. *)

definition convergente :: "(nat ⇒ real) ⇒ bool" where

"convergente u ⟷ (∃ a. limite u a)"

(* 1ª demostración *)

lemma

assumes "convergente u"

shows "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

proof -

obtain a where "limite u a"

using assms convergente_def by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"

using limite_def zero_less_one by blast

have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"

proof (intro allI impI)

fix n

assume hn : "n ≥ k"

have "¦u n¦ = ¦u n - a + a¦" by simp

also have "… ≤ ¦u n - a¦ + ¦a¦" by simp

also have "… ≤ 1 + ¦a¦" by (simp add: hk hn)

finally show "¦u n¦ ≤ 1 + ¦a¦" .

qed

then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

by (intro exI)

qed

(* 2ª demostración *)

lemma

assumes "convergente u"

shows "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

proof -

obtain a where "limite u a"

using assms convergente_def

by blast

then obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ 1"

using limite_def zero_less_one

by blast

have "∀n≥k. ¦u n¦ ≤ 1 + ¦a¦"

using hk

by fastforce

then show "∃ k b. ∀n≥k. ¦u n¦ ≤ b"

by auto

qed

end

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

Los supremos de las sucesiones crecientes son sus límites

PorJosé A. Alonso 23 julio 202121 julio 2021

Demostrar que si M es un supremo de una sucesión creciente u, entonces el límite de u es M.

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

import data.real.basic

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

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

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- (supremo u M) expresa que el supremo de u es M.
def supremo (u : ℕ → ℝ) (M : ℝ) :=
  (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variable (M : ℝ)

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

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

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

-- (supremo u M) expresa que el supremo de u es M.

def supremo (u : ℕ → ℝ) (M : ℝ) :=

(∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

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

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

-- (limite u c) expresa que el límite de u es c.
def limite (u : ℕ → ℝ) (c : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- (supremo u M) expresa que el supremo de u es M.
def supremo (u : ℕ → ℝ) (M : ℝ) :=
  (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- 1ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold supremo at h,
  cases hM with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { -- unfold monotone at h',
    specialize hu hn,
    calc -ε
         = (M - ε) - M : by ring
     ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
     ... ≤ u n - M     : sub_le_sub_right hu M },
  { calc u n - M
         ≤ M - M       : sub_le_sub_right (hM₁ n) M
     ... = 0           : sub_self M
     ... ≤ ε           : le_of_lt hε, },
end

-- 2ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
begin
  intros ε hε,
  cases hM with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { linarith [hu hn] },
  { linarith [hM₁ n] },
end

-- 3ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
begin
  intros ε hε,
  cases hM with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split ; linarith [hu hn, hM₁ n],
end

-- 4ª demostración
example
  (hu : monotone u)
  (hM : supremo u M)
  : limite u M :=
assume ε,
assume hε : ε > 0,
have hM₁ : ∀ (n : ℕ), u n ≤ M,
  from hM.left,
have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),
  from hM.right,
exists.elim (hM₂ ε hε)
  ( assume n₀,
    assume hn₀ : u n₀ ≥ M - ε,
    have h1 : ∀ n, n ≥ n₀ → |u n - M| ≤ ε,
      { assume n,
        assume hn : n ≥ n₀,
        have h2 : -ε ≤ u n - M,
          { have h3 : u n₀ ≤ u n,
              from hu hn,
            calc -ε
                 = (M - ε) - M : by ring
             ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
             ... ≤ u n - M     : sub_le_sub_right h3 M },
        have h4 : u n - M ≤ ε,
          { calc u n - M
                 ≤ M - M       : sub_le_sub_right (hM₁ n) M
             ... = 0           : sub_self M
             ... ≤ ε           : le_of_lt hε },
        show |u n - M| ≤ ε,
          from abs_le.mpr (and.intro h2 h4) },
    show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,
      from exists.intro n₀ h1)

100

101

102

103

104

105

106

107

import data.real.basic

variable (u : ℕ → ℝ)

variable (M : ℝ)

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

-- (limite u c) expresa que el límite de u es c.

def limite (u : ℕ → ℝ) (c : ℝ) :=

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

-- (supremo u M) expresa que el supremo de u es M.

def supremo (u : ℕ → ℝ) (M : ℝ) :=

(∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- 1ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

begin

-- unfold limite,

intros ε hε,

-- unfold supremo at h,

cases hM with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split,

{ -- unfold monotone at h',

specialize hu hn,

calc -ε

= (M - ε) - M : by ring

... ≤ u n₀ - M : sub_le_sub_right hn₀ M

... ≤ u n - M : sub_le_sub_right hu M },

{ calc u n - M

≤ M - M : sub_le_sub_right (hM₁ n) M

... = 0 : sub_self M

... ≤ ε : le_of_lt hε, },

end

-- 2ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

begin

intros ε hε,

cases hM with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split,

{ linarith [hu hn] },

{ linarith [hM₁ n] },

end

-- 3ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

begin

intros ε hε,

cases hM with hM₁ hM₂,

cases hM₂ ε hε with n₀ hn₀,

use n₀,

intros n hn,

rw abs_le,

split ; linarith [hu hn, hM₁ n],

end

-- 4ª demostración

example

(hu : monotone u)

(hM : supremo u M)

: limite u M :=

assume ε,

assume hε : ε > 0,

have hM₁ : ∀ (n : ℕ), u n ≤ M,

from hM.left,

have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),

from hM.right,

exists.elim (hM₂ ε hε)

( assume n₀,

assume hn₀ : u n₀ ≥ M - ε,

have h1 : ∀ n, n ≥ n₀ → |u n - M| ≤ ε,

{ assume n,

assume hn : n ≥ n₀,

have h2 : -ε ≤ u n - M,

{ have h3 : u n₀ ≤ u n,

from hu hn,

calc -ε

= (M - ε) - M : by ring

... ≤ u n₀ - M : sub_le_sub_right hn₀ M

... ≤ u n - M : sub_le_sub_right h3 M },

have h4 : u n - M ≤ ε,

{ calc u n - M

≤ M - M : sub_le_sub_right (hM₁ n) M

... = 0 : sub_self M

... ≤ ε : le_of_lt hε },

show |u n - M| ≤ ε,

from abs_le.mpr (and.intro h2 h4) },

show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,

from exists.intro n₀ h1)

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

(* (limite u c) expresa que el límite de u es c. *)
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where 
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (supremo u M) expresa que el supremo de u es M. *)
definition supremo :: "(nat ⇒ real) ⇒ real ⇒ bool" where    
  "supremo u M ⟷ ((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

(* 1ª demostración *)
lemma
  assumes "mono u"
          "supremo u M"
  shows   "limite u M"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"
    using assms(2) 
    by (simp add: supremo_def)
  then have "∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε"
    by (rule conjunct2)
  then have "∃k. ∀n≥k. u n ≥ M - ε"
    by (simp only: ‹0 < ε›) 
  then obtain n0 where "∀n≥n0. u n ≥ M - ε"
    by (rule exE)
  have "∀n≥n0. ¦u n - M¦ ≤ ε" 
  proof (intro allI impI)
    fix n
    assume "n ≥ n0"
    show "¦u n - M¦ ≤ ε" 
    proof (rule abs_leI)
      have "∀n. u n ≤ M"
        using hM by (rule conjunct1)
      then have "u n - M ≤ M - M" 
        by simp
      also have "… = 0" 
        by (simp only: diff_self)
      also have "… ≤ ε" 
        using ‹0 < ε› by (simp only: less_imp_le)
      finally show "u n - M ≤ ε" 
        by this
    next
      have "-ε = (M - ε) - M" 
        by simp
      also have "… ≤ u n - M" 
        using ‹∀n≥n0. M - ε ≤ u n› ‹n0 ≤ n› by auto
      finally have "-ε ≤ u n - M"
        by this
      then show "- (u n - M) ≤ ε" 
        by simp
    qed
  qed
  then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"
    by (rule exI)
qed

(* 2ª demostración *)
lemma
  assumes "mono u"
          "supremo u M"
  shows   "limite u M"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"
    using assms(2) 
    by (simp add: supremo_def)
  then have "∃k. ∀n≥k. u n ≥ M - ε"
    using ‹0 < ε› by presburger
  then obtain n0 where "∀n≥n0. u n ≥ M - ε" 
    by (rule exE)
  then have "∀n≥n0. ¦u n - M¦ ≤ ε" 
    using hM by auto
  then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"
    by (rule exI)
qed

end

theory Los_supremos_de_las_sucesiones_crecientes_son_sus_limites

imports Main HOL.Real

begin

(* (limite u c) expresa que el límite de u es c. *)

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

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

(* (supremo u M) expresa que el supremo de u es M. *)

definition supremo :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"supremo u M ⟷ ((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

(* 1ª demostración *)

lemma

assumes "mono u"

"supremo u M"

shows "limite u M"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

using assms(2)

by (simp add: supremo_def)

then have "∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε"

by (rule conjunct2)

then have "∃k. ∀n≥k. u n ≥ M - ε"

by (simp only: ‹0 < ε›)

then obtain n0 where "∀n≥n0. u n ≥ M - ε"

by (rule exE)

have "∀n≥n0. ¦u n - M¦ ≤ ε"

proof (intro allI impI)

fix n

assume "n ≥ n0"

show "¦u n - M¦ ≤ ε"

proof (rule abs_leI)

have "∀n. u n ≤ M"

using hM by (rule conjunct1)

then have "u n - M ≤ M - M"

by simp

also have "… = 0"

by (simp only: diff_self)

also have "… ≤ ε"

using ‹0 < ε› by (simp only: less_imp_le)

finally show "u n - M ≤ ε"

by this

have "-ε = (M - ε) - M"

by simp

also have "… ≤ u n - M"

using ‹∀n≥n0. M - ε ≤ u n› ‹n0 ≤ n› by auto

finally have "-ε ≤ u n - M"

by this

then show "- (u n - M) ≤ ε"

by simp

qed

then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"

by (rule exI)

qed

(* 2ª demostración *)

lemma

assumes "mono u"

"supremo u M"

shows "limite u M"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

have hM : "((∀n. u n ≤ M) ∧ (∀ε>0. ∃k. ∀n≥k. u n ≥ M - ε))"

using assms(2)

by (simp add: supremo_def)

then have "∃k. ∀n≥k. u n ≥ M - ε"

using ‹0 < ε› by presburger

then obtain n0 where "∀n≥n0. u n ≥ M - ε"

by (rule exE)

then have "∀n≥n0. ¦u n - M¦ ≤ ε"

using hM by auto

then show "∃k. ∀n≥k. ¦u n - M¦ ≤ ε"

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]

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]