ForMatUS: Pruebas en Lean del teorema del emparedado

He añadido a la lista Lógica con Lean el vídeo Teorema del emparedado en el que se comentan pruebas en Lean del teorema del emparedado:

Si dos sucesiones tienen el mismo límite, entonces las sucesiones que están comprendidas entre éstas también tienen el mismo límite.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

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

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

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

-- ----------------------------------------------------
-- Ejercicio 2. Definir la función
--    limite : (ℕ → ℝ) → ℝ → Prop
-- tal que (limite u c) expresa que c es el límite de
-- la sucesión u.
-- ----------------------------------------------------

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

-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que si dos sucesiones tienen
-- el mismo límite, entonces las sucesiones que están
-- comprendidas entre éstas también tienen el mismo
-- límite.
-- ----------------------------------------------------

-- 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ε : ε &gt; 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

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

import data.real.basic

variables (u v w : ℕ → ℝ)

variable (a : ℝ)

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

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

-- absoluto de x.

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

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

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

-- Ejercicio 2. Definir la función

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

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

-- la sucesión u.

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

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

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

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

-- Ejercicio 3. Demostrar que si dos sucesiones tienen

-- el mismo límite, entonces las sucesiones que están

-- comprendidas entre éstas también tienen el mismo

-- límite.

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

-- 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 imprimir o compartir con