Vestigium

ForMatUS: Pruebas en Lean de “El punto de acumulación de las convergentes es su límite”

PorJosé A. Alonso 13 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

Si a es un punto de acumulación de una sucesión convergente u, entonces a es el límite de u.

usando los estilos declarativo, aplicativos y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variable  {u : ℕ → ℝ}
variables {a b: ℝ}
variables (x y : ℝ)
variable  {φ : ℕ → ℕ}

-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------

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)

lemma unicidad_limite
  (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,
  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

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

def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop
| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

lemma limite_subsucesion
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
assume ε,
assume hε : ε > 0,
exists.elim (h ε hε)
 ( assume N,
   assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε,
   have h1 : ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,
     { assume n,
       assume hn : n ≥ N,
       have h2 : N ≤ φ n, from
         calc N ≤ n   : hn
           ... ≤ φ n : id_mne_extraccion hφ n,
       show |(u ∘ φ) n - a| ≤ ε,
         from hN (φ n) h2,
     },
   show ∃ N, ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,
     from exists.intro N h1)

-- ----------------------------------------------------
-- Ejercicio. Demostrar que si a es un punto de
-- acumulación de una sucesión de límite b, entonces a
-- y b son iguales.
-- ----------------------------------------------------

-- 1ª demostración
example
  (ha : punto_acumulacion u a)
  (hb : limite u b)
  : a = b :=
begin
  -- unfold punto_acumulacion at ha,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  have hφ₃ : limite (u ∘ φ) b,
    from limite_subsucesion hb hφ₁,
  exact unicidad_limite hφ₂ hφ₃,
end

-- 2ª demostración
example
  (ha : punto_acumulacion u a)
  (hb : limite u b)
  : a = b :=
begin
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁),
end

-- 3ª demostración
example
  (ha : punto_acumulacion u a)
  (hb : limite u b)
  : a = b :=
exists.elim ha
  (λ φ hφ, unicidad_limite hφ.2 (limite_subsucesion hb hφ.1))

-- 4ª demostración
example
  (ha : punto_acumulacion u a)
  (hb : limite u b)
  : a = b :=
exists.elim ha
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    have hφ' : limite (u ∘ φ) b,
      from limite_subsucesion hb hφ.1,
    show a = b,
      from unicidad_limite hφ.2 hφ')

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

import data.real.basic

variable {u : ℕ → ℝ}

variables {a b: ℝ}

variables (x y : ℝ)

variable {φ : ℕ → ℕ}

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

-- Nota. Usaremos los siguientes conceptos estudiados

-- anteriormente.

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

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)

lemma unicidad_limite

(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,

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

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

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

| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

lemma limite_subsucesion

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

assume ε,

assume hε : ε > 0,

exists.elim (h ε hε)

( assume N,

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

have h1 : ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,

{ assume n,

assume hn : n ≥ N,

have h2 : N ≤ φ n, from

calc N ≤ n : hn

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

show |(u ∘ φ) n - a| ≤ ε,

from hN (φ n) h2,

show ∃ N, ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,

from exists.intro N h1)

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

-- Ejercicio. Demostrar que si a es un punto de

-- acumulación de una sucesión de límite b, entonces a

-- y b son iguales.

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

-- 1ª demostración

example

(ha : punto_acumulacion u a)

(hb : limite u b)

: a = b :=

begin

-- unfold punto_acumulacion at ha,

rcases ha with ⟨φ, hφ₁, hφ₂⟩,

have hφ₃ : limite (u ∘ φ) b,

from limite_subsucesion hb hφ₁,

exact unicidad_limite hφ₂ hφ₃,

end

-- 2ª demostración

example

(ha : punto_acumulacion u a)

(hb : limite u b)

: a = b :=

begin

rcases ha with ⟨φ, hφ₁, hφ₂⟩,

exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁),

end

-- 3ª demostración

example

(ha : punto_acumulacion u a)

(hb : limite u b)

: a = b :=

exists.elim ha

(λ φ hφ, unicidad_limite hφ.2 (limite_subsucesion hb hφ.1))

-- 4ª demostración

example

(ha : punto_acumulacion u a)

(hb : limite u b)

: a = b :=

exists.elim ha

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

have hφ' : limite (u ∘ φ) b,

from limite_subsucesion hb hφ.1,

show a = b,

from unicidad_limite hφ.2 hφ')

ForMatUS: Pruebas en Lean de “Las subsucesiones tienen el mismo límite que la sucesión”

PorJosé A. Alonso 12 enero 202112 enero 2021

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

Las subsucesiones de las sucesiones convergentes tienen el mismo límite que la sucesión.

usando los estilos aplicativo, funcional y declarativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

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

-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------

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

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

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

lemma extraccion_mye
  (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'))⟩

-- ----------------------------------------------------
-- Ejercicio. Demostrar que las subsucesiones de las
-- sucesiones convergentes tienen el mismo límite que
-- la sucesión.
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold limite at h,
  cases h ε hε with N hN,
  use N,
  intros n hn,
  apply hN,
  apply le_trans hn,
  exact id_mne_extraccion hφ n,
end

-- 2ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros n hn,
  apply hN,
  exact le_trans hn (id_mne_extraccion hφ n),
end

-- 3ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros n hn,
  exact hN (φ n) (le_trans hn (id_mne_extraccion hφ n)),
end

-- 4ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  exact λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n)),
end

