Particiones – Calculemus

Isomorfismo entre relaciones de equivalencia y particiones

PorJosé A. Alonso 15 octubre 20214 octubre 2021

Este ejercicio es el 16º 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.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
11. Las relaciones definidas por particiones son simétricas.
12. Las relaciones definidas por particiones son transitivas.
13. Aplicación de particiones en relaciones de equivalencia.
14. La función relacionP es inversa por la izquierda de la función cociente
15. La función relacionP es inversa por la derecha de la función cociente.

En Lean, el tipo de los isomorfimos de un tipo α en un tipo β está definido mediante la siguiente estructura

   structure equiv (α : Sort*) (β : Sort*) :=
   (to_fun    : α → β)
   (inv_fun   : β → α)
   (left_inv  : left_inverse inv_fun to_fun)
   (right_inv : right_inverse inv_fun to_fun)

structure equiv (α : Sort*) (β : Sort*) :=

(to_fun : α → β)

(inv_fun : β → α)

(left_inv : left_inverse inv_fun to_fun)

(right_inv : right_inverse inv_fun to_fun)

y se equiv α β se denota por α ≃ β. Por tanto, para demostrar que los dos tipos don isomorfos hay que definir dos funciones entre ellos y demostrar que una es la inversa de la otra.

Demostrar que los tipos de las relaciones de equivalencia sobre A y el de las particiones de A son isomorfos.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}
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}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_izq :
  function.left_inverse relacionP (@cociente A) :=
begin
  rintro ⟨R, hR⟩,
  simp [relacionP, cociente],
  ext a b,
  exact ⟨λ hab, hR.2.1 (hab a (hR.1 a)),
         λ hab c hac, hR.2.2 (hR.2.1 hab) hac⟩,
end

lemma inversa_dcha :
  function.right_inverse relacionP (@cociente A) :=
begin
  intro P,
  ext X,
  show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P,
  split,
  { rintro ⟨a, rfl⟩,
    obtain ⟨X, hX, haX⟩ := Hrecubren P a,
    convert hX,
    ext b,
    rw pertenece_clase_syss,
    split,
    { intro hba,
      obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,
      specialize hba Y hY hbY,
      convert hbY,
      exact iguales_si_comun hX hY haX hba, },
    { intros hbX Y hY hbY,
      apply pertenece_si_pertenece hX hY hbX hbY haX, }},
  { intro hX,
    rcases Hno_vacios P X hX with ⟨a, ha⟩,
    use a,
    ext b,
    split,
    { intro hbX,
      rw pertenece_clase_syss,
      intros Y hY hbY,
      exact pertenece_si_pertenece hX hY hbX hbY ha, },
    { rw pertenece_clase_syss,
      intro hba,
      obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,
      specialize hba Y hY hbY,
      exact pertenece_si_pertenece hY hX hba ha hbY, }}
end

theorem equivalencia_particiones
  (A : Type)
  : {R : A → A → Prop // equivalence R} ≃ particion A :=
sorry

end particion

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

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}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_izq :

function.left_inverse relacionP (@cociente A) :=

begin

rintro ⟨R, hR⟩,

simp [relacionP, cociente],

ext a b,

exact ⟨λ hab, hR.2.1 (hab a (hR.1 a)),

λ hab c hac, hR.2.2 (hR.2.1 hab) hac⟩,

end

lemma inversa_dcha :

function.right_inverse relacionP (@cociente A) :=

begin

intro P,

ext X,

show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P,

split,

{ rintro ⟨a, rfl⟩,

obtain ⟨X, hX, haX⟩ := Hrecubren P a,

convert hX,

ext b,

rw pertenece_clase_syss,

split,

{ intro hba,

obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,

specialize hba Y hY hbY,

convert hbY,

exact iguales_si_comun hX hY haX hba, },

{ intros hbX Y hY hbY,

apply pertenece_si_pertenece hX hY hbX hbY haX, }},

{ intro hX,

rcases Hno_vacios P X hX with ⟨a, ha⟩,

use a,

ext b,

split,

{ intro hbX,

rw pertenece_clase_syss,

intros Y hY hbY,

exact pertenece_si_pertenece hX hY hbX hbY ha, },

{ rw pertenece_clase_syss,

intro hba,

obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,

specialize hba Y hY hbY,

exact pertenece_si_pertenece hY hX hba ha hbY, }}

