Menu Close

Día: 3 octubre 2021

Las clases de equivalencia contienen a las clases de equivalencia de sus elementos

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

El ejercicio consiste en demostrar que si C es una clase de equivalencia y a ∈ C, entonces la clase de equivalencia de a está contenida en 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á el siguiente lema auxiliar
lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a  R b a :=
by refl
 
-- 1ª demostración
example
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b  clase R a ⊆ clase R b :=
begin
  intro hab,
  intros z hza,
  rw pertenece_clase_syss at hab hza ⊢,
  obtain ⟨-, -, htrans⟩ := hR,
  exact htrans hza hab,
end
 
-- 2ª demostración
example
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b  clase R a ⊆ clase R b :=
begin
  intros hab z hza,
  exact hR.2.2 hza hab,
end
 
-- 3ª demostración
lemma subclase_si_pertenece
  {hR: equivalence R}
  {a b : A}
  : a ∈ clase R b  clase R a ⊆ clase R b :=
λ hab z hza, hR.2.2 hza 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>