Lean_Prover – Página 4

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)

ForMatUS: Si |x| < ε, para todo ε > 0, entonces x = 0

PorJosé A. Alonso 4 enero 20213 enero 2021

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

Si |x| < ε, para todo ε > 0, entonces x = 0

usando los estilos declarativos, 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 (x : ℝ)

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

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

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

-- 1ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
begin
  rw ← abs_eq_zero,
  apply eq_of_le_of_forall_le_of_dense,
  { exact abs_nonneg x, },
  { intros ε hε,
    apply le_of_lt,
    exact h ε hε, },
end

-- 2ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
begin
  rw ← abs_eq_zero,
  apply eq_of_le_of_forall_le_of_dense,
  { exact abs_nonneg x, },
  { intros ε hε,
    exact le_of_lt (h ε hε), },
end

-- 3ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
begin
  rw ← abs_eq_zero,
  apply eq_of_le_of_forall_le_of_dense,
  { exact abs_nonneg x, },
  { exact λ ε hε, le_of_lt (h ε hε), },
end

-- 4ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
begin
  rw ← abs_eq_zero,
  apply eq_of_le_of_forall_le_of_dense
        (abs_nonneg x)
        (λ ε hε, le_of_lt (h ε hε)),
end

-- 5ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
abs_eq_zero.mp
  (eq_of_le_of_forall_le_of_dense
    (abs_nonneg x)
    (λ ε hε, le_of_lt (h ε hε)))

-- 6ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
have h1 : 0 ≤ |x|,
  from abs_nonneg x,
have h2 : ∀ ε, ε > 0 → |x| ≤ ε,
  { assume ε,
    assume hε : ε > 0,
    have h2a : |x| < ε,
      from h ε hε,
    show |x| ≤ ε,
      from le_of_lt h2a },
have h3 : |x| = 0,
  from eq_of_le_of_forall_le_of_dense h1 h2,
show x = 0,
  from abs_eq_zero.mp h3

-- 7ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
have h1 : 0 ≤ |x|,
  from abs_nonneg x,
have h2 : ∀ ε, ε > 0 → |x| ≤ ε,
  { assume ε,
    assume hε : ε > 0,
    have h2a : |x| < ε,
      from h ε hε,
    show |x| ≤ ε,
      from le_of_lt h2a },
have h3 : |x| = 0,
  from eq_of_le_of_forall_le_of_dense h1 h2,
abs_eq_zero.mp h3

-- 8ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
have h1 : 0 ≤ |x|,
  from abs_nonneg x,
have h2 : ∀ ε, ε > 0 → |x| ≤ ε,
  { assume ε,
    assume hε : ε > 0,
    have h2a : |x| < ε,
      from h ε hε,
    show |x| ≤ ε,
      from le_of_lt h2a },
abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2)

-- 9ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
have h1 : 0 ≤ |x|,
  from abs_nonneg x,
have h2 : ∀ ε, ε > 0 → |x| ≤ ε,
  { assume ε,
    assume hε : ε > 0,
    show |x| ≤ ε,
      from le_of_lt (h ε hε) },
abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2)

-- 10ª demostración
example
  (h : ∀ ε > 0, |x| < ε)
  : x = 0 :=