end

theorem equivalencia_particiones

(A : Type)

: {R : A → A → Prop // equivalence R} ≃ particion A :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}
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}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_izq :
  function.left_inverse relacionP (@cociente A) :=
begin
  rintro ⟨R, hR⟩,
  simp [relacionP, cociente],
  ext a b,
  exact ⟨λ hab, hR.2.1 (hab a (hR.1 a)),
         λ hab c hac, hR.2.2 (hR.2.1 hab) hac⟩,
end

lemma inversa_dcha :
  function.right_inverse relacionP (@cociente A) :=
begin
  intro P,
  ext X,
  show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P,
  split,
  { rintro ⟨a, rfl⟩,
    obtain ⟨X, hX, haX⟩ := Hrecubren P a,
    convert hX,
    ext b,
    rw pertenece_clase_syss,
    split,
    { intro hba,
      obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,
      specialize hba Y hY hbY,
      convert hbY,
      exact iguales_si_comun hX hY haX hba, },
    { intros hbX Y hY hbY,
      apply pertenece_si_pertenece hX hY hbX hbY haX, }},
  { intro hX,
    rcases Hno_vacios P X hX with ⟨a, ha⟩,
    use a,
    ext b,
    split,
    { intro hbX,
      rw pertenece_clase_syss,
      intros Y hY hbY,
      exact pertenece_si_pertenece hX hY hbX hbY ha, },
    { rw pertenece_clase_syss,
      intro hba,
      obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,
      specialize hba Y hY hbY,
      exact pertenece_si_pertenece hY hX hba ha hbY, }}
end

theorem equivalencia_particiones
  (A : Type)
  : {R : A → A → Prop // equivalence R} ≃ particion A :=
{ to_fun    := cociente,
  inv_fun   := relacionP,
  left_inv  := inversa_izq,
  right_inv := inversa_dcha, }

end particion

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

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}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_izq :

function.left_inverse relacionP (@cociente A) :=

begin

rintro ⟨R, hR⟩,

simp [relacionP, cociente],

ext a b,

exact ⟨λ hab, hR.2.1 (hab a (hR.1 a)),

λ hab c hac, hR.2.2 (hR.2.1 hab) hac⟩,

end

lemma inversa_dcha :

function.right_inverse relacionP (@cociente A) :=

begin

intro P,

ext X,

show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P,

split,

{ rintro ⟨a, rfl⟩,

obtain ⟨X, hX, haX⟩ := Hrecubren P a,

convert hX,

ext b,

rw pertenece_clase_syss,

split,

{ intro hba,

obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,

specialize hba Y hY hbY,

convert hbY,

exact iguales_si_comun hX hY haX hba, },

{ intros hbX Y hY hbY,

apply pertenece_si_pertenece hX hY hbX hbY haX, }},

{ intro hX,

rcases Hno_vacios P X hX with ⟨a, ha⟩,

use a,

ext b,

split,

{ intro hbX,

rw pertenece_clase_syss,

intros Y hY hbY,

exact pertenece_si_pertenece hX hY hbX hbY ha, },

{ rw pertenece_clase_syss,

intro hba,

obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,

specialize hba Y hY hbY,

exact pertenece_si_pertenece hY hX hba ha hbY, }}

end

theorem equivalencia_particiones

(A : Type)

: {R : A → A → Prop // equivalence R} ≃ particion A :=

{ to_fun := cociente,

inv_fun := relacionP,

left_inv := inversa_izq,

right_inv := inversa_dcha, }

end particion

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]

La función `relacionP` es inversa por la derecha de la función `cociente`

PorJosé A. Alonso 14 octubre 20214 octubre 2021

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

En los ejercicios 9 y 13 se han definido las funciones

   cociente : {R : A → A → Prop // equivalence R} → particion A
   relacionP : particion A → {R : A → A → Prop // equivalence R}

1 2	cociente : {R : A → A → Prop // equivalence R} → particion A relacionP : particion A → {R : A → A → Prop // equivalence R}

tales que
+ cociente R es el conjunto cociente de la relación de equivalencia R y
+ relacionP P es la relación de equivalencia definida por la partición P de forma que los elementos relacionados son los que pertenecen a los mismos bloques de P.

Demostrar que relacionP es inversa por la derecha de cociente.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}
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}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_dcha :
  function.right_inverse relacionP (@cociente A) :=
sorry

end particion

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

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}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_dcha :

