Menu Close

Día: 4 octubre 2021

Las clases de equivalencia son iguales a las de sus elementos

Este ejercicio es el 5º 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.

El ejercicio consiste en demostrar que si C es una clase de equivalencia y a ∈ C, entonces la clase de equivalencia de a es C.

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}
 
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b  clase R a = clase R b :=
sorry
Soluciones con Lean
import tactic
 
variable {A : Type}
variable (R : A  A  Prop)
 
def clase (a : A) :=
  {b : A | R b a}
 
-- Se usarán los siguientes dos lemas auxiliares
lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a  R b a :=
by refl
 
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
 
-- 1ª demostración
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b  clase R a = clase R b :=
begin
  intro hab,
  apply set.subset.antisymm,
  { apply subclase_si_pertenece hR hab, },
  { apply subclase_si_pertenece hR,
    rcases hR with-, hsymm, -⟩,
    exact hsymm hab }
end
 
-- 2ª demostración
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b  clase R a = clase R b :=
begin
  intro hab,
  apply set.subset.antisymm,
  { exact subclase_si_pertenece hR hab, },
  { exact subclase_si_pertenece hR (hR.2.1 hab), }
end
 
-- 3ª demostración
example
  (hR: equivalence R)
  {a b : A}
  : a ∈ clase R b  clase R a = clase R b :=
begin
  intro hab,
  exact set.subset.antisymm
         (subclase_si_pertenece hR hab)
         (subclase_si_pertenece hR (hR.2.1 hab))
end
 
-- 4ª demostración
lemma clases_iguales_si_pertenece
  (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))

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>