-- 5ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  -- unfold limite at h,
  cases h ε hε with N hN,
  exact ⟨N, λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩,
end

-- 6ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  exact (exists.elim (h ε hε)
          (λ N hN,
            ⟨N, λ n hn,
                  hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩)),
end

-- 7ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
λ ε hε,
  (exists.elim (h ε hε)
    (λ N hN,
       ⟨N, λ n hn,
             hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩))

-- 8ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  unfold limite at h,
  cases h ε hε with N hN,
  use N,
  intros n hn,
  apply hN,
  calc N ≤ n   : hn
     ... ≤ φ n : id_mne_extraccion hφ n,
end

-- 9ª demostración
example
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
assume ε,
assume hε : ε > 0,
exists.elim (h ε hε)
 ( assume N,
   assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε,
   have h1 : ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,
     { assume n,
       assume hn : n ≥ N,
       have h2 : N ≤ φ n, from
         calc N ≤ n   : hn
           ... ≤ φ n : id_mne_extraccion hφ n,
       show |(u ∘ φ) n - a| ≤ ε,
         from hN (φ n) h2,
     },
   show ∃ N, ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,
     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

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

import data.real.basic

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

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

-- Nota. Usaremos los siguientes conceptos estudiados

-- anteriormente.

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

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

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

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

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

lemma extraccion_mye

(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'))⟩

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

-- Ejercicio. Demostrar que las subsucesiones de las

-- sucesiones convergentes tienen el mismo límite que

-- la sucesión.

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

-- 1ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

-- unfold limite,

intros ε hε,

-- unfold limite at h,

cases h ε hε with N hN,

use N,

intros n hn,

apply hN,

apply le_trans hn,

exact id_mne_extraccion hφ n,

end

-- 2ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

cases h ε hε with N hN,

use N,

intros n hn,

apply hN,

exact le_trans hn (id_mne_extraccion hφ n),

end

-- 3ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

cases h ε hε with N hN,

use N,

intros n hn,

exact hN (φ n) (le_trans hn (id_mne_extraccion hφ n)),

end

-- 4ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

cases h ε hε with N hN,

use N,

exact λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n)),

end

-- 5ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

-- unfold limite at h,

cases h ε hε with N hN,

exact ⟨N, λ n hn, hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩,

end

-- 6ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

exact (exists.elim (h ε hε)

(λ N hN,

⟨N, λ n hn,

hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩)),

end

-- 7ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

λ ε hε,

(exists.elim (h ε hε)

(λ N hN,

⟨N, λ n hn,

hN (φ n) (le_trans hn (id_mne_extraccion hφ n))⟩))

-- 8ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

unfold limite at h,

cases h ε hε with N hN,

use N,

intros n hn,

apply hN,

calc N ≤ n : hn

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

end

-- 9ª demostración

example

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

assume ε,

assume hε : ε > 0,

exists.elim (h ε hε)

( assume N,

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

have h1 : ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,

{ assume n,

assume hn : n ≥ N,

have h2 : N ≤ φ n, from

calc N ≤ n : hn

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

show |(u ∘ φ) n - a| ≤ ε,

from hN (φ n) h2,

show ∃ N, ∀n, n ≥ N → |(u ∘ φ) n - a| ≤ ε,

from exists.intro N h1)

ForMatUS: Pruebas en Lean de “Hay infinitos términos arbitrariamente próximos a los puntos de acumulación”

PorJosé A. Alonso 11 enero 202111 enero 2021

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

Si a es un punto de acumulación de la sucesión u, entonces

∀ ε > 0, ∀ N, ∃ n ≥ N, |u n – a| ≤ ε

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

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

-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------

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

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

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

lemma extraccion_mye
  (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'))⟩

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    punto_acumulacion : (ℕ → ℝ) → ℝ → Prop
-- tal que (punto_acumulacion u a) expresa que a es un
-- punto de acumulación de u; es decir, que es el
-- límite de alguna subsucesión de u.
-- ----------------------------------------------------

def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop
| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que si a es un punto de
-- acumulación de u, entonces
--    ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
  intros ε hε N,
  -- unfold punto_acumulacion at h,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  -- unfold limite at hφ2,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  -- clear hφ1 hφ2,
  use φ m,
  split,
  { exact hm', },
  { exact hN' m hm, },
end

-- 2ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  use φ m,
  exact ⟨hm', hN' m hm⟩,
end

-- 3ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end

-- 4ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  use φ m ; finish
end

-- 5ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                have h2 : |u (φ m) - a| ≤ ε,
                  from hN' m hm1,
                show ∃ n ≥ N, |u n - a| ≤ ε,
                  from exists.intro (φ m) (exists.intro hm2 h2)))))

-- 6ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                have h2 : |u (φ m) - a| ≤ ε,
                  from hN' m hm1,
                show ∃ n ≥ N, |u n - a| ≤ ε,
                  from ⟨φ m, hm2, h2⟩))))

