Menu Close

Autor: José A. Alonso

Pruebas en Lean de “La función identidad no está acotada superiormente”

José A. Alonso--

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

La función identidad no está acotada superiormente

usando los estilos aplicativo, declarativo, y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
 
-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    acotada_superiormente : (ℝ → ℝ) → Prop
-- tal que (acotada_superiormente f) expresa que la
-- función f está acotada superiormente.
-- ----------------------------------------------------
 
def acotada_superiormente : (ℝ → ℝ) → Prop
| f := ∃ M, ∀ x, f x ≤ M
 
-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que la función identidad no
-- está acotada superiormente.
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬acotada_superiormente id :=
begin
  unfold acotada_superiormente,
  unfold id,
  by_contradiction h,
  cases h with M hM,
  specialize hM (M+1),
  contrapose hM,
  simp only [not_le],
  exact lt_add_one M,
end
 
-- 2ª demostración
example : ¬acotada_superiormente id :=
begin
  unfold acotada_superiormente id,
  push_neg,
  intro M,
  use M + 1,
  linarith,
end
 
-- 3ª demostración
example : ¬acotada_superiormente id :=
begin
  unfold acotada_superiormente id,
  push_neg,
  exact no_top,
end
 
-- 4ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      have h3 : M + 1 ≤ M,
        from hM (M+1),
      have h4 : ¬(M < M + 1),
        from not_lt.mpr h3,
      have h5 : M < M + 1,
        from lt_add_one M,
      show false,
        from h4 h5)
 
-- 5ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      have h3 : M + 1 ≤ M,
        from hM (M+1),
      have h4 : ¬(M < M + 1),
        from not_lt.mpr h3,
      have h5 : M < M + 1,
        from lt_add_one M,
      h4 h5)
 
-- 6ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      have h3 : M + 1 ≤ M,
        from hM (M+1),
      (not_lt.mpr h3) (lt_add_one M))
 
-- 7ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      (not_lt.mpr (hM (M+1))) (lt_add_one M))
 
-- 8ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))
 
-- 9ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
exists.elim h2
  (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))
 
-- 10ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
exists.elim h1
  (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))
 
-- 11ª demostración
example : ¬acotada_superiormente id :=
λ h1, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))
Seguir leyendo →

Negación del universal en Lean: Caracterización de funciones no pares

José A. Alonso--

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

¬par f ↔ ∃ x, f (-x) ≠ f x

usando los estilos declarativo, aplicativo y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
 
variable (f : ℝ → ℝ)
 
-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    par : (ℝ → ℝ) → Prop
-- tal que (par f) expresa que f es par.
-- ----------------------------------------------------
 
def par : (ℝ → ℝ) → Prop
| f := ∀ x, f (-x) = f x
 
-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que
--    ¬par f ↔ ∃ x, f (-x) ≠ f x
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
begin
  split,
  { contrapose,
    intro h1,
    rw not_not,
    unfold par,
    intro x,
    by_contradiction h2,
    apply h1,
    use x, },
  { intro h1,
    intro h2,
    unfold par at h2,
    cases h1 with x hx,
    apply hx,
    exact h2 x, },
end
 
