octubre 2021 – Página 2

Las relaciones definidas por particiones son simétricas

PorJosé A. Alonso 10 octubre 20213 octubre 2021

Este ejercicio es el 11º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.

Demostrar que la relación definida por una partición es simétrica.

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

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example
  (P : particion A)
  : symmetric (relacion P) :=
sorry

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example

(P : particion A)

: symmetric (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- Se usarán los siguientes lemas auxiliares

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

-- 1ª demostración
example
  (P : particion A)
  : symmetric (relacion P) :=
begin
  rw symmetric,
  intros a b hab,
  unfold relacion at *,
  intros X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize hab Y hY haY,
  exact pertenece_si_pertenece hY hX hab hbX haY,
end

-- 2ª demostración
example
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b hab,
  intros X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize hab Y hY haY,
  exact pertenece_si_pertenece hY hX hab hbX haY,
end

-- 3ª demostración
lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- Se usarán los siguientes lemas auxiliares

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

-- 1ª demostración

example

(P : particion A)

: symmetric (relacion P) :=

begin

rw symmetric,

intros a b hab,

unfold relacion at *,

intros X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize hab Y hY haY,

exact pertenece_si_pertenece hY hX hab hbX haY,

end

-- 2ª demostración

example

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b hab,

intros X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize hab Y hY haY,

exact pertenece_si_pertenece hY hX hab hbX haY,

end

-- 3ª demostración

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

end particion

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]

Las relaciones definidas por particiones son reflexivas

PorJosé A. Alonso 9 octubre 20213 octubre 2021

Este ejercicio es el 10º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Para cada partición se define una relación de forma que un par de elementos están relacionados si pertenecen al mismo bloque de la partición. En Lean,

   def relacion : (particion A) → (A → A → Prop) :=
     λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

1 2	def relacion : (particion A) → (A → A → Prop) := λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

Demostrar que la relación definida por la partición P es reflexiva.

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

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

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

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example

(P : particion A)

: reflexive (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- 1ª demostración
example
  (P : particion A)
  : reflexive (relacion P) :=
begin
  rw reflexive,
  intro a,
  unfold relacion,
  intros X hXC haX,
  exact haX,
end

-- 2ª demostración
example
  (P : particion A)
  : reflexive (relacion P) :=
begin
  intro a,
  intros X hXC haX,
  exact haX,
end

-- 3ª demostración
example
  (P : particion A)
  : reflexive (relacion P) :=
begin
  intros a X hXC haX,
  exact haX,
end

-- 4ª demostración
lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- 1ª demostración

example

(P : particion A)

: reflexive (relacion P) :=

begin

rw reflexive,

intro a,

unfold relacion,

intros X hXC haX,

exact haX,

end

-- 2ª demostración

example

(P : particion A)

: reflexive (relacion P) :=

begin

intro a,

intros X hXC haX,

exact haX,

end

-- 3ª demostración

example

(P : particion A)

: reflexive (relacion P) :=

begin

intros a X hXC haX,

exact haX,

end

-- 4ª demostración

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

end particion

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]

El cociente aplica relaciones de equivalencia en particiones

PorJosé A. Alonso 8 octubre 20212 octubre 2021

Este ejercicio es el 9º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