abs_eq_zero.mp
  (eq_of_le_of_forall_le_of_dense
    (abs_nonneg x)
    (λ ε hε, le_of_lt (h ε 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

134

135

136

137

138

139

140

141

142

143

import data.real.basic

variable (x : ℝ)

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

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

-- absoluto de x.

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

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

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

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

-- ε > 0, entonces x = 0

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

-- 1ª demostración

example

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

: x = 0 :=

begin

rw ← abs_eq_zero,

apply eq_of_le_of_forall_le_of_dense,

{ exact abs_nonneg x, },

{ intros ε hε,

apply le_of_lt,

exact h ε hε, },

end

-- 2ª demostración

example

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

: x = 0 :=

begin

rw ← abs_eq_zero,

apply eq_of_le_of_forall_le_of_dense,

{ exact abs_nonneg x, },

{ intros ε hε,

exact le_of_lt (h ε hε), },

end

-- 3ª demostración

example

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

: x = 0 :=

begin

rw ← abs_eq_zero,

apply eq_of_le_of_forall_le_of_dense,

{ exact abs_nonneg x, },

{ exact λ ε hε, le_of_lt (h ε hε), },

end

-- 4ª demostración

example

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

: x = 0 :=

begin

rw ← abs_eq_zero,

apply eq_of_le_of_forall_le_of_dense

(abs_nonneg x)

(λ ε hε, le_of_lt (h ε hε)),

end

-- 5ª demostración

example

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

: x = 0 :=

abs_eq_zero.mp

(eq_of_le_of_forall_le_of_dense

(abs_nonneg x)

(λ ε hε, le_of_lt (h ε hε)))

-- 6ª demostración

example

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

: x = 0 :=

have h1 : 0 ≤ |x|,

from abs_nonneg x,

have h2 : ∀ ε, ε > 0 → |x| ≤ ε,

{ assume ε,

assume hε : ε > 0,

have h2a : |x| < ε,

from h ε hε,

show |x| ≤ ε,

from le_of_lt h2a },

have h3 : |x| = 0,

from eq_of_le_of_forall_le_of_dense h1 h2,

show x = 0,

from abs_eq_zero.mp h3

-- 7ª demostración

example

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

: x = 0 :=

have h1 : 0 ≤ |x|,

from abs_nonneg x,

have h2 : ∀ ε, ε > 0 → |x| ≤ ε,

{ assume ε,

assume hε : ε > 0,

have h2a : |x| < ε,

from h ε hε,

show |x| ≤ ε,

from le_of_lt h2a },

have h3 : |x| = 0,

from eq_of_le_of_forall_le_of_dense h1 h2,

abs_eq_zero.mp h3

-- 8ª demostración

example

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

: x = 0 :=

have h1 : 0 ≤ |x|,

from abs_nonneg x,

have h2 : ∀ ε, ε > 0 → |x| ≤ ε,

{ assume ε,

assume hε : ε > 0,

have h2a : |x| < ε,

from h ε hε,

show |x| ≤ ε,

from le_of_lt h2a },

abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2)

-- 9ª demostración

example

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

: x = 0 :=

have h1 : 0 ≤ |x|,

from abs_nonneg x,

have h2 : ∀ ε, ε > 0 → |x| ≤ ε,

{ assume ε,

assume hε : ε > 0,

show |x| ≤ ε,

from le_of_lt (h ε hε) },

abs_eq_zero.mp (eq_of_le_of_forall_le_of_dense h1 h2)

-- 10ª demostración

example

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

: x = 0 :=

abs_eq_zero.mp

(eq_of_le_of_forall_le_of_dense

(abs_nonneg x)

(λ ε hε, le_of_lt (h ε hε)))

ForMatUS: Pruebas en Lean del teorema del emparedado

PorJosé A. Alonso 3 enero 20212 enero 2021

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

ForMatUS: Pruebas en Lean de que la identidad es biyectiva

PorJosé A. Alonso 3 noviembre 202022 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de que la identidad es biyectiva 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 tactic

open function

variables {X : Type}

-- #print injective
-- #print surjective
-- #print bijective

-- ----------------------------------------------------
-- Ej. 1. Demostrar que la identidad es inyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : injective (@id X) :=
begin
  intros x₁ x₂ h,
  exact h,
end

-- 2ª demostración
example : injective (@id X) :=
λ x₁ x₂ h, h

-- 3ª demostración
example : injective (@id X) :=
λ x₁ x₂, id

-- 4ª demostración
example : injective (@id X) :=
assume x₁ x₂,
assume h : id x₁ = id x₂,
show x₁ = x₂, from h

-- 5ª demostración
example : injective (@id X) :=
--by library_search
injective_id

-- 6ª demostración
example : injective (@id X) :=
-- by hint
by tauto

-- 7ª demostración
example : injective (@id X) :=
-- by hint
by finish

-- ----------------------------------------------------
-- Ej. 2. Demostrar que la identidad es suprayectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : surjective (@id X) :=
begin
  intro x,
  use x,
  exact rfl,
end

-- 2ª demostración
example : surjective (@id X) :=
begin
  intro x,
  exact ⟨x, rfl⟩,
end

-- 3ª demostración
example : surjective (@id X) :=
λ x, ⟨x, rfl⟩

-- 4ª demostración
example : surjective (@id X) :=
assume y,
show ∃ x, id x = y, from exists.intro y rfl

-- 5ª demostración
example : surjective (@id X) :=
-- by library_search
surjective_id

-- 6ª demostración
example : surjective (@id X) :=
-- by hint
by tauto

-- ----------------------------------------------------
-- Ej. 3. Demostrar que la identidad es biyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : bijective (@id X) :=
and.intro injective_id surjective_id

-- 2ª demostración
example : bijective (@id X) :=
⟨injective_id, surjective_id⟩

-- 3ª demostración
example : bijective (@id X) :=
-- by library_search
bijective_id

100

101

102

103

104

import tactic

open function

variables {X : Type}

-- #print injective

-- #print surjective

-- #print bijective

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

-- Ej. 1. Demostrar que la identidad es inyectiva.

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

-- 1ª demostración