function.right_inverse relacionP (@cociente A) :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}
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}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

-- 1ª demostración
example :
  function.right_inverse relacionP (@cociente A) :=
begin
  unfold function.right_inverse,
  unfold function.left_inverse,
  intro P,
  ext X,
  simp [cociente],
  split,
  { intro h,
    cases h with a ha,
    rw ha,
    rcases Hrecubren P a with ⟨X, hX, haX⟩,
    convert hX,
    ext b,
    rw pertenece_clase_syss,
    split,
    { intro hba,
      rcases Hrecubren P b with ⟨Y, hY, hbY⟩,
      specialize hba Y hY hbY,
      convert hbY,
      exact iguales_si_comun hX hY haX hba, },
    { intros hbX Y hY hbY,
      apply pertenece_si_pertenece hX hY hbX hbY haX, }},
  { intro hX,
    rcases Hno_vacios P X hX with ⟨a, ha⟩,
    use a,
    ext b,
    split,
    { intro hbX,
      rw pertenece_clase_syss,
      intros Y hY hbY,
      exact pertenece_si_pertenece hX hY hbX hbY ha, },
    { rw pertenece_clase_syss,
      intro hba,
      rcases Hrecubren P b with ⟨Y, hY, hbY⟩,
      specialize hba Y hY hbY,
      exact pertenece_si_pertenece hY hX hba ha hbY, }}
end

-- 2ª demostración
lemma inversa_dcha :
  function.right_inverse relacionP (@cociente A) :=
begin
  intro P,
  ext X,
  show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P,
  split,
  { rintro ⟨a, rfl⟩,
    obtain ⟨X, hX, haX⟩ := Hrecubren P a,
    convert hX,
    ext b,
    rw pertenece_clase_syss,
    split,
    { intro hba,
      obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,
      specialize hba Y hY hbY,
      convert hbY,
      exact iguales_si_comun hX hY haX hba, },
    { intros hbX Y hY hbY,
      apply pertenece_si_pertenece hX hY hbX hbY haX, }},
  { intro hX,
    rcases Hno_vacios P X hX with ⟨a, ha⟩,
    use a,
    ext b,
    split,
    { intro hbX,
      rw pertenece_clase_syss,
      intros Y hY hbY,
      exact pertenece_si_pertenece hX hY hbX hbY ha, },
    { rw pertenece_clase_syss,
      intro hba,
      obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,
      specialize hba Y hY hbY,
      exact pertenece_si_pertenece hY hX hba ha hbY, }}
end

end particion

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

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}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

-- 1ª demostración

example :

function.right_inverse relacionP (@cociente A) :=

begin

unfold function.right_inverse,

unfold function.left_inverse,

intro P,

ext X,

simp [cociente],

split,

{ intro h,

cases h with a ha,

rw ha,

rcases Hrecubren P a with ⟨X, hX, haX⟩,

convert hX,

ext b,

rw pertenece_clase_syss,

split,

{ intro hba,

rcases Hrecubren P b with ⟨Y, hY, hbY⟩,

specialize hba Y hY hbY,

convert hbY,

exact iguales_si_comun hX hY haX hba, },

{ intros hbX Y hY hbY,

apply pertenece_si_pertenece hX hY hbX hbY haX, }},

{ intro hX,

rcases Hno_vacios P X hX with ⟨a, ha⟩,

use a,

ext b,

split,

{ intro hbX,

rw pertenece_clase_syss,

intros Y hY hbY,

exact pertenece_si_pertenece hX hY hbX hbY ha, },

{ rw pertenece_clase_syss,

intro hba,

rcases Hrecubren P b with ⟨Y, hY, hbY⟩,

specialize hba Y hY hbY,

exact pertenece_si_pertenece hY hX hba ha hbY, }}

end

-- 2ª demostración

lemma inversa_dcha :

function.right_inverse relacionP (@cociente A) :=

begin

