Pertenencia a su propia clase de equivalencia

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

En este empezamos con las relaciones de equivalencia, que están definidas en Lean por:

donde A un tipo y R: A → A → Prop es una relación binaria en A.

Además, en Lean se puede definir la clase de equivalencia de un elemento a respecto de una relación de equivalencia R por

Demostrar que cada elemento pertenece a su clase de equivalencia.

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

[expand title=»Soluciones con Lean»]

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]