Menu Close

Día: 4 enero, 2021

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

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