intro P,

ext X,

show (∃ (a : A), X = clase _ a) ↔ X ∈ Bloques P,

split,

{ rintro ⟨a, rfl⟩,

obtain ⟨X, hX, haX⟩ := Hrecubren P a,

convert hX,

ext b,

rw pertenece_clase_syss,

split,

{ intro hba,

obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,

specialize hba Y hY hbY,

convert hbY,

exact iguales_si_comun hX hY haX hba, },

{ intros hbX Y hY hbY,

apply pertenece_si_pertenece hX hY hbX hbY haX, }},

{ intro hX,

rcases Hno_vacios P X hX with ⟨a, ha⟩,

use a,

ext b,

split,

{ intro hbX,

rw pertenece_clase_syss,

intros Y hY hbY,

exact pertenece_si_pertenece hX hY hbX hbY ha, },

{ rw pertenece_clase_syss,

intro hba,

obtain ⟨Y, hY, hbY⟩ := Hrecubren P b,

specialize hba Y hY hbY,

exact pertenece_si_pertenece hY hX hba ha hbY, }}

end

end particion

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]

La función `relacionP` es inversa por la izquierda de la función `cociente`

PorJosé A. Alonso 13 octubre 20214 octubre 2021

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

En los ejercicios 9 y 13 se han definido las funciones

   cociente : {R : A → A → Prop // equivalence R} → particion A
   relacionP : particion A → {R : A → A → Prop // equivalence R}

1 2	cociente : {R : A → A → Prop // equivalence R} → particion A relacionP : particion A → {R : A → A → Prop // equivalence R}

tales que

cociente R es el conjunto cociente de la relación de equivalencia R y
relacionP P es la relación de equivalencia definida por la partición P de forma que los elementos relacionados son los que pertenecen a los mismos bloques de P.

Demostrar que relacionP es inversa por la izquierda de cociente.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}
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}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_izq :
  function.left_inverse relacionP (@cociente A) :=
sorry

end particion

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

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}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

lemma inversa_izq :

function.left_inverse relacionP (@cociente A) :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}
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}

lemma pertenece_clase_syss
  {a b : A}
  : b ∈ clase R a ↔ R b a :=
by refl

lemma clases_no_vacias
  (hR: equivalence R)
  : ∀ (X : set A), X ∈ clases R → X.nonempty :=
begin
  rintros _ ⟨a, rfl⟩,
  use a,
  rw pertenece_clase_syss,
  apply hR.1,
end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=
  λ R, { Bloques    := {B : set A | ∃ x : A, B = clase R.1 x},
         Hno_vacios := clases_no_vacias R.1 R.2,
         Hrecubren  := clases_recubren R.1 R.2,
         Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

-- 1ª demostración
example :
  function.left_inverse relacionP (@cociente A) :=
begin
  unfold function.left_inverse,
  intro S,
  cases S with R hR,
  unfold relacionP cociente relacion,
  simp,
  ext a b,
  split,
  { intros hab,
    apply hR.2.1,
    unfold clase at hab,
    dsimp at hab,
    apply hab,
    apply hR.1, },
  { intros hab c hac,
    unfold clase at *,
    dsimp at *,
    apply hR.2.2 (hR.2.1 hab) hac, },
end

-- 2ª demostración
example :
  function.left_inverse relacionP (@cociente A) :=
begin
  rintro ⟨R, hR⟩,
  simp [relacionP, cociente],
  ext a b,
  split,
  { intros hab,
    apply hR.2.1,
    apply hab,
    apply hR.1, },
  { intros hab c hac,
    apply hR.2.2 (hR.2.1 hab) hac, },
end

-- 3ª demostración
example :
  function.left_inverse relacionP (@cociente A) :=
begin
  rintro ⟨R, hR⟩,
  simp [relacionP, cociente],
  ext a b,
  split,
  { intros hab,
    exact hR.2.1 (hab a (hR.1 a)), },
  { intros hab c hac,
    exact hR.2.2 (hR.2.1 hab) hac, },
end

-- 4ª demostración
example :
  function.left_inverse relacionP (@cociente A) :=
begin
  rintro ⟨R, hR⟩,
  simp [relacionP, cociente],
  ext a b,
  split,
  { exact λ hab, hR.2.1 (hab a (hR.1 a)), },
  { exact λ hab c hac, hR.2.2 (hR.2.1 hab) hac, },
end

-- 5ª demostración
lemma inversa_izq :
  function.left_inverse relacionP (@cociente A) :=
begin
  rintro ⟨R, hR⟩,
  simp [relacionP, cociente],
  ext a b,
  exact ⟨λ hab, hR.2.1 (hab a (hR.1 a)),
         λ hab c hac, hR.2.2 (hR.2.1 hab) hac⟩,
end

end particion

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

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}

