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:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 |
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»]
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 44 45 46 47 48 49 |
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]