Las clases de equivalencia son disjuntas
Este ejercicio es el 8º 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.
7. Las clases de equivalencia recubren el conjunto.
El ejercicio consiste en demostrar que si R es una relación de equivalencia en A, entonces las clases de equivalencia de R son disjuntas.
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) : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y := 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 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 |
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 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 lemma clases_iguales_si_pertenece {R : A → A → Prop} (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)) -- 1ª demostración example (hR: equivalence R) : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y := begin intros X Y hX hY hXY, unfold clases at hX hY, dsimp at hX hY, cases hX with a ha, cases hY with b hb, rw [ha, hb] at *, rw set.nonempty_def at hXY, cases hXY with c hc, cases hc with hca hcb, apply clases_iguales_si_pertenece hR, apply hR.2.2 _ hcb, apply hR.2.1, exact hca, end -- 2ª demostración example (hR: equivalence R) : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y := begin intros X Y hX hY hXY, cases hX with a ha, cases hY with b hb, rw [ha, hb] at *, rw set.nonempty_def at hXY, cases hXY with c hc, cases hc with hca hcb, apply clases_iguales_si_pertenece hR, apply hR.2.2 _ hcb, apply hR.2.1, exact hca, end -- 3ª demostración example (hR: equivalence R) : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y := begin rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩, apply clases_iguales_si_pertenece hR, apply hR.2.2 _ hcb, apply hR.2.1, exact hca, end -- 4ª demostración lemma clases_disjuntas (hR: equivalence R) : ∀ X Y ∈ clases R, (X ∩ Y : set A).nonempty → X = Y := begin rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩, exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb), end |
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]