lemma pertenece_clase_syss

{a b : A}

: b ∈ clase R a ↔ R b a :=

by refl

lemma clases_no_vacias

(hR: equivalence R)

: ∀ (X : set A), X ∈ clases R → X.nonempty :=

begin

rintros _ ⟨a, rfl⟩,

use a,

rw pertenece_clase_syss,

apply hR.1,

end

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

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))

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

def cociente : {R : A → A → Prop // equivalence R} → particion A :=

λ R, { Bloques := {B : set A | ∃ x : A, B = clase R.1 x},

Hno_vacios := clases_no_vacias R.1 R.2,

Hrecubren := clases_recubren R.1 R.2,

Hdisjuntos := clases_disjuntas R.1 R.2, }

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

-- 1ª demostración

example :

function.left_inverse relacionP (@cociente A) :=

begin

unfold function.left_inverse,

intro S,

cases S with R hR,

unfold relacionP cociente relacion,

simp,

ext a b,

split,

{ intros hab,

apply hR.2.1,

unfold clase at hab,

dsimp at hab,

apply hab,

apply hR.1, },

{ intros hab c hac,

unfold clase at *,

dsimp at *,

apply hR.2.2 (hR.2.1 hab) hac, },

end

-- 2ª demostración

example :

function.left_inverse relacionP (@cociente A) :=

begin

rintro ⟨R, hR⟩,

simp [relacionP, cociente],

ext a b,

split,

{ intros hab,

apply hR.2.1,

apply hab,

apply hR.1, },

{ intros hab c hac,

apply hR.2.2 (hR.2.1 hab) hac, },

end

-- 3ª demostración

example :

function.left_inverse relacionP (@cociente A) :=

begin

rintro ⟨R, hR⟩,

simp [relacionP, cociente],

ext a b,

split,

{ intros hab,

exact hR.2.1 (hab a (hR.1 a)), },

{ intros hab c hac,

exact hR.2.2 (hR.2.1 hab) hac, },

end

-- 4ª demostración

example :

function.left_inverse relacionP (@cociente A) :=

begin

rintro ⟨R, hR⟩,

simp [relacionP, cociente],

ext a b,

split,

{ exact λ hab, hR.2.1 (hab a (hR.1 a)), },

{ exact λ hab c hac, hR.2.2 (hR.2.1 hab) hac, },

end

-- 5ª demostración

lemma inversa_izq :

function.left_inverse relacionP (@cociente A) :=

begin

rintro ⟨R, hR⟩,

simp [relacionP, cociente],

ext a b,

exact ⟨λ hab, hR.2.1 (hab a (hR.1 a)),

λ hab c hac, hR.2.2 (hR.2.1 hab) hac⟩,

end

end particion

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]

Aplicación de particiones en relaciones de equivalencia

PorJosé A. Alonso 12 octubre 20214 octubre 2021

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

