Menu Close

Día: 6 octubre 2021

Las clases de equivalencia recubren el conjunto

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.

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.

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

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