José A. Alonso

ForMatUS: Pruebas en Lean de “Las funciones de extracción no están acotadas”

PorJosé A. Alonso 9 enero 20219 enero 2021

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 11 pruebas en Lean de la propiedad

Las funciones de extracción no están acotadas; es decir, que si φ es una función de extracción, entonces

∀ N N’, ∃ n ≥ N’, φ n ≥ N

usando los estilos declarativo, aplicativo y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
open nat

variable {φ : ℕ → ℕ}

-- ----------------------------------------------------
-- Nota. Se usará la siguiente definición y lema
-- estudiado anteriormente.
-- ----------------------------------------------------

def extraccion : (ℕ → ℕ) → Prop
| φ := ∀ n m, n < m → φ n < φ m

lemma id_mne_extraccion
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intros n,
  induction n with m HI,
  { linarith },
  { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },
end

-- ----------------------------------------------------
-- Ejercicio. Demostrar que las funciones de extracción
-- no está acotadas; es decir, que si φ es una función
-- de extracción, entonces
--     ∀ N N', ∃ n ≥ N', φ n ≥ N
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
begin
  intros N N',
  let n := max N N',
  use n,
  split,
  { exact le_max_right N N', },
  { calc N ≤ n   : le_max_left N N'
       ... ≤ φ n : id_mne_extraccion h n, },
end

-- 2ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
begin
  intros N N',
  let n := max N N',
  use n,
  split,
  { exact le_max_right N N', },
  { exact le_trans (le_max_left N N')
                   (id_mne_extraccion h n), },
end

-- 3ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
begin
  intros N N',
  use max N N',
  split,
  { exact le_max_right N N', },
  { exact le_trans (le_max_left N N')
                   (id_mne_extraccion h (max N N')), },
end

-- 4ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
begin
  intros N N',
  use max N N',
  exact ⟨le_max_right N N',
         le_trans (le_max_left N N')
                  (id_mne_extraccion h (max N N'))⟩,
end

-- 5ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
λ N N',
  ⟨max N N', ⟨le_max_right N N',
              le_trans (le_max_left N N')
                       (id_mne_extraccion h (max N N'))⟩⟩

-- 6ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
assume N N',
let n := max N N' in
have h1 : n ≥ N',
  from le_max_right N N',
show ∃ n ≥ N', φ n ≥ N, from
exists.intro n
  (exists.intro h1
    (show φ n ≥ N, from
       calc N ≤ n   : le_max_left N N'
          ... ≤ φ n : id_mne_extraccion h n))

-- 7ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
assume N N',
let n := max N N' in
have h1 : n ≥ N',
  from le_max_right N N',
show ∃ n ≥ N', φ n ≥ N, from
⟨n, h1, calc N ≤ n   : le_max_left N N'
          ...  ≤ φ n : id_mne_extraccion h n⟩

-- 8ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
assume N N',
let n := max N N' in
have h1 : n ≥ N',
  from le_max_right N N',
show ∃ n ≥ N', φ n ≥ N, from
⟨n, h1, le_trans (le_max_left N N')
                 (id_mne_extraccion h (max N N'))⟩

-- 9ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
assume N N',
let n := max N N' in
have h1 : n ≥ N',
  from le_max_right N N',
⟨n, h1, le_trans (le_max_left N N')
                 (id_mne_extraccion h n)⟩

-- 10ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
assume N N',
⟨max N N', le_max_right N N',
           le_trans (le_max_left N N')
                    (id_mne_extraccion h (max N N'))⟩

-- 11ª demostración
example
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
λ N N',
  ⟨max N N', le_max_right N N',
             le_trans (le_max_left N N')
             (id_mne_extraccion h (max N N'))⟩

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

import data.real.basic

open nat

variable {φ : ℕ → ℕ}

-- ----------------------------------------------------

-- Nota. Se usará la siguiente definición y lema

-- estudiado anteriormente.

-- ----------------------------------------------------

def extraccion : (ℕ → ℕ) → Prop

| φ := ∀ n m, n < m → φ n < φ m

lemma id_mne_extraccion

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intros n,

induction n with m HI,

{ linarith },

{ exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },

end

-- ----------------------------------------------------

-- Ejercicio. Demostrar que las funciones de extracción

-- no está acotadas; es decir, que si φ es una función

-- de extracción, entonces

-- ∀ N N', ∃ n ≥ N', φ n ≥ N

-- ----------------------------------------------------

-- 1ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

begin

intros N N',

let n := max N N',

use n,

split,

{ exact le_max_right N N', },

{ calc N ≤ n : le_max_left N N'

... ≤ φ n : id_mne_extraccion h n, },

end

-- 2ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

begin

intros N N',

let n := max N N',

use n,

split,

{ exact le_max_right N N', },

{ exact le_trans (le_max_left N N')

(id_mne_extraccion h n), },

end

-- 3ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

begin

intros N N',

use max N N',

split,

{ exact le_max_right N N', },

{ exact le_trans (le_max_left N N')

(id_mne_extraccion h (max N N')), },

end

-- 4ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

begin

intros N N',

use max N N',

exact ⟨le_max_right N N',

le_trans (le_max_left N N')

(id_mne_extraccion h (max N N'))⟩,

end

-- 5ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

λ N N',

⟨max N N', ⟨le_max_right N N',

le_trans (le_max_left N N')

(id_mne_extraccion h (max N N'))⟩⟩

-- 6ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

assume N N',

let n := max N N' in

have h1 : n ≥ N',

from le_max_right N N',

show ∃ n ≥ N', φ n ≥ N, from

exists.intro n

(exists.intro h1

(show φ n ≥ N, from

calc N ≤ n : le_max_left N N'

... ≤ φ n : id_mne_extraccion h n))

-- 7ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

assume N N',

let n := max N N' in

have h1 : n ≥ N',

from le_max_right N N',

show ∃ n ≥ N', φ n ≥ N, from

⟨n, h1, calc N ≤ n : le_max_left N N'

... ≤ φ n : id_mne_extraccion h n⟩

-- 8ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

assume N N',

let n := max N N' in

have h1 : n ≥ N',

from le_max_right N N',

show ∃ n ≥ N', φ n ≥ N, from

⟨n, h1, le_trans (le_max_left N N')

(id_mne_extraccion h (max N N'))⟩

-- 9ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

assume N N',

let n := max N N' in

have h1 : n ≥ N',

from le_max_right N N',

⟨n, h1, le_trans (le_max_left N N')

(id_mne_extraccion h n)⟩

-- 10ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

assume N N',

⟨max N N', le_max_right N N',

le_trans (le_max_left N N')

(id_mne_extraccion h (max N N'))⟩

-- 11ª demostración

example

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

λ N N',

⟨max N N', le_max_right N N',

le_trans (le_max_left N N')

(id_mne_extraccion h (max N N'))⟩

ForMatUS: Pruebas en Lean de “La función identidad es menor o igual que la función de extracción”

PorJosé A. Alonso 8 enero 20218 enero 2021

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 5 pruebas en Lean de la propiedad

Si φ es una función de extracción (es decir, una función creciente de ℕ en ℕ), entonces n ≤ φ n (para todo n).

usando los estilos declarativo y aplicativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
open nat

variable {φ : ℕ → ℕ}

set_option pp.structure_projections false

-- ----------------------------------------------------
-- Ejercicio 1. Para extraer una sucesión se aplica una
-- función de extracción que conserva el orden; por
-- ejemplo, la subsucesión
--    uₒ, u₂, u₄, u₆, ...
-- se ha obtenido con la función de extracción φ tal
-- que φ(n) = 2*n.
--
-- Definir la función
--    extraccion : (ℕ → ℕ) → Prop
-- tal que (extraccion φ) expresa que φ es una función
-- de extracción
-- ----------------------------------------------------

def extraccion : (ℕ → ℕ) → Prop
| φ := ∀ n m, n < m → φ n < φ m

-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que si φ es una función de
-- extracción, entonces
--    ∀ n, n ≤ φ n
-- ----------------------------------------------------

-- 1ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    have h1 : m < succ m,
      from lt_add_one m,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (succ m) h1, },
end

-- 2ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le _ },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : by linarith [h m (m+1) (by linarith)] },
end

-- 3ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { linarith },
  { apply nat.succ_le_of_lt,
    linarith [h m (m+1) (by linarith)] },
end

-- 4ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { linarith },
  { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },
end

-- 5ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
assume h : extraccion φ,
assume n,
nat.rec_on n
  ( show 0 ≤ φ 0,
      from nat.zero_le (φ 0) )
  ( assume m,
    assume HI : m ≤ φ m,
    have h1 : m < succ m,
      from lt_add_one m,
    have h2 : m < φ (succ m), from
      calc m ≤ φ m        : HI
         ... < φ (succ m) : h m (succ m) h1,
    show succ m ≤ φ (succ m),
      from nat.succ_le_of_lt h2)

import data.real.basic

open nat

variable {φ : ℕ → ℕ}

set_option pp.structure_projections false

-- ----------------------------------------------------

-- Ejercicio 1. Para extraer una sucesión se aplica una

-- función de extracción que conserva el orden; por

-- ejemplo, la subsucesión

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

-- se ha obtenido con la función de extracción φ tal

-- que φ(n) = 2*n.

-- Definir la función

-- extraccion : (ℕ → ℕ) → Prop

-- tal que (extraccion φ) expresa que φ es una función

-- de extracción

-- ----------------------------------------------------

def extraccion : (ℕ → ℕ) → Prop

| φ := ∀ n m, n < m → φ n < φ m

-- ----------------------------------------------------

-- Ejercicio 2. Demostrar que si φ es una función de

-- extracción, entonces

-- ∀ n, n ≤ φ n

-- ----------------------------------------------------

-- 1ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

have h1 : m < succ m,

from lt_add_one m,

calc m ≤ φ m : HI

... < φ (succ m) : h m (succ m) h1, },

end

-- 2ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ exact nat.zero_le _ },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : by linarith [h m (m+1) (by linarith)] },

end

-- 3ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ linarith },

{ apply nat.succ_le_of_lt,

linarith [h m (m+1) (by linarith)] },

end

-- 4ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ linarith },

{ exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },

end

-- 5ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

assume h : extraccion φ,

assume n,

nat.rec_on n

( show 0 ≤ φ 0,

from nat.zero_le (φ 0) )

( assume m,

assume HI : m ≤ φ m,

have h1 : m < succ m,

from lt_add_one m,

have h2 : m < φ (succ m), from

calc m ≤ φ m : HI

... < φ (succ m) : h m (succ m) h1,

show succ m ≤ φ (succ m),

from nat.succ_le_of_lt h2)

ForMatUS: Pruebas en Lean de “Los supremos de las sucesiones no decrecientes son sus límites”

PorJosé A. Alonso 8 enero 20218 enero 2021

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad

Los supremos de las sucesiones no decrecientes son sus límites

usando los estilos declarativo y aplicativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

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

-- ----------------------------------------------------
-- Nota. Se usarán las siguientes notaciones y
-- definiciones estudiadas anteriormente:
-- + |x| = abs x
-- + limite u c :
--      ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε
-- ----------------------------------------------------

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

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

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    no_decreciente : (ℕ → ℝ) → Prop
-- tal que (no_decreciente) expresa que la sucesión u
-- es no decreciente.
-- ----------------------------------------------------

def no_decreciente : (ℕ → ℝ) → Prop
| u := ∀ n m, n ≤ m → u n ≤ u m

-- ----------------------------------------------------
-- Ejercicio 2. Definir la función
--    es_sup_suc : ℝ → (ℕ → ℝ) → Prop
-- tal que (es_sup_suc M u) expresa que M es el supremo
-- de la sucesión u.
-- ----------------------------------------------------

def es_sup_suc : ℝ → (ℕ → ℝ) → Prop
| M u := (∀ n, u n ≤ M) ∧ ∀ ε > 0, ∃ n₀, u n₀ ≥ M - ε

-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que si M es un supremo de la
-- sucesión no decreciente u, entonces el límite de u
-- es M.
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold es_sup_suc at h,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { -- unfold no_decreciente at h',
    specialize h' n₀ n hn,
    calc -ε
         = (M - ε) - M : by ring
     ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
     ... ≤ u n - M     : sub_le_sub_right h' 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
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  intros ε hε,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { linarith [h' n₀ n hn] },
  { linarith [hM₁ n] },
end

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

-- 4ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
assume ε,
assume hε : ε > 0,
have hM₁ : ∀ (n : ℕ), u n ≤ M,
  from h.left,
have hM₂ : ∀ (ε : ℝ), ε > 0 → (∃ (n₀ : ℕ), u n₀ ≥ M - ε),
  from h.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 h'a : u n₀ ≤ u n,
              from h' n₀ n hn,
            calc -ε
                 = (M - ε) - M : by ring
             ... ≤ u n₀ - M    : sub_le_sub_right hn₀ M
             ... ≤ u n - M     : sub_le_sub_right h'a M },
        have h3 : 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 h3) },
    show ∃ N, ∀ n, n ≥ N → |u n - M| ≤ ε,
      from exists.intro n₀ h1)

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

import data.real.basic

variable (u : ℕ → ℝ)

variable (M : ℝ)

-- ----------------------------------------------------

-- Nota. Se usarán las siguientes notaciones y

-- definiciones estudiadas anteriormente:

-- + |x| = abs x

-- + limite u c :

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

-- ----------------------------------------------------

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

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

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

-- ----------------------------------------------------

-- Ejercicio 1. Definir la función

-- no_decreciente : (ℕ → ℝ) → Prop

-- tal que (no_decreciente) expresa que la sucesión u

-- es no decreciente.

-- ----------------------------------------------------

def no_decreciente : (ℕ → ℝ) → Prop

| u := ∀ n m, n ≤ m → u n ≤ u m

-- ----------------------------------------------------

-- Ejercicio 2. Definir la función

-- es_sup_suc : ℝ → (ℕ → ℝ) → Prop

-- tal que (es_sup_suc M u) expresa que M es el supremo

-- de la sucesión u.

-- ----------------------------------------------------

def es_sup_suc : ℝ → (ℕ → ℝ) → Prop

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

-- ----------------------------------------------------

-- Ejercicio 3. Demostrar que si M es un supremo de la

-- sucesión no decreciente u, entonces el límite de u

-- es M.

-- ----------------------------------------------------

-- 1ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

begin

-- unfold limite,

intros ε hε,

-- unfold es_sup_suc at h,

cases h with hM₁ hM₂,

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

use n₀,

intros n hn,

rw abs_le,

split,

{ -- unfold no_decreciente at h',

specialize h' n₀ n hn,

calc -ε

= (M - ε) - M : by ring

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

... ≤ u n - M : sub_le_sub_right h' 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

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

begin

intros ε hε,

cases h with hM₁ hM₂,

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

use n₀,

intros n hn,

rw abs_le,

split,

{ linarith [h' n₀ n hn] },

{ linarith [hM₁ n] },

end

-- 3ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

begin

intros ε hε,

cases h with hM₁ hM₂,

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

use n₀,

intros n hn,

rw abs_le,

split ; linarith [h' n₀ n hn, hM₁ n],

end

-- 4ª demostración

example

(h : es_sup_suc M u)

(h' : no_decreciente u)

: limite u M :=

assume ε,

assume hε : ε > 0,

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

from h.left,

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

from h.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 h'a : u n₀ ≤ u n,

from h' n₀ n hn,

calc -ε

= (M - ε) - M : by ring

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

... ≤ u n - M : sub_le_sub_right h'a M },

have h3 : 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 h3) },

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

from exists.intro n₀ h1)

ForMatUS: Pruebas en Lean de la unicidad del límite de las sucesiones

PorJosé A. Alonso 5 enero 2021

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la unicidad del límite de las sucesiones.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variables (u : ℕ → ℝ)
variables (a b x y : ℝ)

-- ----------------------------------------------------
-- Nota. Se usarán las siguientes notaciones,
-- definiciones y lemas estudiados anteriormente:
-- + |x| = abs x
-- + limite u c :
--      ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε
-- + cero_de_abs_mn_todos:
--      (∀ ε > 0, |x| ≤ ε) → x = 0
-- + ig_de_abs_sub_mne_todos:
--      (∀ ε > 0, |x - y| ≤ ε) → x = y
-- ----------------------------------------------------

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

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

lemma cero_de_abs_mn_todos
  (h : ∀ ε > 0, |x| ≤ ε)
  : x = 0 :=
abs_eq_zero.mp
  (eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)

lemma ig_de_abs_sub_mne_todos
  (h : ∀ ε > 0, |x - y| ≤ ε)
  : x = y :=
sub_eq_zero.mp (cero_de_abs_mn_todos (x - y) h)

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

-- 1ª demostración
example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
begin
  apply ig_de_abs_sub_mne_todos,
  intros ε hε,
  cases ha (ε/2) (half_pos hε) with Na hNa,
  cases hb (ε/2) (half_pos hε) with Nb hNb,
  let N := max Na Nb,
  clear ha hb,
  specialize hNa N (le_max_left  _ _),
  specialize hNb N (le_max_right  _ _),
  calc |a - b|
       = |(a - u N) + (u N - b)| : by ring
   ... ≤ |a - u N| + |u N - b|   : by apply abs_add
   ... = |u N - a| + |u N - b|   : by rw abs_sub
   ... ≤ ε/2 + ε/2               : add_le_add hNa hNb
   ... = ε                       : add_halves ε
end

-- 2ª demostración
example
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
begin
  apply ig_de_abs_sub_mne_todos,
  intros ε hε,
  cases ha (ε/2) (by linarith) with Na hNa,
  cases hb (ε/2) (by linarith) with Nb hNb,
  let N := max Na Nb,
  clear ha hb,
  specialize hNa N (by finish),
  specialize hNb N (by finish),
  calc |a - b|
       = |(a - u N) + (u N - b)| : by ring
   ... ≤ |a - u N| + |u N - b|   : by apply abs_add
   ... = |u N - a| + |u N - b|   : by rw abs_sub
   ... ≤ ε                       : by linarith [hNa, hNb]
end

import data.real.basic

variables (u : ℕ → ℝ)

variables (a b x y : ℝ)

-- ----------------------------------------------------

-- Nota. Se usarán las siguientes notaciones,

-- definiciones y lemas estudiados anteriormente:

-- + |x| = abs x

-- + limite u c :

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

-- + cero_de_abs_mn_todos:

-- (∀ ε > 0, |x| ≤ ε) → x = 0

-- + ig_de_abs_sub_mne_todos:

-- (∀ ε > 0, |x - y| ≤ ε) → x = y

-- ----------------------------------------------------

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

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

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

lemma cero_de_abs_mn_todos

(h : ∀ ε > 0, |x| ≤ ε)

: x = 0 :=

abs_eq_zero.mp

(eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)

lemma ig_de_abs_sub_mne_todos

(h : ∀ ε > 0, |x - y| ≤ ε)

: x = y :=

sub_eq_zero.mp (cero_de_abs_mn_todos (x - y) h)

-- ----------------------------------------------------

-- Ejercicio. Demostrar que cada sucesión tiene como

-- máximo un límite.

-- ----------------------------------------------------

-- 1ª demostración

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

begin

apply ig_de_abs_sub_mne_todos,

intros ε hε,

cases ha (ε/2) (half_pos hε) with Na hNa,

cases hb (ε/2) (half_pos hε) with Nb hNb,

let N := max Na Nb,

clear ha hb,

specialize hNa N (le_max_left _ _),

specialize hNb N (le_max_right _ _),

calc |a - b|

= |(a - u N) + (u N - b)| : by ring

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

... = |u N - a| + |u N - b| : by rw abs_sub

... ≤ ε/2 + ε/2 : add_le_add hNa hNb

... = ε : add_halves ε

end

-- 2ª demostración

example

(ha : limite u a)

(hb : limite u b)

: a = b :=

begin

apply ig_de_abs_sub_mne_todos,

intros ε hε,

cases ha (ε/2) (by linarith) with Na hNa,

cases hb (ε/2) (by linarith) with Nb hNb,

let N := max Na Nb,

clear ha hb,

specialize hNa N (by finish),

specialize hNb N (by finish),

calc |a - b|

= |(a - u N) + (u N - b)| : by ring

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

... = |u N - a| + |u N - b| : by rw abs_sub

... ≤ ε : by linarith [hNa, hNb]

end

Pruebas en Lean de “Si |x – y| ≤ ε, para todo ε > 0, entonces x = y”

PorJosé A. Alonso 5 enero 20214 enero 2021

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad:

Si |x – y| ≤ ε, para todo ε > 0, entonces x = y

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variables (x y : ℝ)

-- ----------------------------------------------------
-- Ejercicio 1. Definir la notación |x| para el valor
-- absoluto de x.
-- ----------------------------------------------------

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

-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que si |x - y| ≤ ε, para todo
-- ε > 0, entonces x = y.
-- ----------------------------------------------------

-- Se usará el lema demostrado anteriormente
lemma cero_de_abs_mne_todos
  (h : ∀ ε > 0, |x| ≤ ε)
  : x = 0 :=
abs_eq_zero.mp
  (eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)

-- 1ª demostración
example
  (h : ∀ ε > 0, |x - y| ≤ ε)
  : x = y :=
begin
  rw ← sub_eq_zero,
  exact cero_de_abs_mne_todos (x - y) h,
end

-- 2ª demostración
lemma ig_de_abs_sub_mne_todos
  (h : ∀ ε > 0, |x - y| ≤ ε)
  : x = y :=
sub_eq_zero.mp (cero_de_abs_mne_todos (x - y) h)

import data.real.basic

variables (x y : ℝ)

-- ----------------------------------------------------

-- Ejercicio 1. Definir la notación |x| para el valor

-- absoluto de x.

-- ----------------------------------------------------

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

-- ----------------------------------------------------

-- Ejercicio 2. Demostrar que si |x - y| ≤ ε, para todo

-- ε > 0, entonces x = y.

-- ----------------------------------------------------

-- Se usará el lema demostrado anteriormente

lemma cero_de_abs_mne_todos

(h : ∀ ε > 0, |x| ≤ ε)

: x = 0 :=

abs_eq_zero.mp

(eq_of_le_of_forall_le_of_dense (abs_nonneg x) h)

-- 1ª demostración

example

(h : ∀ ε > 0, |x - y| ≤ ε)

: x = y :=

begin

rw ← sub_eq_zero,

exact cero_de_abs_mne_todos (x - y) h,

end

-- 2ª demostración

lemma ig_de_abs_sub_mne_todos

(h : ∀ ε > 0, |x - y| ≤ ε)

: x = y :=

sub_eq_zero.mp (cero_de_abs_mne_todos (x - y) h)