Definir la función

   relacionP : particion A → {R : A → A → Prop // equivalence R}

1	relacionP : particion A → {R : A → A → Prop // equivalence R}

tal que relacionP P es la relación de equivalencia definida por la partición P.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
sorry

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=
  λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,
        ⟨reflexiva P, simetrica P, transitiva P⟩⟩

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

lemma reflexiva

(P : particion A)

: reflexive (relacion P) :=

λ a X hXC haX, haX

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

def relacionP : particion A → {R : A → A → Prop // equivalence R} :=

λ P, ⟨λ a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X,

⟨reflexiva P, simetrica P, transitiva P⟩⟩

end particion

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]

Las relaciones definidas por particiones son transitivas

PorJosé A. Alonso 11 octubre 20214 octubre 2021

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

Demostrar que la relación definida por una partición es transitiva.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example
  (P : particion A)
  : transitive (relacion P) :=
sorry

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example

(P : particion A)

: transitive (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- 1ª demostración
example
  (P : particion A)
  : transitive (relacion P) :=
begin
  unfold transitive,
  intros a b c hab hbc,
  unfold relacion at *,
  intros X hX haX,
  apply hbc,
  { exact hX, },
  { apply hab,
    { exact hX, },
    { exact haX, }},
end

-- 2ª demostración
example
  (P : particion A)
  : transitive (relacion P) :=
begin
  intros a b c hab hbc,
  intros X hX haX,
  apply hbc X hX,
  apply hab X hX,
  exact haX,
end

-- 3ª demostración
example
  (P : particion A)
  : transitive (relacion P) :=
begin
  intros a b c hab hbc X hX haX,
  exact hbc X hX (hab X hX haX),
end

-- 4ª demostración
lemma transitiva
  (P : particion A)
  : transitive (relacion P) :=
λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- 1ª demostración

example

(P : particion A)

: transitive (relacion P) :=

begin

unfold transitive,

intros a b c hab hbc,

unfold relacion at *,

intros X hX haX,

apply hbc,

{ exact hX, },

{ apply hab,

{ exact hX, },

{ exact haX, }},

end

-- 2ª demostración

example

(P : particion A)

: transitive (relacion P) :=

begin

intros a b c hab hbc,

intros X hX haX,

apply hbc X hX,

apply hab X hX,

exact haX,

end

-- 3ª demostración

example

(P : particion A)

: transitive (relacion P) :=

begin

intros a b c hab hbc X hX haX,

exact hbc X hX (hab X hX haX),

end

-- 4ª demostración

lemma transitiva

(P : particion A)

: transitive (relacion P) :=

λ a b c hab hbc X hX haX, hbc X hX (hab X hX haX)

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]

Las relaciones definidas por particiones son simétricas

PorJosé A. Alonso 10 octubre 20213 octubre 2021

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

Demostrar que la relación definida por una partición es simétrica.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example
  (P : particion A)
  : symmetric (relacion P) :=
sorry

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

example

(P : particion A)

: symmetric (relacion P) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variables {X Y : set A}
variable  {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=
  λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- Se usarán los siguientes lemas auxiliares

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

-- 1ª demostración
example
  (P : particion A)
  : symmetric (relacion P) :=
begin
  rw symmetric,
  intros a b hab,
  unfold relacion at *,
  intros X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize hab Y hY haY,
  exact pertenece_si_pertenece hY hX hab hbX haY,
end

-- 2ª demostración
example
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b hab,
  intros X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize hab Y hY haY,
  exact pertenece_si_pertenece hY hX hab hbX haY,
end

-- 3ª demostración
lemma simetrica
  (P : particion A)
  : symmetric (relacion P) :=
begin
  intros a b h X hX hbX,
  obtain ⟨Y, hY, haY⟩ := Hrecubren P a,
  specialize h Y hY haY,
  exact pertenece_si_pertenece hY hX h hbX haY,
end

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variables {X Y : set A}

variable {P : particion A}

def relacion : (particion A) → (A → A → Prop) :=

λ P a b, ∀ X ∈ Bloques P, a ∈ X → b ∈ X

-- Se usarán los siguientes lemas auxiliares

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

-- 1ª demostración

example

(P : particion A)

: symmetric (relacion P) :=

begin

rw symmetric,

intros a b hab,

unfold relacion at *,

intros X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize hab Y hY haY,

exact pertenece_si_pertenece hY hX hab hbX haY,

end

-- 2ª demostración

example

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b hab,

intros X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize hab Y hY haY,

exact pertenece_si_pertenece hY hX hab hbX haY,

end

-- 3ª demostración

lemma simetrica

(P : particion A)

: symmetric (relacion P) :=

begin

intros a b h X hX hbX,

obtain ⟨Y, hY, haY⟩ := Hrecubren P a,

specialize h Y hY haY,

exact pertenece_si_pertenece hY hX h hbX haY,

end

end particion

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]

Pertenencia a bloques de una partición con elementos comunes

PorJosé A. Alonso 1 octubre 20212 octubre 2021

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

El anterior es Igualdad de bloques de una partición cuando tienen elementos comunes.

El ejercicio consiste en demostrar que si dos bloques de una partición tienen elementos comunes, entonces los elementos de uno también pertenecen al otro.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
sorry

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

-- 1ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  apply iguales_si_comun hY hX haY,
  exact haX,
end

-- 2ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  have hXY : X = Y := iguales_si_comun hX hY haX haY,
  rw ← hXY,
  exact hbX,
end

-- 3ª demostración
lemma pertenece_si_pertenece
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a b : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  (hbX : b ∈ X)
  : b ∈ Y :=
begin
  convert hbX,
  exact iguales_si_comun hY hX haY haX,
end

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

-- 1ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

apply iguales_si_comun hY hX haY,

exact haX,

end

-- 2ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

have hXY : X = Y := iguales_si_comun hX hY haX haY,

rw ← hXY,

exact hbX,

end

-- 3ª demostración

lemma pertenece_si_pertenece

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a b : A}

(haX : a ∈ X)

(haY : a ∈ Y)

(hbX : b ∈ X)

: b ∈ Y :=

begin

convert hbX,

exact iguales_si_comun hY hX haY haX,

end

end particion

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]

