L.le_antisymm – Calculemus

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]

El conjunto de las clases de equivalencia es una partición

PorJosé A. Alonso 24 agosto 202121 agosto 2021

Demostrar que si R es una relación de equivalencia en X, entonces las clases de equivalencia de R es una partición de X.

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}

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

example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
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}

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

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

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

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}

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

lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz

-- 1ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        apply le_antisymm,
        { exact aux h hx, },
        { exact aux h (h.2.1 hx), }}}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

-- 2ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end

-- 3ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use [clase R y,
         ⟨by use y,
          ⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
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}

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

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

lemma aux

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

λ z hz, h.2.2 hxy hz

-- 1ª demostración

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

begin

split,

{ simp,

intro y,

use (clase R y),

split,

{ use y, },

{ split,

{ exact h.1 y, },

{ intros x hx,

apply le_antisymm,

{ exact aux h hx, },

{ exact aux h (h.2.1 hx), }}}},

{ simp,

intros x hx,

have h1 : x ∈ clase R x := h.1 x,

rw ← hx at h1,

exact set.not_mem_empty x h1, },

end

-- 2ª demostración

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

begin

split,

{ simp,

intro y,

use (clase R y),

split,

{ use y, },

{ split,

{ exact h.1 y, },

{ intros x hx,

exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},

{ simp,

intros x hx,

have h1 : x ∈ clase R x := h.1 x,

rw ← hx at h1,

exact set.not_mem_empty x h1, },

end

-- 3ª demostración

example

(h : equivalence R)

: particion {a : set X | ∃ s : X, a = clase R s} :=

begin

split,

{ simp,

intro y,

use [clase R y,

⟨by use y,

⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },

{ simp,

intros x hx,

have h1 : x ∈ clase R x := h.1 x,

rw ← hx at h1,

exact set.not_mem_empty x h1, },

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_conjunto_de_las_clases_de_equivalencia_es_una_particion
imports Main
begin

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

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

lemma
  fixes   R :: "'a ⇒ 'a ⇒ bool"
  assumes "equivp R"
  shows   "particion (⋃x. {clase R x})" (is "particion ?P")
proof (unfold particion_def; intro conjI)
  show "(∀x. ∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C))"
  proof (intro allI)
    fix x
    have "clase R x ∈ ?P"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    moreover have "∀C∈?P. x ∈ C ⟶ clase R x = C"
    proof
      fix C
      assume "C ∈ ?P"
      then obtain y where "C = clase R y"
        by auto
      show "x ∈ C ⟶ clase R x = C"
      proof
        assume "x ∈ C"
        then have "R y x"
          using ‹C = clase R y› assms clase_def
          by (metis CollectD)
        then show "clase R x = C"
          using assms ‹C = clase R y› clase_def equivp_def
          by metis
      qed
    qed
    ultimately show "∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C)"
      by blast
  qed
next
  show "{} ∉ ?P"
  proof
    assume "{} ∈ ?P"
    then obtain x where "{} = clase R x"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    ultimately show False
      by simp
  qed
qed

end

theory El_conjunto_de_las_clases_de_equivalencia_es_una_particion

imports Main

begin

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

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

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

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

lemma

fixes R :: "'a ⇒ 'a ⇒ bool"

assumes "equivp R"

shows "particion (⋃x. {clase R x})" (is "particion ?P")

proof (unfold particion_def; intro conjI)

show "(∀x. ∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C))"

proof (intro allI)

fix x

have "clase R x ∈ ?P"

by auto

moreover have "x ∈ clase R x"

using assms clase_def equivp_def

by (metis CollectI)

moreover have "∀C∈?P. x ∈ C ⟶ clase R x = C"

proof

fix C

assume "C ∈ ?P"

then obtain y where "C = clase R y"

by auto

show "x ∈ C ⟶ clase R x = C"

proof

assume "x ∈ C"

then have "R y x"

using ‹C = clase R y› assms clase_def

by (metis CollectD)

then show "clase R x = C"

using assms ‹C = clase R y› clase_def equivp_def

by metis

qed

ultimately show "∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C)"

by blast

qed

show "{} ∉ ?P"

proof

assume "{} ∈ ?P"

then obtain x where "{} = clase R x"

by auto

moreover have "x ∈ clase R x"

using assms clase_def equivp_def

by (metis CollectI)

ultimately show False

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 clases de equivalencia de elementos relacionados son iguales

PorJosé A. Alonso 22 agosto 202121 agosto 2021

Demostrar que las clases de equivalencia de elementos relacionados son iguales.

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}

-- En la demostración se usará el siguiente lema del que se presentan
-- varias demostraciones.

-- 1ª demostración del lema auxiliar
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
begin
  intros z hz,
  have hyz : R y z := hz,
  have htrans : transitive R := h.2.2,
  have hxz : R x z := htrans hxy hyz,
  exact hxz,
end

-- 2ª demostración del lema auxiliar
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
begin
  intros z hz,
  exact h.2.2 hxy hz,
end

-- 3ª demostración del lema auxiliar
lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz

-- A continuación se presentan varias demostraciones del ejercicio
-- usando el lema auxiliar

-- 1ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
begin
  apply le_antisymm,
  { have hs : symmetric R := h.2.1,
    have hyx : R y x := hs hxy,
    exact aux h hyx, },
  { exact aux h hxy, },
end

-- 2ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
begin
  apply le_antisymm,
  { exact aux h (h.2.1 hxy), },
  { exact aux h hxy, },
end

-- 3ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
le_antisymm (aux h (h.2.1 hxy)) (aux h hxy)

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}

-- En la demostración se usará el siguiente lema del que se presentan

-- varias demostraciones.

-- 1ª demostración del lema auxiliar

example

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

begin

intros z hz,

have hyz : R y z := hz,

have htrans : transitive R := h.2.2,

have hxz : R x z := htrans hxy hyz,

exact hxz,

end

-- 2ª demostración del lema auxiliar

example

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

begin

intros z hz,

exact h.2.2 hxy hz,

end

-- 3ª demostración del lema auxiliar

lemma aux

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

λ z hz, h.2.2 hxy hz

-- A continuación se presentan varias demostraciones del ejercicio

-- usando el lema auxiliar

-- 1ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

begin

apply le_antisymm,

{ have hs : symmetric R := h.2.1,

have hyx : R y x := hs hxy,

exact aux h hyx, },

{ exact aux h hxy, },

end

-- 2ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

begin

apply le_antisymm,

{ exact aux h (h.2.1 hxy), },

{ exact aux h hxy, },

end

-- 3ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

le_antisymm (aux h (h.2.1 hxy)) (aux h hxy)

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_relacionados_son_iguales
imports Main
begin

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

(* En la demostración se usará el siguiente lema del que se presentan
   varias demostraciones. *)

(* 1ª demostración del lema auxiliar *)
lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y ⊆ clase R x"
proof (rule subsetI)
  fix z
  assume "z ∈ clase R y"
  then have "R y z"
    by (simp add: clase_def)
  have "transp R"
    using assms(1) by (rule equivp_imp_transp)
  then have "R x z"
    using ‹R x y› ‹R y z› by (rule transpD)
  then show "z ∈ clase R x"
    by (simp add: clase_def)
qed

(* 2ª demostración del lema auxiliar *)
lemma aux :
  assumes "equivp R"
          "R x y"
  shows "clase R y ⊆ clase R x"
  using assms
  by (metis clase_def eq_refl equivp_def)

(* A continuación se presentan demostraciones del ejercicio *)

(* 1ª demostración *)
lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y = clase R x"
proof (rule equalityI)
  show "clase R y ⊆ clase R x"
    using assms by (rule aux)
next
  show "clase R x ⊆ clase R y"
  proof -
    have "symp R"
      using assms(1) equivpE by blast
    have "R y x"
      using ‹R x y› by (simp add: ‹symp R› sympD)
    with assms(1) show "clase R x ⊆ clase R y"
       by (rule aux)
  qed
qed

(* 2ª demostración *)
lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y = clase R x"
  using assms
  by (metis clase_def equivp_def)

end

theory Las_clases_de_equivalencia_de_elementos_relacionados_son_iguales

imports Main

begin

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

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

(* En la demostración se usará el siguiente lema del que se presentan

varias demostraciones. *)

(* 1ª demostración del lema auxiliar *)

lemma

assumes "equivp R"

"R x y"

shows "clase R y ⊆ clase R x"

proof (rule subsetI)

fix z

assume "z ∈ clase R y"

then have "R y z"

by (simp add: clase_def)

have "transp R"

using assms(1) by (rule equivp_imp_transp)

then have "R x z"

using ‹R x y› ‹R y z› by (rule transpD)

then show "z ∈ clase R x"

by (simp add: clase_def)

qed

(* 2ª demostración del lema auxiliar *)

lemma aux :

assumes "equivp R"

"R x y"

shows "clase R y ⊆ clase R x"

using assms

by (metis clase_def eq_refl equivp_def)

(* A continuación se presentan demostraciones del ejercicio *)

(* 1ª demostración *)

lemma

assumes "equivp R"

"R x y"

shows "clase R y = clase R x"

proof (rule equalityI)

show "clase R y ⊆ clase R x"

using assms by (rule aux)

show "clase R x ⊆ clase R y"

proof -

have "symp R"

using assms(1) equivpE by blast

have "R y x"

using ‹R x y› by (simp add: ‹symp R› sympD)

with assms(1) show "clase R x ⊆ clase R y"

by (rule aux)

qed

(* 2ª demostración *)

lemma

assumes "equivp R"

"R x y"

shows "clase R y = clase R x"

using assms

by (metis clase_def equivp_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]