El ejercicio consiste en definir la función

   cociente : {R : A → A → Prop // equivalence R} → particion A

1	cociente : {R : A → A → Prop // equivalence R} → particion A

tal que cociente R es la partición de A formada por las clases de equivalencia de la relación de equivalencia R.

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

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}
variable  (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
sorry

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}
variable  (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

lemma clases_recubren
  (hR: equivalence R)
  : ∀ a, ∃ X ∈ clases R, a ∈ X :=
begin
  intro a,
  use clase R a,
  split,
  { use a, },
  { exact hR.1 a, },
end

lemma subclase_si_pertenece
  {R : A → A → Prop}
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
λ hab z hza, hR.2.2 hza hab

lemma clases_iguales_si_pertenece
  {R : A → A → Prop}
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a = clase R b :=
λ hab, set.subset.antisymm
        (subclase_si_pertenece hR hab)
        (subclase_si_pertenece hR (hR.2.1 hab))

lemma clases_disjuntas
  (hR: equivalence R)
  : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
begin
  rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,
  exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),
end

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

lemma clases_recubren

(hR: equivalence R)

: ∀ a, ∃ X ∈ clases R, a ∈ X :=

begin

intro a,

use clase R a,

split,

{ use a, },

{ exact hR.1 a, },

end

lemma subclase_si_pertenece

{R : A → A → Prop}

(hR: equivalence R)

{a b : A}

: a ∈ clase R b → clase R a ⊆ clase R b :=

λ hab z hza, hR.2.2 hza hab

lemma clases_iguales_si_pertenece

{R : A → A → Prop}

(hR: equivalence R)

{a b : A}

: a ∈ clase R b → clase R a = clase R b :=

λ hab, set.subset.antisymm

(subclase_si_pertenece hR hab)

(subclase_si_pertenece hR (hR.2.1 hab))

lemma clases_disjuntas

(hR: equivalence R)

: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=

begin

rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,

exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),

end

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

end particion

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]

Las clases de equivalencia son disjuntas

PorJosé A. Alonso 7 octubre 20212 octubre 2021

Este ejercicio es el 8º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

El ejercicio consiste en demostrar que si R es una relación de equivalencia en A, entonces las clases de equivalencia de R son disjuntas.

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

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

example
  (hR: equivalence R)
  : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
sorry

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

example

(hR: equivalence R)

: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

-- Se usarán los dos siguientes lemas auxiliares
lemma subclase_si_pertenece
  {R : A → A → Prop}
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a ⊆ clase R b :=
λ hab z hza, hR.2.2 hza hab

lemma clases_iguales_si_pertenece
  {R : A → A → Prop}
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b → clase R a = clase R b :=
λ hab, set.subset.antisymm
        (subclase_si_pertenece hR hab)
        (subclase_si_pertenece hR (hR.2.1 hab))

-- 1ª demostración
example
  (hR: equivalence R)
  : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
begin
  intros X Y hX hY hXY,
  unfold clases at hX hY,
  dsimp at hX hY,
  cases hX with a ha,
  cases hY with b hb,
  rw [ha, hb] at *,
  rw set.nonempty_def at hXY,
  cases hXY with c hc,
  cases hc with hca hcb,
  apply clases_iguales_si_pertenece hR,
  apply hR.2.2 _ hcb,
  apply hR.2.1,
  exact hca,
end

-- 2ª demostración
example
  (hR: equivalence R)
  : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
begin
  intros X Y hX hY hXY,
  cases hX with a ha,
  cases hY with b hb,
  rw [ha, hb] at *,
  rw set.nonempty_def at hXY,
  cases hXY with c hc,
  cases hc with hca hcb,
  apply clases_iguales_si_pertenece hR,
  apply hR.2.2 _ hcb,
  apply hR.2.1,
  exact hca,
end

-- 3ª demostración
example
  (hR: equivalence R)
  : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
begin
  rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,
  apply clases_iguales_si_pertenece hR,
  apply hR.2.2 _ hcb,
  apply hR.2.1,
  exact hca,
end

-- 4ª demostración
lemma clases_disjuntas
  (hR: equivalence R)
  : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=
begin
  rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,
  exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),
end

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

-- Se usarán los dos siguientes lemas auxiliares

lemma subclase_si_pertenece

{R : A → A → Prop}

(hR: equivalence R)

{a b : A}

: a ∈ clase R b → clase R a ⊆ clase R b :=

λ hab z hza, hR.2.2 hza hab

lemma clases_iguales_si_pertenece

{R : A → A → Prop}

(hR: equivalence R)

{a b : A}

: a ∈ clase R b → clase R a = clase R b :=

λ hab, set.subset.antisymm

(subclase_si_pertenece hR hab)