Igualdad de bloques de una partición cuando tienen elementos comunes

PorJosé A. Alonso 30 septiembre 202130 septiembre 2021

Este ejercicio es el primero 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. El desarrollo de dicha serie está basado en la cuarta parte de la primera sesión del curso de Kevin Buzzard Formalising mathematics: workshop 1 — logic, sets, functions, relations.

Una partición de un conjunto A es un conjunto de subconjuntos no vacíos de A tal que todo elemento de A está exactamente en uno de dichos subconjuntos. Es decir, una famila de conjuntos C es una partición de A si se verifican las siguientes condiciones:

Los conjuntos de C son no vacíos; es decir,

     ∀ X ∈ C, X ≠ ∅.

1	∀ X ∈ C, X ≠ ∅.

Los conjuntos de C recubren A; es decir,

     ∀ a ∈ A, ∃ X ∈ C, a ∈ X

1	∀ a ∈ A, ∃ X ∈ C, a ∈ X

Los conjuntos de C son disjuntos entre sí; es decir,

     ∀ X Y ∈ C, X ∩ Y ≠ ∅ → X = Y

1	∀ X Y ∈ C, X ∩ Y ≠ ∅ → X = Y

En Lean, se puede definir el tipo de las particiones sobre un tipo A mediante una estructura con 4 campos:

Un conjunto de subconjuntos de A llamados los bloques de la partición.
Una prueba de que los bloques son no vacíos.
Una prueba de que cada término de tipo A está en uno de los bloques.
Una prueba de que dos bloques con intersección no vacía son iguales.

Su definición es

    @[ext] structure particion (A : Type) :=
    (Bloques    : set (set A))
    (Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
    (Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
    (Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

Con la definición anterior,

P : particion A expresa que P es una partición de A.
Bloques P es el conjunto de los bloque de P.
Hno_vacios P prueba que los bloques de P son no vacíos.
Hrecubren P prueba que los bloque de P recubren a A.
Hdisjuntos P prueba que los bloques de P son disjuntos entre sí

Demostrar que si dos bloques de una partición tienen un elemento en común, entonces son iguales.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
sorry

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

-- 1ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { rw set.nonempty_def,
    use a,
    split,
    { exact haX, },
    { exact haY, }},
end

-- 2ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { use a,
    exact ⟨haX, haY⟩, },
end

-- 3ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { exact ⟨a, haX, haY⟩, },
end

-- 4ª demostración
lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

-- 1ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

begin

apply P.Hdisjuntos,

{ exact hX, },

{ exact hY, },

{ rw set.nonempty_def,

use a,

split,

{ exact haX, },

{ exact haY, }},

end

-- 2ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

begin

apply P.Hdisjuntos,

{ exact hX, },

{ exact hY, },

{ use a,

exact ⟨haX, haY⟩, },

end

-- 3ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

begin

apply P.Hdisjuntos,

{ exact hX, },

{ exact hY, },

{ exact ⟨a, haX, haY⟩, },

end

-- 4ª demostración

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

end particion

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]