-- 2ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
begin
  split,
  { contrapose,
    intro h1,
    rw not_not,
    intro x,
    by_contradiction h2,
    apply h1,
    use x, },
  { rintros ⟨x, hx⟩ h',
    exact hx (h' x) },
end
 
-- 3ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
begin
  unfold par,
  push_neg,
end
 
-- 4ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
iff.intro
  ( have h1 : ¬(∃ x, f (-x) ≠ f x) → ¬¬par f,
      { assume h2 : ¬(∃ x, f (-x) ≠ f x),
        have h3 : par f,
          { assume x,
            have h4 : ¬(f (-x) ≠ f x),
              { assume h5 : f (-x) ≠ f x,
                have h6 : ∃ x, f (-x) ≠ f x,
                  from exists.intro x h5,
                show false,
                  from h2 h6, },
            show f (-x) = f x,
              from not_not.mp h4},
        show ¬¬par f,
          from not_not.mpr h3 },
    show ¬par f → (∃ x, f (-x) ≠ f x),
      from not_imp_not.mp h1)
  ( assume h1 : ∃ x, f (-x) ≠ f x,
    show ¬par f,
      { assume h2 : par f,
        show false, from
          exists.elim h1
            ( assume x,
              assume hx : f (-x) ≠ f x,
              have h3 : f (-x) = f x,
                from h2 x,
              show false,
                from hx h3)})
 
-- 5ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
-- by suggest
not_forall
 
-- 6ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
-- by hint
by simp [par]
Seguir leyendo →

Negación del existencial en Lean: Caracterización de números no pares

José A. Alonso--

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

¬(∃ k, n = 2k) ↔ ∀ k, n ≠ 2k

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 tactic
 
variable (n : ℤ)
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que si n es un número entero,
-- entonces
--    ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
begin
  split,
  { intro h,
    intro k,
    intro hk,
    apply h,
    use k,
    exact hk, },
  { intro h1,
    intro h2,
    cases h2 with k hk,
    apply h1 k,
    exact hk, },
end
 
-- 2ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
begin
  split,
  { intros h k hk,
    exact h ⟨k, hk⟩ },
  { rintros h ⟨k, rfl⟩,
    apply h k,
    refl, },
end
 
-- 3ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
begin
  split,
  { intros h k hk,
    exact h ⟨k, hk⟩ },
  { rintros h ⟨k, rfl⟩,
    exact h k rfl },
end
 
-- 4ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
begin
  push_neg,
end
 
-- 5ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
by push_neg
 
-- 6ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
iff.intro
  ( assume h1 : ¬(∃ k, n = 2*k),
    show ∀ k, n ≠ 2*k, from
      assume k,
      show n ≠ 2*k, from
        assume h2 : n = 2*k,
        have h3 : ∃ k, n = 2*k,
          from exists.intro k h2,
        show false,
          from h1 h3)
  ( assume h1 : ∀ k, n ≠ 2*k,
    show ¬(∃ k, n = 2*k), from
      assume h2 : ∃ k, n = 2*k,
      show false, from
        exists.elim h2
          ( assume k,
            assume hk : n = 2*k,
            have h3 : n ≠ 2*k,
              from h1 k,
            show false,
              from h3 hk))
 
-- 7ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
iff.intro
  ( assume h1 : ¬(∃ k, n = 2*k),
    show ∀ k, n ≠ 2*k, from
      assume k,
      show n ≠ 2*k, from
        assume h2 : n = 2*k,
        have h3 : ∃ k, n = 2*k,
          from exists.intro k h2,
        h1 h3)
  ( assume h1 : ∀ k, n ≠ 2*k,
    show ¬(∃ k, n = 2*k), from
      assume h2 : ∃ k, n = 2*k,
      show false, from
        exists.elim h2
          ( assume k,
            assume hk : n = 2*k,
            have h3 : n ≠ 2*k,
              from h1 k,
            h3 hk))
 
-- 8ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
iff.intro
  ( assume h1 : ¬(∃ k, n = 2*k),
    show ∀ k, n ≠ 2*k, from
      assume k,
      show n ≠ 2*k, from
        assume h2 : n = 2*k,
        h1 (exists.intro k h2))
  ( assume h1 : ∀ k, n ≠ 2*k,
    show ¬(∃ k, n = 2*k), from
      assume h2 : ∃ k, n = 2*k,
      show false, from
        exists.elim h2
          ( assume k,
            assume hk : n = 2*k,
            (h1 k) hk))
 
-- 9ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
iff.intro
  ( assume h1 : ¬(∃ k, n = 2*k),
    show ∀ k, n ≠ 2*k, from
      assume k,
      λ h2, h1 (exists.intro k h2))
  ( assume h1 : ∀ k, n ≠ 2*k,
    show ¬(∃ k, n = 2*k), from
      assume h2 : ∃ k, n = 2*k,
      show false, from
        exists.elim h2
          (λ k hk, (h1 k) hk))
 
-- 10ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
iff.intro
  ( assume h1 : ¬(∃ k, n = 2*k),
    λ k, λ h2, h1 (exists.intro k h2))
  ( assume h1 : ∀ k, n ≠ 2*k,
    show ¬(∃ k, n = 2*k), from
      assume h2 : ∃ k, n = 2*k,
      exists.elim h2 (λ k hk, (h1 k) hk))
 
-- 11ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
iff.intro
  (λ h1 k h2, h1 (exists.intro k h2))
  (λ h1 h2, exists.elim h2 (λ k hk, (h1 k) hk))
 
-- 12ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
⟨λ h1 k h2, h1 ⟨k, h2⟩,
 λ h1 h2, exists.elim h2 (λ k hk, (h1 k) hk)⟩
 
-- 13ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
-- by hint
by simp
 
-- 14ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
by finish
 
-- 15ª demostración
example : ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k :=
by norm_num
Seguir leyendo →

Pruebas en Lean de la ley de De Morgan: ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

José A. Alonso--

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

¬(P ∧ Q) ↔ ¬P ∨ ¬Q

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 tactic
variables (P Q : Prop)
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que
--    ¬(P ∧ Q) ↔ ¬P ∨ ¬Q
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
begin
  split,
  { intro h,
    by_cases hP : P,
    { right,
      intro hQ,
      apply h,
      split,
      { exact hP, },
      { exact hQ, }},
    { left,
      exact hP, }},
  { intros h h',
    cases h' with hP hQ,
    cases h with hnP hnQ,
    { exact hnP hP, },
    { exact hnQ hQ, }},
end
 
-- 2ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
begin
  split,
  { intro h,
    by_cases hP : P,
    { right,
      intro hQ,
      exact h ⟨hP, hQ⟩, },
    { left,
      exact hP, }},
  { rintros (hnP | hnQ) ⟨hP, hQ⟩,
    { exact hnP hP, },
    { exact hnQ hQ, }},
end
 
-- 3ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          show ¬P ∨ ¬Q,
            from or.inr hnQ)
        ( assume hnP : ¬P,
          show ¬P ∨ ¬Q,
            from or.inl hnP))
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          ( assume hnP: ¬P,
            show false,
              from hnP (and.left hPQ))
          ( assume hnQ: ¬Q,
            show false,
              from hnQ (and.right hPQ)))
 