-- 7ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                have h2 : |u (φ m) - a| ≤ ε,
                  from hN' m hm1,
                ⟨φ m, hm2, h2⟩))))

-- 8ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              ( assume hm1 : m ≥ N',
                assume hm2 : φ m ≥ N,
                ⟨φ m, hm2, hN' m hm1⟩))))

-- 9ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          ( assume m,
            assume hm : ∃ (H : m ≥ N'), φ m ≥ N,
            exists.elim hm
              (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 10ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        have h1 : ∃ n ≥ N', φ n ≥ N,
          from extraccion_mye hφ.1 N N',
        exists.elim h1
          (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 11ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      ( assume N',
        assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| ≤ ε,
        exists.elim (extraccion_mye hφ.1 N N')
          (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 12ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  ( assume φ,
    assume hφ : extraccion φ ∧ limite (u ∘ φ) a,
    exists.elim (hφ.2 ε hε)
      (λ N' hN', exists.elim (extraccion_mye hφ.1 N N')
        (λ m hm, exists.elim hm
          (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 13ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
assume ε,
assume hε : ε > 0,
assume N,
exists.elim h
  (λ φ hφ, exists.elim (hφ.2 ε hε)
    (λ N' hN', exists.elim (extraccion_mye hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 14ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
λ ε hε N, exists.elim h
  (λ φ hφ, exists.elim (hφ.2 ε hε)
    (λ N' hN', exists.elim (extraccion_mye hφ.1 N N')
      (λ m hm, exists.elim hm
        (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

import data.real.basic

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

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

-- Nota. Usaremos los siguientes conceptos estudiados

-- anteriormente.

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

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

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

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

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

lemma extraccion_mye

(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'))⟩

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

-- Ejercicio 1. Definir la función

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

-- tal que (punto_acumulacion u a) expresa que a es un

-- punto de acumulación de u; es decir, que es el

-- límite de alguna subsucesión de u.

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

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

| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

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

-- Ejercicio 2. Demostrar que si a es un punto de

-- acumulación de u, entonces

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

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

-- 1ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

begin

intros ε hε N,

-- unfold punto_acumulacion at h,

rcases h with ⟨φ, hφ1, hφ2⟩,

-- unfold limite at hφ2,

cases hφ2 ε hε with N' hN',

rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,

-- clear hφ1 hφ2,

use φ m,

split,

{ exact hm', },

{ exact hN' m hm, },

end

-- 2ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,

use φ m,

exact ⟨hm', hN' m hm⟩,

end

-- 3ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,

exact ⟨φ m, hm', hN' _ hm⟩,

end

-- 4ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,

use φ m ; finish

end

-- 5ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

have h1 : ∃ n ≥ N', φ n ≥ N,

from extraccion_mye hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

have h2 : |u (φ m) - a| ≤ ε,

from hN' m hm1,

show ∃ n ≥ N, |u n - a| ≤ ε,

from exists.intro (φ m) (exists.intro hm2 h2)))))

-- 6ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

have h1 : ∃ n ≥ N', φ n ≥ N,

from extraccion_mye hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

have h2 : |u (φ m) - a| ≤ ε,

from hN' m hm1,

show ∃ n ≥ N, |u n - a| ≤ ε,

from ⟨φ m, hm2, h2⟩))))

-- 7ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

have h1 : ∃ n ≥ N', φ n ≥ N,

from extraccion_mye hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

have h2 : |u (φ m) - a| ≤ ε,

from hN' m hm1,

⟨φ m, hm2, h2⟩))))

-- 8ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

have h1 : ∃ n ≥ N', φ n ≥ N,

from extraccion_mye hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

( assume hm1 : m ≥ N',

assume hm2 : φ m ≥ N,

⟨φ m, hm2, hN' m hm1⟩))))

-- 9ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

have h1 : ∃ n ≥ N', φ n ≥ N,

from extraccion_mye hφ.1 N N',

exists.elim h1

( assume m,

assume hm : ∃ (H : m ≥ N'), φ m ≥ N,

exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 10ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

have h1 : ∃ n ≥ N', φ n ≥ N,

from extraccion_mye hφ.1 N N',

exists.elim h1

(λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 11ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

( assume N',

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

exists.elim (extraccion_mye hφ.1 N N')

(λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 12ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

( assume φ,

assume hφ : extraccion φ ∧ limite (u ∘ φ) a,

exists.elim (hφ.2 ε hε)

(λ N' hN', exists.elim (extraccion_mye hφ.1 N N')

(λ m hm, exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 13ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

assume ε,

assume hε : ε > 0,

assume N,

exists.elim h

(λ φ hφ, exists.elim (hφ.2 ε hε)

(λ N' hN', exists.elim (extraccion_mye hφ.1 N N')

(λ m hm, exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

-- 14ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

λ ε hε N, exists.elim h

(λ φ hφ, exists.elim (hφ.2 ε hε)

(λ N' hN', exists.elim (extraccion_mye hφ.1 N N')

(λ m hm, exists.elim hm

(λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))

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)