Menu Close

Día: 9 octubre 2021

Las relaciones definidas por particiones son reflexivas

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

Para cada partición se define una relación de forma que un par de elementos están relacionados si pertenecen al mismo bloque de la partición. En Lean,

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

Demostrar que la relación definida por la partición P es reflexiva.

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 relacion : (particion A)  (A  A  Prop) :=
  λ P a b,  X ∈ Bloques P, a ∈ X  b ∈ X
 
example
  (P : particion A)
  : reflexive (relacion P) :=
sorry
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}
 
def relacion : (particion A)  (A  A  Prop) :=
  λ P a b,  X ∈ Bloques P, a ∈ X  b ∈ X
 
-- 1ª demostración
example
  (P : particion A)
  : reflexive (relacion P) :=
begin
  rw reflexive,
  intro a,
  unfold relacion,
  intros X hXC haX,
  exact haX,
end
 
-- 2ª demostración
example
  (P : particion A)
  : reflexive (relacion P) :=
begin
  intro a,
  intros X hXC haX,
  exact haX,
end
 
-- 3ª demostración
example
  (P : particion A)
  : reflexive (relacion P) :=
begin
  intros a X hXC haX,
  exact haX,
end
 
-- 4ª demostración
lemma reflexiva
  (P : particion A)
  : reflexive (relacion P) :=
λ a X hXC haX, haX
 
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>