-- 4ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          show ¬P ∨ ¬Q,
            from or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          ( assume hnP: ¬P,
            show false,
              from hnP (and.left hPQ))
          (λ hnQ, hnQ (and.right hPQ)))
 
-- 5ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          (λ hnP, hnP (and.left hPQ))
          (λ hnQ, hnQ (and.right hPQ)))
 
-- 6ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              show false,
                from h (and.intro hP hQ) },
          or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      λ hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))
 
-- 7ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          or.inr (λ hQ, h (and.intro hP hQ)))
        or.inl)
  ( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))
 
-- 8ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        (λ hP, or.inr (λ hQ, h (and.intro hP hQ)))
        or.inl)
  ( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))
 
-- 9ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  (λ h, or.elim (classical.em P)
          (λ hP, or.inr (λ hQ, h (and.intro hP hQ)))
          or.inl)
  (λ h hPQ, or.elim h
              (λ hnP, hnP (and.left hPQ))
              (λ hnQ, hnQ (and.right hPQ)))
 
-- 10ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
⟨λ h, or.elim (classical.em P) (λ hP, or.inr (λ hQ, h ⟨hP, hQ⟩)) or.inl,
 λ h hPQ, or.elim h (λ hnP, hnP hPQ.1) (λ hnQ, hnQ hPQ.2)⟩
 
-- 11ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
-- by library_search
not_and_distrib
 
-- 12ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
-- by hint
by finish
Seguir leyendo →

Pruebas en Lean de “Un número es par si, y sólo si, lo es su cuadrado”

José A. Alonso--

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

Un número es par si, y sólo si, lo es su cuadrado-

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.int.parity
open int
 
variable (n : ℤ)
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que un número es par syss lo es
-- su cuadrado.
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    rw ← odd_iff_not_even,
    rw ← odd_iff_not_even,
    unfold odd,
    intro h,
    cases h with k hk,
    use 2*k*(k+1),
    rw hk,
    ring, },
  { unfold even,
    intro h,
    cases h with k hk,
    use 2*k^2,
    rw hk,
    ring, },
end
 
-- 2ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    rw ← odd_iff_not_even,
    rw ← odd_iff_not_even,
    rintro ⟨k, rfl⟩,
    use 2*k*(k+1),
    ring, },
  { rintro ⟨k, rfl⟩,
    use 2*k^2,
    ring, },
end
 
-- 3ª demostración
example :
  even (n^2) ↔ even n :=
iff.intro
  ( have h : ¬even n → ¬even (n^2),
      { assume h1 : ¬even n,
        have h2 : odd n,
          from odd_iff_not_even.mpr h1,
        have h3: odd (n^2), from
          exists.elim h2
            ( assume k,
              assume hk : n = 2*k+1,
              have h4 : n^2 = 2*(2*k*(k+1))+1, from
                calc  n^2
                    = (2*k+1)^2       : by rw hk
                ... = 4*k^2+4*k+1     : by ring
                ... = 2*(2*k*(k+1))+1 : by ring,
              show odd (n^2),
                from exists.intro (2*k*(k+1)) h4),
        show ¬even (n^2),
          from odd_iff_not_even.mp h3 },
    show even (n^2) → even n,
      from not_imp_not.mp h )
  ( assume h1 : even n,
    show even (n^2), from
      exists.elim h1
        ( assume k,
          assume hk : n = 2*k ,
          have h2 : n^2 = 2*(2*k^2), from
            calc  n^2
                = (2*k)^2   : by rw hk
            ... = 2*(2*k^2) : by ring,
          show even (n^2),
            from exists.intro (2*k^2) h2 ))
