L.rcases – Calculemus

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

PorJosé A. Alonso 4 septiembre 202130 agosto 2021

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Para extraer una subsucesión se aplica una función de extracción queconserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, \|u k - a\| < ε

que a es un punto de acumulación de u por

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

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

que la sucesión u es de Cauchy por

   def suc_cauchy (u : ℕ → ℝ) :=
     ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

1 2	def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, \|u p - u q\| < ε

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.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

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

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

def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m

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

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

def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

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

def extraccion (φ : ℕ → ℕ) :=

∀ n m, n < m → φ n < φ m

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

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

def suc_cauchy (u : ℕ → ℝ) :=

∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

example

(hu : suc_cauchy u)

(ha : punto_acumulacion u a)

: limite u a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

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

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

def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m

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

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

def suc_cauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

lemma aux1
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end

lemma aux2
  (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')
                             (aux1 h (max N N'))⟩⟩

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 aux2 hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end

-- 1ª demostración
example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold limite,
  intros ε hε,
  unfold suc_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_nf
   ... ≤ |u n - u N'| + |u N' - a|   : abs_add (u n - u N') (u N' - a)
   ... < ε/2 + |u N' - a|            : add_lt_add_right (hN n hn N' hNN') _
   ... < ε/2 + ε/2                   : add_lt_add_left hN' (ε / 2)
   ... = ε                           : add_halves ε
end

-- 2ª demostración
example
  (hu : suc_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_nf
  ... ≤ |u n - u N'| + |u N' - a|   : by simp [abs_add]
  ... < ε                           : by linarith [hN n hn N' hNN'],
end

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

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

def extraccion (φ : ℕ → ℕ) :=

∀ n m, n < m → φ n < φ m

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

∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

def suc_cauchy (u : ℕ → ℝ) :=

∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

lemma aux1

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intro n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h m (m+1) (lt_add_one m), },

end

lemma aux2

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

(aux1 h (max N N'))⟩⟩

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 aux2 hφ1 N N' with ⟨m, hm, hm'⟩,

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

end

-- 1ª demostración

example

(hu : suc_cauchy u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

unfold limite,

intros ε hε,

unfold suc_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_nf

... ≤ |u n - u N'| + |u N' - a| : abs_add (u n - u N') (u N' - a)

... < ε/2 + |u N' - a| : add_lt_add_right (hN n hn N' hNN') _

... < ε/2 + ε/2 : add_lt_add_left hN' (ε / 2)

... = ε : add_halves ε

end

-- 2ª demostración

example

(hu : suc_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_nf

... ≤ |u n - u N'| + |u N' - a| : by simp [abs_add]

... < ε : by linarith [hN n hn N' hNN'],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory "Si_a_es_un_punto_de_acumulacion_de_la_sucesion_de_Cauchy_u,_entonces_a_es_el_limite_de_u"
imports Main HOL.Real
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

definition suc_cauchy :: "(nat ⇒ real) ⇒ bool"
  where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"

(* Lemas auxiliares *)

lemma aux1 :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed

lemma aux2 :
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  have "max N N' ≥ N' ∧ φ (max N N') ≥ N"
    by (meson assms aux1 max.bounded_iff max.cobounded2)
  then show "∃k ≥ N'. φ k ≥ N"
    by blast
qed

lemma cerca_acumulacion :
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where hφ1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using hφ2 limite_def ‹ε > 0› by auto
  obtain m where "m ≥ N' ∧ φ m ≥ N"
    using aux2 hφ1 by blast
  then show "∃k≥N. ¦u k - a¦ < ε"
    using hN' by auto
qed

(* Demostración *)
lemma
  assumes "suc_cauchy u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then have "ε/2 > 0"
    by simp
  then obtain N where hN : "∀m≥N. ∀n≥N. ¦u m - u n¦ < ε/2"
    using assms(1) suc_cauchy_def
    by blast
  have "∀k≥N. ¦u k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume hk : "k ≥ N"
    obtain N' where hN'1 : "N' ≥ N" and
                    hN'2 : "¦u N' - a¦ < ε/2"
      using assms(2) cerca_acumulacion ‹ε/2 > 0› by blast
    have "¦u k - a¦ = ¦(u k - u N') + (u N'  - a)¦"
      by simp
    also have "… ≤ ¦u k - u N'¦ + ¦u N'  - a¦"
      by simp
    also have "… < ε/2 + ¦u N'  - a¦"
      using hk hN hN'1 by auto
    also have "… < ε/2 + ε/2"
      using hN'2 by auto
    also have "… = ε"
      by simp
    finally show "¦u k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦u k - a¦ < ε"
    by auto
qed

end

theory "Si_a_es_un_punto_de_acumulacion_de_la_sucesion_de_Cauchy_u,_entonces_a_es_el_limite_de_u"

imports Main HOL.Real

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

definition suc_cauchy :: "(nat ⇒ real) ⇒ bool"

where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"

(* Lemas auxiliares *)

lemma aux1 :

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0" by simp

fix n assume HI : "n ≤ φ n"

then show "Suc n ≤ φ (Suc n)"

using assms extraccion_def

by (metis Suc_leI lessI order_le_less_subst1)

qed

lemma aux2 :

assumes "extraccion φ"

shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N"

proof (intro allI)

fix N N' :: nat

have "max N N' ≥ N' ∧ φ (max N N') ≥ N"

by (meson assms aux1 max.bounded_iff max.cobounded2)

then show "∃k ≥ N'. φ k ≥ N"

by blast

qed

lemma cerca_acumulacion :

assumes "punto_acumulacion u a"

shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"

proof (intro allI impI)

fix ε :: real and N :: nat

assume "ε > 0"

obtain φ where hφ1 : "extraccion φ"

and hφ2 : "limite (u ∘ φ) a"

using assms punto_acumulacion_def by blast

obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"

using hφ2 limite_def ‹ε > 0› by auto

obtain m where "m ≥ N' ∧ φ m ≥ N"

using aux2 hφ1 by blast

then show "∃k≥N. ¦u k - a¦ < ε"

using hN' by auto

qed

(* Demostración *)

lemma

assumes "suc_cauchy u"

"punto_acumulacion u a"

shows "limite u a"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "ε > 0"

then have "ε/2 > 0"

by simp

then obtain N where hN : "∀m≥N. ∀n≥N. ¦u m - u n¦ < ε/2"

using assms(1) suc_cauchy_def

by blast

have "∀k≥N. ¦u k - a¦ < ε"

proof (intro allI impI)

fix k

assume hk : "k ≥ N"

obtain N' where hN'1 : "N' ≥ N" and

hN'2 : "¦u N' - a¦ < ε/2"

using assms(2) cerca_acumulacion ‹ε/2 > 0› by blast

have "¦u k - a¦ = ¦(u k - u N') + (u N' - a)¦"

by simp

also have "… ≤ ¦u k - u N'¦ + ¦u N' - a¦"

by simp

also have "… < ε/2 + ¦u N' - a¦"

using hk hN hN'1 by auto

also have "… < ε/2 + ε/2"

using hN'2 by auto

also have "… = ε"

by simp

finally show "¦u k - a¦ < ε" .

qed

then show "∃N. ∀k≥N. ¦u k - a¦ < ε"

by auto

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

El punto de acumulación de las sucesiones convergente es su límite

PorJosé A. Alonso 2 septiembre 202128 agosto 2021

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, \|u k - a\| < ε

que u es convergente por

   def convergente (u : ℕ → ℝ) :=
     ∃ a, limite u a

1 2	def convergente (u : ℕ → ℝ) := ∃ a, limite u a

que a es un punto de acumulación de u por

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

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

Demostrar que si u es una sucesión convergente y a es un punto de acumulación de u, entonces a es un límite de u.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

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

def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

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

example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

def extraccion (φ : ℕ → ℕ) :=

∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

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

def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a

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

-- Lemas auxiliares
-- ================

lemma unicidad_limite_aux
  {a b: ℝ}
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
begin
  by_contra h,
  set ε := b - a with hε,
  cases ha (ε/2) (by linarith) with A hA,
  cases hb (ε/2) (by linarith) with B hB,
  set N := max A B with hN,
  have hAN : A ≤ N := le_max_left A B,
  have hBN : B ≤ N := le_max_right A B,
  specialize hA N hAN,
  specialize hB N hBN,
  rw abs_lt at hA hB,
  linarith,
end

lemma unicidad_limite
  {a b: ℝ}
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (unicidad_limite_aux hb ha)
            (unicidad_limite_aux ha hb)

lemma limite_subsucesion_aux
  {φ : ℕ → ℕ}
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end

lemma limite_subsucesion
  {φ : ℕ → ℕ}
  {a : ℝ}
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros k hk,
  calc |(u ∘ φ) k - a|
       = |u (φ k) - a| : rfl
   ... < ε             : hN (φ k) _,
  calc φ k
       ≥ k : limite_subsucesion_aux hφ k
   ... ≥ N : hk,
end

-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold convergente at hu,
  cases hu with b hb,
  convert hb,
  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

-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  apply unicidad_limite hφ₂ _,
  exact limite_subsucesion hb hφ₁,
end

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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

def extraccion (φ : ℕ → ℕ) :=

∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def convergente (u : ℕ → ℝ) :=

∃ a, limite u a

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- Lemas auxiliares

-- ================

lemma unicidad_limite_aux

{a b: ℝ}

(ha : limite u a)

(hb : limite u b)

: b ≤ a :=

begin

by_contra h,

set ε := b - a with hε,

cases ha (ε/2) (by linarith) with A hA,

cases hb (ε/2) (by linarith) with B hB,

set N := max A B with hN,

have hAN : A ≤ N := le_max_left A B,

have hBN : B ≤ N := le_max_right A B,

specialize hA N hAN,

specialize hB N hBN,

rw abs_lt at hA hB,

linarith,

end

lemma unicidad_limite

{a b: ℝ}

(ha : limite u a)

(hb : limite u b)

: a = b :=

le_antisymm (unicidad_limite_aux hb ha)

(unicidad_limite_aux ha hb)

lemma limite_subsucesion_aux

{φ : ℕ → ℕ}

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intro n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h m (m+1) (lt_add_one m), },

end

lemma limite_subsucesion

{φ : ℕ → ℕ}

{a : ℝ}

(h : limite u a)

(hφ : extraccion φ)

: limite (u ∘ φ) a :=

begin

intros ε hε,

cases h ε hε with N hN,

use N,

intros k hk,

calc |(u ∘ φ) k - a|

= |u (φ k) - a| : rfl

... < ε : hN (φ k) _,

calc φ k

≥ k : limite_subsucesion_aux hφ k

... ≥ N : hk,

end

-- 1ª demostración

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

unfold convergente at hu,

cases hu with b hb,

convert hb,

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

-- 1ª demostración

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

cases hu with b hb,

convert hb,

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

apply unicidad_limite hφ₂ _,

exact limite_subsucesion hb hφ₁,

end

-- 2ª demostración

example

(hu : convergente u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

cases hu with b hb,

convert hb,

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

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

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite
imports Main HOL.Real
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* Lemas auxiliares *)

lemma unicidad_limite_aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed

lemma unicidad_limite :
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1)
    by (rule unicidad_limite_aux)
next
  show "b ≤ a" using assms(1) assms(2)
    by (rule unicidad_limite_aux)
qed

lemma limite_subsucesion_aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed

lemma limite_subsucesion :
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: limite_subsucesion_aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using hφ2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed

(* Demostración *)
lemma
  assumes "convergente u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof -
  obtain b where hb : "limite u b"
    using assms(1) convergente_def by auto
  obtain φ where hφ1 : "extraccion φ" and
                 hφ2 : "limite (u ∘ φ) a"
    using assms(2) punto_acumulacion_def  by auto
  have "limite (u ∘ φ) b"
    using hφ1 hb limite_subsucesion subsucesion_def by blast
  with hφ2 have "a = b"
    by (rule unicidad_limite)
  then show "limite u a"
    using hb by simp
qed

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite

imports Main HOL.Real

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"

where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition convergente :: "(nat ⇒ real) ⇒ bool" where

"convergente u ⟷ (∃ a. limite u a)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* Lemas auxiliares *)

lemma unicidad_limite_aux :

assumes "limite u a"

"limite u b"

shows "b ≤ a"

proof (rule ccontr)

assume "¬ b ≤ a"

let ?ε = "b - a"

have "0 < ?ε/2"

using ‹¬ b ≤ a› by auto

obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"

using assms(1) limite_def ‹0 < ?ε/2› by blast

obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"

using assms(2) limite_def ‹0 < ?ε/2› by blast

let ?C = "max A B"

have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"

using hA by simp

have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"

using hB by simp

have "∀n≥?C. ¦a - b¦ < ?ε"

proof (intro allI impI)

fix n assume "n ≥ ?C"

have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp

also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp

finally show "¦a - b¦ < b - a"

using hCa hCb ‹n ≥ ?C› by fastforce

qed

then show False by fastforce

qed

lemma unicidad_limite :

assumes "limite u a"

"limite u b"

shows "a = b"

proof (rule antisym)

show "a ≤ b" using assms(2) assms(1)

by (rule unicidad_limite_aux)

show "b ≤ a" using assms(1) assms(2)

by (rule unicidad_limite_aux)

qed

lemma limite_subsucesion_aux :

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0" by simp

fix n assume HI : "n ≤ φ n"

then show "Suc n ≤ φ (Suc n)"

using assms extraccion_def

by (metis Suc_leI lessI order_le_less_subst1)

qed

lemma limite_subsucesion :

assumes "subsucesion v u"

"limite u a"

shows "limite v a"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "ε > 0"

then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"

using assms(2) limite_def by auto

obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"

using assms(1) subsucesion_def by auto

have "∀k≥N. ¦v k - a¦ < ε"

proof (intro allI impI)

fix k

assume "N ≤ k"

also have "... ≤ φ k"

by (simp add: limite_subsucesion_aux hφ1)

finally have "N ≤ φ k" .

have "¦v k - a¦ = ¦u (φ k) - a¦"

using hφ2 by simp

also have "… < ε"

using hN ‹N ≤ φ k› by simp

finally show "¦v k - a¦ < ε" .

qed

then show "∃N. ∀k≥N. ¦v k - a¦ < ε"

by auto

qed

(* Demostración *)

lemma

assumes "convergente u"

"punto_acumulacion u a"

shows "limite u a"

proof -

obtain b where hb : "limite u b"

using assms(1) convergente_def by auto

obtain φ where hφ1 : "extraccion φ" and

hφ2 : "limite (u ∘ φ) a"

using assms(2) punto_acumulacion_def by auto

have "limite (u ∘ φ) b"

using hφ1 hb limite_subsucesion subsucesion_def by blast

with hφ2 have "a = b"

by (rule unicidad_limite)

then show "limite u a"

using hb by simp

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las subsucesiones tienen el mismo límite que la sucesión

PorJosé A. Alonso 1 septiembre 202125 agosto 2021

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

que v es una subsucesión de u por

   def subsucesion (v u : ℕ → ℝ) :=
     ∃ φ, extraccion φ ∧ v = u ∘ φ

1 2	def subsucesion (v u : ℕ → ℝ) := ∃ φ, extraccion φ ∧ v = u ∘ φ

y que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, \|u k - a\| < ε

Demostrar que las subsucesiones de una sucesión convergente tienen el mismo límite que la sucesión.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

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

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
sorry

import data.real.basic

open nat

variables {u v : ℕ → ℝ}

variable {a : ℝ}

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=

∀ n m, n < m → φ n < φ m

def subsucesion (v u : ℕ → ℝ) :=

∃ φ, extraccion φ ∧ v = u ∘ φ

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

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

example

(hv : subsucesion v u)

(ha : limite u a)

: limite v a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

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

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

-- En la demostración se usará el siguiente lema.
lemma aux
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end

-- 1ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  unfold limite,
  intros ε hε,
  unfold limite at ha,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  unfold subsucesion at hv,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  apply hN,
  apply le_trans hn,
  exact aux hφ1 n,
end

-- 2ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  apply hN,
  exact le_trans hn (aux hφ1 n),
end

-- 3ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  exact hN (φ n) (le_trans hn (aux hφ1 n)),
end

-- 4ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  use N,
  exact λ n hn, hN (φ n) (le_trans hn (aux hφ1 n)),
end

-- 5ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  exact ⟨N, λ n hn, hN (φ n) (le_trans hn (aux hφ1 n))⟩,
end

100

101

102

103

104

105

106

107

108

import data.real.basic

open nat

variables {u v : ℕ → ℝ}

variable {a : ℝ}

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=

∀ n m, n < m → φ n < φ m

def subsucesion (v u : ℕ → ℝ) :=

∃ φ, extraccion φ ∧ v = u ∘ φ

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

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

-- En la demostración se usará el siguiente lema.

lemma aux

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intro n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h m (m+1) (lt_add_one m), },

end

-- 1ª demostración

example

(hv : subsucesion v u)

(ha : limite u a)

: limite v a :=

begin

unfold limite,

intros ε hε,

unfold limite at ha,

cases ha ε hε with N hN,

use N,

intros n hn,

unfold subsucesion at hv,

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

rw hφ2,

apply hN,

apply le_trans hn,

exact aux hφ1 n,

end

-- 2ª demostración

example

(hv : subsucesion v u)

(ha : limite u a)

: limite v a :=

begin

intros ε hε,

cases ha ε hε with N hN,

use N,

intros n hn,

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

rw hφ2,

apply hN,

exact le_trans hn (aux hφ1 n),

end

-- 3ª demostración

example

(hv : subsucesion v u)

(ha : limite u a)

: limite v a :=

begin

intros ε hε,

cases ha ε hε with N hN,

use N,

intros n hn,

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

rw hφ2,

exact hN (φ n) (le_trans hn (aux hφ1 n)),

end

-- 4ª demostración

example

(hv : subsucesion v u)

(ha : limite u a)

: limite v a :=

begin

intros ε hε,

cases ha ε hε with N hN,

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

rw hφ2,

use N,

exact λ n hn, hN (φ n) (le_trans hn (aux hφ1 n)),

end

-- 5ª demostración

example

(hv : subsucesion v u)

(ha : limite u a)

: limite v a :=

begin

intros ε hε,

cases ha ε hε with N hN,

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

rw hφ2,

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

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion
imports Main HOL.Real
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

(* En la demostración se usará el siguiente lema *)
lemma aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed

(* Demostración *)
lemma
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using hφ2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed

end

theory Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion

imports Main HOL.Real

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"

where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

(* En la demostración se usará el siguiente lema *)

lemma aux :

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0" by simp

fix n assume HI : "n ≤ φ n"

then show "Suc n ≤ φ (Suc n)"

using assms extraccion_def

by (metis Suc_leI lessI order_le_less_subst1)

qed

(* Demostración *)

lemma

assumes "subsucesion v u"

"limite u a"

shows "limite v a"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "ε > 0"

then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"

using assms(2) limite_def by auto

obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"

using assms(1) subsucesion_def by auto

have "∀k≥N. ¦v k - a¦ < ε"

proof (intro allI impI)

fix k

assume "N ≤ k"

also have "... ≤ φ k"

by (simp add: aux hφ1)

finally have "N ≤ φ k" .

have "¦v k - a¦ = ¦u (φ k) - a¦"

using hφ2 by simp

also have "… < ε"

using hN ‹N ≤ φ k› by simp

finally show "¦v k - a¦ < ε" .

qed

then show "∃N. ∀k≥N. ¦v k - a¦ < ε"

by auto

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Si a es un punto de acumulación de u, entonces ∀ε>0, ∀ N, ∃k≥N, |u(k)−a| < ε

PorJosé A. Alonso 31 agosto 202125 agosto 2021

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ n m, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

También se puede definir que a es un límite de u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, \|u k - a\| < ε

Los puntos de acumulación de una sucesión son los límites de sus subsucesiones. En Lean se puede definir por

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

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

Demostrar que si a es un punto de acumulación de u, entonces

   ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε

1	∀ ε > 0, ∀ N, ∃ k ≥ N, \|u k - a\| < ε

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

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

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

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

example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε :=
sorry

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=

∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

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

def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

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

-- En la demostración se usarán los siguientes lemas.

lemma aux1
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end

lemma aux2
  (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')
                             (aux1 h (max N N'))⟩⟩

-- 1ª demostración
example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 (aux2 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 (aux2 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 (aux2 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 (aux2 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

import data.real.basic

open nat

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ):=

∀ n m, n < m → φ n < φ m

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

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε

def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=

∃ φ, extraccion φ ∧ limite (u ∘ φ) a

-- En la demostración se usarán los siguientes lemas.

lemma aux1

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intro n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h m (m+1) (lt_add_one m), },

end

lemma aux2

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

(aux1 h (max N N'))⟩⟩

-- 1ª demostración

example

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 aux2 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 (aux2 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 (aux2 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 (aux2 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 (aux2 hφ.1 N N')

(λ m hm, exists.elim hm

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

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory "Si_a_es_un_punto_de_acumulacion_de_u,_entonces_a_tiene_puntos_cercanos"
imports Main HOL.Real
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* En la demostración se usarán los siguientes lemas *)
lemma aux1 :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed

lemma aux2 :
  assumes "extraccion φ"
  shows   "∀ N N'. ∃ k ≥ N'. φ k ≥ N"
proof (intro allI)
  fix N N' :: nat
  have "max N N' ≥ N' ∧ φ (max N N') ≥ N"
    by (meson assms aux1 max.bounded_iff max.cobounded2)
  then show "∃k ≥ N'. φ k ≥ N"
    by blast
qed

(* 1ª demostración *)
lemma
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where hφ1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using hφ2 limite_def ‹ε > 0› by auto
  obtain m where hm1 : "m ≥ N'" and hm2 : "φ m ≥ N"
    using aux2 hφ1 by blast
  have "φ m ≥ N ∧ ¦u (φ m) - a¦ < ε"
    using hN' hm1 hm2 by force
  then show "∃k≥N. ¦u k - a¦ < ε"
    by auto
qed

(* 2ª demostración *)
lemma
  assumes "punto_acumulacion u a"
  shows   "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"
proof (intro allI impI)
  fix ε :: real and N :: nat
  assume "ε > 0"
  obtain φ where hφ1 : "extraccion φ"
             and hφ2 : "limite (u ∘ φ) a"
    using assms punto_acumulacion_def by blast
  obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"
    using hφ2 limite_def ‹ε > 0› by auto
  obtain m where "m ≥ N' ∧ φ m ≥ N"
    using aux2 hφ1 by blast
  then show "∃k≥N. ¦u k - a¦ < ε"
    using hN' by auto
qed

end

theory "Si_a_es_un_punto_de_acumulacion_de_u,_entonces_a_tiene_puntos_cercanos"

imports Main HOL.Real

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"

definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"

where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"

(* En la demostración se usarán los siguientes lemas *)

lemma aux1 :

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0" by simp

fix n assume HI : "n ≤ φ n"

then show "Suc n ≤ φ (Suc n)"

using assms extraccion_def

by (metis Suc_leI lessI order_le_less_subst1)

qed

lemma aux2 :

assumes "extraccion φ"

shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N"

proof (intro allI)

fix N N' :: nat

have "max N N' ≥ N' ∧ φ (max N N') ≥ N"

by (meson assms aux1 max.bounded_iff max.cobounded2)

then show "∃k ≥ N'. φ k ≥ N"

by blast

qed

(* 1ª demostración *)

lemma

assumes "punto_acumulacion u a"

shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"

proof (intro allI impI)

fix ε :: real and N :: nat

assume "ε > 0"

obtain φ where hφ1 : "extraccion φ"

and hφ2 : "limite (u ∘ φ) a"

using assms punto_acumulacion_def by blast

obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"

using hφ2 limite_def ‹ε > 0› by auto

obtain m where hm1 : "m ≥ N'" and hm2 : "φ m ≥ N"

using aux2 hφ1 by blast

have "φ m ≥ N ∧ ¦u (φ m) - a¦ < ε"

using hN' hm1 hm2 by force

then show "∃k≥N. ¦u k - a¦ < ε"

by auto

qed

(* 2ª demostración *)

lemma

assumes "punto_acumulacion u a"

shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε"

proof (intro allI impI)

fix ε :: real and N :: nat

assume "ε > 0"

obtain φ where hφ1 : "extraccion φ"

and hφ2 : "limite (u ∘ φ) a"

using assms punto_acumulacion_def by blast

obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε"

using hφ2 limite_def ‹ε > 0› by auto

obtain m where "m ≥ N' ∧ φ m ≥ N"

using aux2 hφ1 by blast

then show "∃k≥N. ¦u k - a¦ < ε"

using hN' by auto

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las particiones definen relaciones de equivalencia

PorJosé A. Alonso 28 agosto 202123 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada elemento de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

1 2	def particion (P : set (set X)) : Prop := (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar que si P es una partición de X, entonces la relación definida por P es una relación de equivalencia.

Para ello, completar la siguiente teoría de Lean:

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : equivalence (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=

(∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example

(h : particion P)

: equivalence (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : equivalence (relacion P) :=
begin
  repeat { split },
  { intro x,
    rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,
    use [A, ⟨hAP, hxA, hxA⟩], },
  { intros x y hxy,
    rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
    use [B, ⟨hBP, hyB, hxB⟩], },
  { rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
    use B1,
    repeat { split },
    { exact hB1P, },
    { exact hxB1, },
    { convert hzB2,
      rcases (h.1 y) with ⟨B, -, -, hB⟩,
      exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), }},
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=

(∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example

(h : particion P)

: equivalence (relacion P) :=

begin

repeat { split },

{ intro x,

rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,

use [A, ⟨hAP, hxA, hxA⟩], },

{ intros x y hxy,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use [B, ⟨hBP, hyB, hxB⟩], },

{ rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,

use B1,

repeat { split },

{ exact hB1P, },

{ exact hxB1, },

{ convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), }},

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_particiones_definen_relaciones_de_equivalencia
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "equivp (relacion P)"
proof (rule equivpI)
  show "reflp (relacion P)"
  proof (rule reflpI)
    fix x
    obtain A where "A ∈ P ∧ x ∈ A"
      using assms particion_def by metis
    then show "relacion P x x"
      using relacion_def by metis
  qed
next
  show "symp (relacion P)"
  proof (rule sympI)
    fix x y
    assume "relacion P x y"
    then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"
      using relacion_def by metis
    then show "relacion P y x"
      using relacion_def by metis
  qed
next
  show "transp (relacion P)"
  proof (rule transpI)
    fix x y z
    assume "relacion P x y" and "relacion P y z"
    obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
      using ‹relacion P x y› by (meson relacion_def)
    obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
      using ‹relacion P y z› by (meson relacion_def)
    have "A = B"
    proof -
      obtain C where "C ∈ P"
                 and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
        using assms particion_def by metis
      then show "A = B"
        using ‹A ∈ P› ‹B ∈ P› hA hB by blast
    qed
    then have "x ∈ A ∧ z ∈ A"  using hA hB by auto
    then show "relacion P x z"
      using ‹A = B› ‹A ∈ P› relacion_def by metis
  qed
qed

(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "equivp (relacion P)"
proof (rule equivpI)
  show "reflp (relacion P)"
    using assms particion_def relacion_def
    by (metis reflpI)
next
  show "symp (relacion P)"
    using assms relacion_def
    by (metis sympI)
next
  show "transp (relacion P)"
    using assms relacion_def particion_def
    by (smt (verit) transpI)
qed

end

theory Las_particiones_definen_relaciones_de_equivalencia

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where

"particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)

lemma

assumes "particion P"

shows "equivp (relacion P)"

proof (rule equivpI)

show "reflp (relacion P)"

proof (rule reflpI)

fix x

obtain A where "A ∈ P ∧ x ∈ A"

using assms particion_def by metis

then show "relacion P x x"

using relacion_def by metis

qed

show "symp (relacion P)"

proof (rule sympI)

fix x y

assume "relacion P x y"

then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"

using relacion_def by metis

then show "relacion P y x"

using relacion_def by metis

qed

show "transp (relacion P)"

proof (rule transpI)

fix x y z

assume "relacion P x y" and "relacion P y z"

obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"

using ‹relacion P x y› by (meson relacion_def)

obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"

using ‹relacion P y z› by (meson relacion_def)

have "A = B"

proof -

obtain C where "C ∈ P"

and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

using assms particion_def by metis

then show "A = B"

using ‹A ∈ P› ‹B ∈ P› hA hB by blast

qed

then have "x ∈ A ∧ z ∈ A" using hA hB by auto

then show "relacion P x z"

using ‹A = B› ‹A ∈ P› relacion_def by metis

qed

(* 2ª demostración *)

lemma

assumes "particion P"

shows "equivp (relacion P)"

proof (rule equivpI)

show "reflp (relacion P)"

using assms particion_def relacion_def

by (metis reflpI)

show "symp (relacion P)"

using assms relacion_def

by (metis sympI)

show "transp (relacion P)"

using assms relacion_def particion_def

by (smt (verit) transpI)

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las particiones definen relaciones transitivas

PorJosé A. Alonso 27 agosto 202121 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

1 2	def particion (P : set (set X)) : Prop := (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar que si P es una partición de X, entonces la relación definida por P es transitiva.

Para ello, completar la siguiente teoría de Lean:

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : transitive (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=

(∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example

(h : particion P)

: transitive (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

-- 1ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  unfold transitive,
  intros x y z h1 h2,
  unfold relacion at *,
  rcases h1 with ⟨B1, hB1P, hxB1, hyB1⟩,
  rcases h2 with ⟨B2, hB2P, hyB2, hzB2⟩,
  use B1,
  repeat { split },
  { exact hB1P, },
  { exact hxB1, },
  { convert hzB2,
    rcases (h.1 y) with ⟨B, -, -, hB⟩,
    have hBB1 : B = B1 := hB B1 hB1P hyB1,
    have hBB2 : B = B2 := hB B2 hB2P hyB2,
    exact eq.trans hBB1.symm hBB2, },
end

-- 2ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
  use B1,
  repeat { split },
  { exact hB1P, },
  { exact hxB1, },
  { convert hzB2,
    rcases (h.1 y) with ⟨B, -, -, hB⟩,
    exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), },
end

-- 3ª demostración
example
  (h : particion P)
  : transitive (relacion P) :=
begin
  rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,
  use [B1, ⟨hB1P,
            hxB1,
            by { convert hzB2,
                 rcases (h.1 y) with ⟨B, -, -, hB⟩,
                 exact eq.trans (hB B1 hB1P hyB1).symm
                                (hB B2 hB2P hyB2), }⟩],
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=

(∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

-- 1ª demostración

example

(h : particion P)

: transitive (relacion P) :=

begin

unfold transitive,

intros x y z h1 h2,

unfold relacion at *,

rcases h1 with ⟨B1, hB1P, hxB1, hyB1⟩,

rcases h2 with ⟨B2, hB2P, hyB2, hzB2⟩,

use B1,

repeat { split },

{ exact hB1P, },

{ exact hxB1, },

{ convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

have hBB1 : B = B1 := hB B1 hB1P hyB1,

have hBB2 : B = B2 := hB B2 hB2P hyB2,

exact eq.trans hBB1.symm hBB2, },

end

-- 2ª demostración

example

(h : particion P)

: transitive (relacion P) :=

begin

rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,

use B1,

repeat { split },

{ exact hB1P, },

{ exact hxB1, },

{ convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

exact eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2), },

end

-- 3ª demostración

example

(h : particion P)

: transitive (relacion P) :=

begin

rintros x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩,

use [B1, ⟨hB1P,

hxB1,

by { convert hzB2,

rcases (h.1 y) with ⟨B, -, -, hB⟩,

exact eq.trans (hB B1 hB1P hyB1).symm

(hB B2 hB2P hyB2), }⟩],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_particiones_definen_relaciones_transitivas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  have "∃A∈P. x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (simp only: relacion_def)
  then obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    by (rule bexE)
  have "∃B∈P. y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (simp only: relacion_def)
  then obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    by (rule bexE)
  have "A = B"
  proof -
    have "∃C ∈ P. y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms
      by (simp only: particion_def)
    then obtain C where "C ∈ P"
                    and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      by (rule bexE)
    have hC' : "∀D∈P. y ∈ D ⟶ C = D"
      using hC by (rule conjunct2)
    have "C = A"
      using ‹A ∈ P› hA hC' by simp
    moreover have "C = B"
      using ‹B ∈ P› hB hC by simp
    ultimately show "A = B"
      by (rule subst)
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by simp
  then have "∃A∈P. x ∈ A ∧ z ∈ A"
    using ‹A ∈ P› by (rule bexI)
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P›
    by (unfold relacion_def)
qed

(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (meson relacion_def)
  obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (meson relacion_def)
  have "A = B"
  proof -
    obtain C where "C ∈ P" and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms particion_def
      by metis
    have "C = A"
      using ‹A ∈ P› hA hC by auto
    moreover have "C = B"
      using ‹B ∈ P› hB hC by auto
    ultimately show "A = B"
      by simp
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by auto
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P› relacion_def
    by metis
qed

(* 3ª demostración *)
lemma
  assumes "particion P"
  shows   "transp (relacion P)"
  using assms particion_def relacion_def
  by (smt (verit) transpI)

end

theory Las_particiones_definen_relaciones_transitivas

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where

"particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)

lemma

assumes "particion P"

shows "transp (relacion P)"

proof (rule transpI)

fix x y z

assume "relacion P x y" and "relacion P y z"

have "∃A∈P. x ∈ A ∧ y ∈ A"

using ‹relacion P x y›

by (simp only: relacion_def)

then obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"

by (rule bexE)

have "∃B∈P. y ∈ B ∧ z ∈ B"

using ‹relacion P y z›

by (simp only: relacion_def)

then obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"

by (rule bexE)

have "A = B"

proof -

have "∃C ∈ P. y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

using assms

by (simp only: particion_def)

then obtain C where "C ∈ P"

and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

by (rule bexE)

have hC' : "∀D∈P. y ∈ D ⟶ C = D"

using hC by (rule conjunct2)

have "C = A"

using ‹A ∈ P› hA hC' by simp

moreover have "C = B"

using ‹B ∈ P› hB hC by simp

ultimately show "A = B"

by (rule subst)

qed

then have "x ∈ A ∧ z ∈ A"

using hA hB by simp

then have "∃A∈P. x ∈ A ∧ z ∈ A"

using ‹A ∈ P› by (rule bexI)

then show "relacion P x z"

using ‹A = B› ‹A ∈ P›

by (unfold relacion_def)

qed

(* 2ª demostración *)

lemma

assumes "particion P"

shows "transp (relacion P)"

proof (rule transpI)

fix x y z

assume "relacion P x y" and "relacion P y z"

obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"

using ‹relacion P x y›

by (meson relacion_def)

obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"

using ‹relacion P y z›

by (meson relacion_def)

have "A = B"

proof -

obtain C where "C ∈ P" and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"

using assms particion_def

by metis

have "C = A"

using ‹A ∈ P› hA hC by auto

moreover have "C = B"

using ‹B ∈ P› hB hC by auto

ultimately show "A = B"

by simp

qed

then have "x ∈ A ∧ z ∈ A"

using hA hB by auto

then show "relacion P x z"

using ‹A = B› ‹A ∈ P› relacion_def

by metis

qed

(* 3ª demostración *)

lemma

assumes "particion P"

shows "transp (relacion P)"

using assms particion_def relacion_def

by (smt (verit) transpI)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las familias de conjuntos definen relaciones simétricas

PorJosé A. Alonso 26 agosto 202121 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Demostrar que si P es una familia de subconjunt❙os de X, entonces la relación definida por P es simétrica.

Para ello, completar la siguiente teoría de Lean:

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

example : symmetric (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

example : symmetric (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

-- 1ª demostración
example : symmetric (relacion P) :=
begin
  unfold symmetric,
  intros x y hxy,
  unfold relacion at *,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split },
  { exact hBP, },
  { exact hyB, },
  { exact hxB, },
end

-- 2ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use B,
  repeat { split } ;
  assumption,
end

-- 3ª demostración
example : symmetric (relacion P) :=
begin
  intros x y hxy,
  rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,
  use [B, ⟨hBP, hyB, hxB⟩],
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

-- 1ª demostración

example : symmetric (relacion P) :=

begin

unfold symmetric,

intros x y hxy,

unfold relacion at *,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use B,

repeat { split },

{ exact hBP, },

{ exact hyB, },

{ exact hxB, },

end

-- 2ª demostración

example : symmetric (relacion P) :=

begin

intros x y hxy,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use B,

repeat { split } ;

assumption,

end

-- 3ª demostración

example : symmetric (relacion P) :=

begin

intros x y hxy,

rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩,

use [B, ⟨hBP, hyB, hxB⟩],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_familias_de_conjuntos_definen_relaciones_simetricas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

(* 1ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then have "∃A∈P. x ∈ A ∧ y ∈ A"
    by (unfold relacion_def)
  then have "∃A∈P. y ∈ A ∧ x ∈ A"
  proof (rule bexE)
    fix A
    assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A"
    have "y ∈ A ∧ x ∈ A"
      using hA2 by (simp only: conj_commute)
    then show "∃A∈P. y ∈ A ∧ x ∈ A"
      using hA1 by (rule bexI)
  qed
  then show "relacion P y x"
    by (unfold relacion_def)
qed

(* 2ª demostración *)
lemma "symp (relacion P)"
proof (rule sympI)
  fix x y
  assume "relacion P x y"
  then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"
    using relacion_def
    by metis
  then show "relacion P y x"
    using relacion_def
    by metis
qed

(* 3ª demostración *)
lemma "symp (relacion P)"
  using relacion_def
  by (metis sympI)

end

theory Las_familias_de_conjuntos_definen_relaciones_simetricas

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

(* 1ª demostración *)

lemma "symp (relacion P)"

proof (rule sympI)

fix x y

assume "relacion P x y"

then have "∃A∈P. x ∈ A ∧ y ∈ A"

by (unfold relacion_def)

then have "∃A∈P. y ∈ A ∧ x ∈ A"

proof (rule bexE)

fix A

assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A"

have "y ∈ A ∧ x ∈ A"

using hA2 by (simp only: conj_commute)

then show "∃A∈P. y ∈ A ∧ x ∈ A"

using hA1 by (rule bexI)

qed

then show "relacion P y x"

by (unfold relacion_def)

qed

(* 2ª demostración *)

lemma "symp (relacion P)"

proof (rule sympI)

fix x y

assume "relacion P x y"

then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A"

using relacion_def

by metis

then show "relacion P y x"

using relacion_def

by metis

qed

(* 3ª demostración *)

lemma "symp (relacion P)"

using relacion_def

by (metis sympI)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las particiones definen relaciones reflexivas

PorJosé A. Alonso 25 agosto 202119 agosto 2021

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

1 2	def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia de subconjuntos de X es una partición de X si cada elemento de X pertenece a un único conjunto de P y todos los elementos de P son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

1 2	def particion (P : set (set X)) : Prop := (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar que si P es una partición de X, entonces la relación definida por P es reflexiva.

Para ello, completar la siguiente teoría de Lean:

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : reflexive (relacion P) :=
sorry

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=

(∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example

(h : particion P)

: reflexive (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {X : Type}
variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

-- 1ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  unfold reflexive,
  intro x,
  unfold relacion,
  unfold particion at h,
  replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,
  rcases h with ⟨A, hAP, hxA, -⟩,
  use A,
  repeat { split },
  { exact hAP, },
  { exact hxA, },
  { exact hxA, },
end

-- 2ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  intro x,
  replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,
  rcases h with ⟨A, hAP, hxA, -⟩,
  use A,
  repeat { split } ; assumption,
end

-- 3ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  intro x,
  rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,
  use A,
  repeat { split } ; assumption,
end

-- 4ª demostración
example
  (h : particion P)
  : reflexive (relacion P) :=
begin
  intro x,
  rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,
  use [A, ⟨hAP, hxA, hxA⟩],
end

import tactic

variable {X : Type}

variable (P : set (set X))

def relacion (P : set (set X)) (x y : X) :=

∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : set (set X)) : Prop :=

(∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

-- 1ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

unfold reflexive,

intro x,

unfold relacion,

unfold particion at h,

replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,

rcases h with ⟨A, hAP, hxA, -⟩,

use A,

repeat { split },

{ exact hAP, },

{ exact hxA, },

end

-- 2ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

intro x,

replace h : ∃ A ∈ P, x ∈ A ∧ ∀ B ∈ P, x ∈ B → A = B := h.1 x,

rcases h with ⟨A, hAP, hxA, -⟩,

use A,

repeat { split } ; assumption,

end

-- 3ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

intro x,

rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,

use A,

repeat { split } ; assumption,

end

-- 4ª demostración

example

(h : particion P)

: reflexive (relacion P) :=

begin

intro x,

rcases (h.1 x) with ⟨A, hAP, hxA, -⟩,

use [A, ⟨hAP, hxA, hxA⟩],

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_particiones_definen_relaciones_reflexivas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

ru(* 1ª demostración *)
lemma
  assumes "particion P"
  shows   "reflp (relacion P)"
proof (rule reflpI)
  fix x
  have "(∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"
    using assms by (unfold particion_def)
  then have "∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"
    by (rule conjunct1)
  then have "∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C)"
    by (rule allE)
  then obtain B where "B ∈ P ∧ (x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"
    by (rule someI2_bex)
  then obtain B where "(B ∈ P ∧ x ∈ B) ∧ (∀C∈P. x ∈ C ⟶ B = C)"
    by (simp only: conj_assoc)
  then have "B ∈ P ∧ x ∈ B"
    by (rule conjunct1)
  then have "x ∈ B"
    by (rule conjunct2)
  then have "x ∈ B ∧ x ∈ B"
    using ‹x ∈ B› by (rule conjI)
  moreover have "B ∈ P"
    using ‹B ∈ P ∧ x ∈ B› by (rule conjunct1)
  ultimately have "∃B∈P. x ∈ B ∧ x ∈ B"
    by (rule bexI)
  then show "relacion P x x"
    by (unfold relacion_def)
qed

(* 2ª demostración *)
lemma
  assumes "particion P"
  shows   "reflp (relacion P)"
proof (rule reflpI)
  fix x
  obtain A where "A ∈ P ∧ x ∈ A"
    using assms particion_def
    by metis
  then show "relacion P x x"
    using relacion_def
    by metis
qed

(* 3ª demostración *)
lemma
  assumes "particion P"
  shows   "reflp (relacion P)"
  using assms particion_def relacion_def
  by (metis reflp_def)

end

theory Las_particiones_definen_relaciones_reflexivas

imports Main

begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where

"relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where

"particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

ru(* 1ª demostración *)

lemma

assumes "particion P"

shows "reflp (relacion P)"

proof (rule reflpI)

fix x

have "(∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

using assms by (unfold particion_def)

then have "∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"

by (rule conjunct1)

then have "∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C)"

by (rule allE)

then obtain B where "B ∈ P ∧ (x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))"

by (rule someI2_bex)

then obtain B where "(B ∈ P ∧ x ∈ B) ∧ (∀C∈P. x ∈ C ⟶ B = C)"

by (simp only: conj_assoc)

then have "B ∈ P ∧ x ∈ B"

by (rule conjunct1)

then have "x ∈ B"

by (rule conjunct2)

then have "x ∈ B ∧ x ∈ B"

using ‹x ∈ B› by (rule conjI)

moreover have "B ∈ P"

using ‹B ∈ P ∧ x ∈ B› by (rule conjunct1)

ultimately have "∃B∈P. x ∈ B ∧ x ∈ B"

by (rule bexI)

then show "relacion P x x"

by (unfold relacion_def)

qed

(* 2ª demostración *)

lemma

assumes "particion P"

shows "reflp (relacion P)"

proof (rule reflpI)

fix x

obtain A where "A ∈ P ∧ x ∈ A"

using assms particion_def

by metis

then show "relacion P x x"

using relacion_def

by metis

qed

(* 3ª demostración *)

lemma

assumes "particion P"

shows "reflp (relacion P)"

using assms particion_def relacion_def

by (metis reflp_def)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Las clases de equivalencia de elementos no relacionados son disjuntas

PorJosé A. Alonso 23 agosto 202121 agosto 2021

Demostrar que las clases de equivalencia de elementos no relacionados son disjuntas.

Para ello, completar la siguiente teoría de Lean:

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
sorry

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

-- 1ª demostración
example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
begin
  rcases h with ⟨hr, hs, ht⟩,
  by_contradiction h1,
  apply hxy,
  have h2 : ∃ z, z ∈ clase R x ∩ clase R y,
    { contrapose h1,
      intro h1a,
      apply h1a,
      push_neg at h1,
      exact set.eq_empty_iff_forall_not_mem.mpr h1, },
  rcases h2 with ⟨z, hxz, hyz⟩,
  replace hxz : R x z := hxz,
  replace hyz : R y z := hyz,
  have hzy : R z y := hs hyz,
  exact ht hxz hzy,
end

-- 2ª demostración
example
  (h : equivalence R)
  (hxy : ¬ R x y)
  : clase R x ∩ clase R y = ∅ :=
begin
  rcases h with ⟨hr, hs, ht⟩,
  by_contradiction h1,
  have h2 : ∃ z, z ∈ clase R x ∩ clase R y,
    { by finish [set.eq_empty_iff_forall_not_mem]},
  apply hxy,
  rcases h2 with ⟨z, hxz, hyz⟩,
  exact ht hxz (hs hyz),
end

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

-- 1ª demostración

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

begin

rcases h with ⟨hr, hs, ht⟩,

by_contradiction h1,

apply hxy,

have h2 : ∃ z, z ∈ clase R x ∩ clase R y,

{ contrapose h1,

intro h1a,

apply h1a,

push_neg at h1,

exact set.eq_empty_iff_forall_not_mem.mpr h1, },

rcases h2 with ⟨z, hxz, hyz⟩,

replace hxz : R x z := hxz,

replace hyz : R y z := hyz,

have hzy : R z y := hs hyz,

exact ht hxz hzy,

end

-- 2ª demostración

example

(h : equivalence R)

(hxy : ¬ R x y)

: clase R x ∩ clase R y = ∅ :=

begin

rcases h with ⟨hr, hs, ht⟩,

by_contradiction h1,

have h2 : ∃ z, z ∈ clase R x ∩ clase R y,

{ by finish [set.eq_empty_iff_forall_not_mem]},

apply hxy,

rcases h2 with ⟨z, hxz, hyz⟩,

exact ht hxz (hs hyz),

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Las_clases_de_equivalencia_de_elementos_no_relacionados_son_disjuntas
imports Main
begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"
  where "clase R x = {y. R x y}"

(* 1ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
proof -
  have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"
  proof (intro allI impI)
    fix z
    assume "z ∈ clase R x"
    then have "R x z"
      using clase_def by (metis CollectD)
    show "z ∉ clase R y"
    proof (rule notI)
      assume "z ∈ clase R y"
      then have "R y z"
        using clase_def by (metis CollectD)
      then have "R z y"
        using assms(1) by (simp only: equivp_symp)
      with ‹R x z› have "R x y"
        using assms(1) by (simp only: equivp_transp)
      with ‹¬R x y› show False
        by (rule notE)
    qed
  qed
  then show "clase R x ∩ clase R y = {}"
    by (simp only: disjoint_iff)
qed

(* 2ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
proof -
  have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"
  proof (intro allI impI)
    fix z
    assume "z ∈ clase R x"
    then have "R x z"
      using clase_def by fastforce
    show "z ∉ clase R y"
    proof (rule notI)
      assume "z ∈ clase R y"
      then have "R y z"
        using clase_def by fastforce
      then have "R z y"
        using assms(1) by (simp only: equivp_symp)
      with ‹R x z› have "R x y"
        using assms(1) by (simp only: equivp_transp)
      with ‹¬R x y› show False
        by simp
    qed
  qed
  then show "clase R x ∩ clase R y = {}"
    by (simp only: disjoint_iff)
qed

(* 3ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
  using assms
  by (metis clase_def
            CollectD
            equivp_symp
            equivp_transp
            disjoint_iff)

(* 4ª demostración *)
lemma
  assumes "equivp R"
          "¬(R x y)"
  shows "clase R x ∩ clase R y = {}"
  using assms
  by (metis equivp_def
            clase_def
            CollectD
            disjoint_iff_not_equal)

end

theory Las_clases_de_equivalencia_de_elementos_no_relacionados_son_disjuntas

imports Main

begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"

where "clase R x = {y. R x y}"

(* 1ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

proof -

have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"

proof (intro allI impI)

fix z

assume "z ∈ clase R x"

then have "R x z"

using clase_def by (metis CollectD)

show "z ∉ clase R y"

proof (rule notI)

assume "z ∈ clase R y"

then have "R y z"

using clase_def by (metis CollectD)

then have "R z y"

using assms(1) by (simp only: equivp_symp)

with ‹R x z› have "R x y"

using assms(1) by (simp only: equivp_transp)

with ‹¬R x y› show False

by (rule notE)

qed

then show "clase R x ∩ clase R y = {}"

by (simp only: disjoint_iff)

qed

(* 2ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

proof -

have "∀z. z ∈ clase R x ⟶ z ∉ clase R y"

proof (intro allI impI)

fix z

assume "z ∈ clase R x"

then have "R x z"

using clase_def by fastforce

show "z ∉ clase R y"

proof (rule notI)

assume "z ∈ clase R y"

then have "R y z"

using clase_def by fastforce

then have "R z y"

using assms(1) by (simp only: equivp_symp)

with ‹R x z› have "R x y"

using assms(1) by (simp only: equivp_transp)

with ‹¬R x y› show False

by simp

qed

then show "clase R x ∩ clase R y = {}"

by (simp only: disjoint_iff)

qed

(* 3ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

using assms

by (metis clase_def

CollectD

equivp_symp

equivp_transp

disjoint_iff)

(* 4ª demostración *)

lemma

assumes "equivp R"

"¬(R x y)"

shows "clase R x ∩ clase R y = {}"

using assms

by (metis equivp_def

clase_def

CollectD

disjoint_iff_not_equal)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]