(subclase_si_pertenece hR (hR.2.1 hab))

-- 1ª demostración

example

(hR: equivalence R)

: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=

begin

intros X Y hX hY hXY,

unfold clases at hX hY,

dsimp at hX hY,

cases hX with a ha,

cases hY with b hb,

rw [ha, hb] at *,

rw set.nonempty_def at hXY,

cases hXY with c hc,

cases hc with hca hcb,

apply clases_iguales_si_pertenece hR,

apply hR.2.2 _ hcb,

apply hR.2.1,

exact hca,

end

-- 2ª demostración

example

(hR: equivalence R)

: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=

begin

intros X Y hX hY hXY,

cases hX with a ha,

cases hY with b hb,

rw [ha, hb] at *,

rw set.nonempty_def at hXY,

cases hXY with c hc,

cases hc with hca hcb,

apply clases_iguales_si_pertenece hR,

apply hR.2.2 _ hcb,

apply hR.2.1,

exact hca,

end

-- 3ª demostración

example

(hR: equivalence R)

: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=

begin

rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,

apply clases_iguales_si_pertenece hR,

apply hR.2.2 _ hcb,

apply hR.2.1,

exact hca,

end

-- 4ª demostración

lemma clases_disjuntas

(hR: equivalence R)

: ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y :=

begin

rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,

exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),

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]

Las clases de equivalencia recubren el conjunto

PorJosé A. Alonso 6 octubre 20212 octubre 2021

Este ejercicio es el 7º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

El ejercicio consiste en demostrar que si R es una relación de equivalencia en A, entonces las clases de equivalencia de R recubren a A.

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

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

example
  (hR: equivalence R)
  : ∀ a, ∃ X ∈ clases R, a ∈ X :=
sorry

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

example

(hR: equivalence R)

: ∀ a, ∃ X ∈ clases R, a ∈ X :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable {A : Type}
variable (R : A → A → Prop)

def clase (a : A) :=
  {b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=
  λ R, {B : set A | ∃ x : A, B = clase R x}

-- Se usarán los dos siguientes lemas auxiliares
lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma pertenece_clase_propia
  {R : A → A → Prop}
  (hR: equivalence R)
  (a : A)
  : a ∈ clase R a :=
(pertenece_clase_syss R).mpr (hR.1 a)

-- 1ª demostración,
example
  (hR: equivalence R)
  : ∀ a, ∃ X ∈ clases R, a ∈ X :=
begin
  intro a,
  use clase R a,
  split,
  { unfold clases,
    dsimp,
    use a, },
  { exact pertenece_clase_propia hR a, },
end

-- 2ª demostración,
lemma clases_recubren
  (hR: equivalence R)
  : ∀ a, ∃ X ∈ clases R, a ∈ X :=
begin
  intro a,
  use clase R a,
  split,
  { use a, },
  { exact hR.1 a, },
end

import tactic

variable {A : Type}

variable (R : A → A → Prop)

def clase (a : A) :=

{b : A | R b a}

def clases : (A → A → Prop) → set (set A) :=

λ R, {B : set A | ∃ x : A, B = clase R x}

-- Se usarán los dos siguientes lemas auxiliares

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma pertenece_clase_propia

{R : A → A → Prop}

(hR: equivalence R)

(a : A)

: a ∈ clase R a :=

(pertenece_clase_syss R).mpr (hR.1 a)

-- 1ª demostración,

example

(hR: equivalence R)

: ∀ a, ∃ X ∈ clases R, a ∈ X :=

begin

intro a,

use clase R a,

split,

{ unfold clases,

dsimp,

use a, },

{ exact pertenece_clase_propia hR a, },

end

-- 2ª demostración,

lemma clases_recubren

(hR: equivalence R)

: ∀ a, ∃ X ∈ clases R, a ∈ X :=

begin

intro a,

use clase R a,

split,

{ use a, },

{ exact hR.1 a, },

end

Se puede interactuar con la prueba anterior en esta sesión con Lean.
[/expand]