Seguir leyendo →

Pruebas en Lean de “La relación menor es irreflexiva en los reales”

José A. Alonso--

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

La relación menor es irreflexiva en los reales

usando los estilos declarativo, funcional, aplicativo y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
import tactic
 
variable {x : ℝ}
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que la relación menor es
-- irreflexiva en los reales.
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬ x < x :=
begin
  intro h1,
  rw lt_iff_le_and_ne at h1,
  cases h1 with h2 h3,
  -- clear h2,
  -- change x = x → false at h3,
  apply h3,
  refl,
end
 
-- 2ª demostración
example : ¬ x < x :=
begin
  intro h1,
  rw lt_iff_le_and_ne at h1,
  cases h1 with h2 h3,
  apply h3,
  refl,
end
 
-- 3ª demostración
example : ¬ x < x :=
begin
  intro h1,
  cases (lt_iff_le_and_ne.mp h1) with h2 h3,
  apply h3,
  refl,
end
 
-- 4ª demostración
example : ¬ x < x :=
begin
  intro h1,
  apply (lt_iff_le_and_ne.mp h1).2,
  refl,
end
 
-- 5ª demostración
example : ¬ x < x :=
begin
  intro h1,
  exact absurd rfl (lt_iff_le_and_ne.mp h1).2,
end
 
-- 6ª demostración
example : ¬ x < x :=
λ h, absurd rfl (lt_iff_le_and_ne.mp h).2
 
-- 7ª demostración
example : ¬ x < x :=
assume h1 : x < x,
have h2 : x ≤ x ∧ x ≠ x,
  from lt_iff_le_and_ne.mp h1,
have h3 : x ≠ x,
  from and.right h2,
have h4 : x = x,
  from rfl,
show false,
  from absurd h4 h3
 
-- 8ª demostración
example : ¬ x < x :=
assume h1 : x < x,
have h2 : x ≤ x ∧ x ≠ x,
  from lt_iff_le_and_ne.mp h1,
absurd rfl (and.right h2)
 
-- 9ª demostración
example : ¬ x < x :=
assume h1 : x < x,
absurd rfl (and.right (lt_iff_le_and_ne.mp h1))
 
-- 10ª demostración
example : ¬ x < x :=
assume h1 : x < x,
absurd rfl (lt_iff_le_and_ne.mp h1).2
 
-- 11ª demostración
example : ¬ x < x :=
λ h, absurd rfl (lt_iff_le_and_ne.mp h).2
 
-- 12ª demostración
example : ¬ x < x :=
-- by library_search
irrefl x
 
-- 12ª demostración
example : ¬ x < x :=
-- by hint
by simp
 
-- 13ª demostración
example : ¬ x < x :=
by finish
 
-- 14ª demostración
example : ¬ x < x :=
by norm_num
 
-- 15ª demostración
example : ¬ x < x :=
by linarith
 
-- 16ª demostración
example : ¬ x < x :=
by nlinarith
Seguir leyendo →

Pruebas en Lean de “Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u”

José A. Alonso--

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

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

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'))⟩
 
def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop
| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a
 
