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:
1 2 3 4 5 6 7 8 9 10 11 12 13 |
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 |
[expand title=»Soluciones con Lean»]
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 |
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>
[/expand]