lemma cerca_acumulacion
  (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
 
def sucesion_de_Cauchy : (ℕ → ℝ) → Prop
| u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que si u es una sucesión de
-- Cauchy y a es un punto de acumulación de u, entonces
-- a es el límite de u.
-- ----------------------------------------------------
 
-- 1ª demostración
example
  (hu : sucesion_de_Cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold sucesion_de_Cauchy at hu,
  cases hu (ε/2) (half_pos hε) with N hN,
  use N,
  have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2,
    apply cerca_acumulacion ha (ε/2) (half_pos hε),
  cases ha' with N' h,
  cases h with hNN' hN',
  intros n hn,
  calc   |u n - a|
       = |(u n - u N') + (u N' - a)| : by ring
   ... ≤ |u n - u N'| + |u N' - a|   : abs_add (u n - u N') (u N' - a)
   ... ≤ ε/2 + |u N' - a|            : add_le_add_right (hN n N' hn hNN') _
   ... ≤ ε/2 + ε/2                   : add_le_add_left hN' (ε / 2)
   ... = ε                           : add_halves ε
end
 
-- 2ª demostración
example
  (hu : sucesion_de_Cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with N hN,
  use N,
  have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2,
    apply cerca_acumulacion ha (ε/2) (by linarith),
  rcases ha' with ⟨N', hNN', hN'⟩,
  intros n hn,
  calc  |u n - a|
      = |(u n - u N') + (u N' - a)| : by ring
  ... ≤ |u n - u N'| + |u N' - a|   : by simp [abs_add]
  ... ≤ ε                           : by linarith [hN n N' hn hNN'],
end
Seguir leyendo →

Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”

José A. Alonso--

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

Toda sucesión convergente es una sucesión de Cauchy

usando los estilos aplicativo 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 : ℕ → ℝ}
 
-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------
 
notation `|`x`|` := abs x
 
def limite : (ℕ → ℝ) → ℝ → Prop :=
λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε
 
-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    sucesion_convergente : (ℕ → ℝ) → Prop
-- tal que (sucesion_convergente u) expresa que la
-- sucesión u es convergente.
-- ----------------------------------------------------
 
def sucesion_convergente : (ℕ → ℝ) → Prop
| u := ∃ a, limite u a
 
-- ----------------------------------------------------
-- Ejercicio 2. Definir la función
--    sucesion_de_Cauchy : (ℕ → ℝ) → Prop
-- tal que (sucesion_de_Cauchy u) expresa que la
-- sucesión u es una sucesión de Cauchy.
-- ----------------------------------------------------
 
def sucesion_de_Cauchy : (ℕ → ℝ) → Prop
| u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε
 
-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que toda sucesión convergente
-- es una sucesión de Cauchy.
-- ----------------------------------------------------
 
-- 1ª demostración
example
  (h : sucesion_convergente u)
  : sucesion_de_Cauchy u :=
begin
  -- unfold sucesion_convergente at h,
  cases h with a ha,
  -- unfold sucesion_de_Cauchy,
  intros ε hε,
  -- unfold limite at ha,
  cases ha (ε/2) (half_pos hε) with N hN,
  use N,
  intros p q hp hq,
  calc  |u p - u q|
      = |(u p - a) + (a - u q)| : by ring
  ... ≤ |u p - a| + |a - u q|   : by apply abs_add
  ... = |u p - a| + |u q - a|   : by rw abs_sub (u q) a
  ... ≤ ε/2 + |u q - a|         : add_le_add_right (hN p hp) _
  ... ≤ ε/2 + ε/2               : add_le_add_left (hN q hq) (ε/2)
  ... = ε                       : add_halves ε
end
 
-- 2ª demostración
example
  (h : sucesion_convergente u)
  : sucesion_de_Cauchy u :=
begin
  cases h with a ha,
  intros ε hε,
  cases ha (ε/2) (by linarith) with N hN,
  use N,
  intros p q hp hq,
  calc  |u p - u q|
      = |(u p - a) + (a - u q)| : by ring
  ... ≤ |u p - a| + |a - u q|   : by simp only [abs_add]
  ... = |u p - a| + |u q - a|   : by simp only [abs_add, abs_sub]
  ... ≤ ε                       : by linarith [hN p hp, hN q hq],
end
 
-- 3ª demostración
example
  (h : sucesion_convergente u)
  : sucesion_de_Cauchy u :=
exists.elim h
  (assume a,
   assume ha : limite u a,
   show sucesion_de_Cauchy u, from
     (assume ε,
      assume hε : ε > 0,
      exists.elim (ha (ε/2) (by linarith))
        (assume N,
         assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε/2,
         show ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε,
           from exists.intro N
             (assume p q,
              assume hp: p ≥ N,
              assume hq: q ≥ N,
              show |u p - u q| ≤ ε, from
                calc  |u p - u q|
                    = |(u p - a) + (a - u q)| : by ring
                ... ≤ |u p - a| + |a - u q|   : by simp only [abs_add]
                ... = |u p - a| + |u q - a|   : by simp only [abs_add, abs_sub]
                ... ≤ ε                       : by linarith [hN p hp, hN q hq]))))
Seguir leyendo →

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

José A. Alonso--

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φ')
Seguir leyendo →

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

José A. Alonso--

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)
Seguir leyendo →