ZFC in LEAN 之 等价关系（Equivalence Relation）及前集的等价关系（Equivalence in Pre-Set）

        等价关系（Equivalence Relation）在LEAN中定义十分直接明了，如下图：

        即，当一个定义在类型α上的二元关系 r，满足，自反性，对称性，以及传递性，那么，该二元关系r 为等价关系。

        这里，refl、symm、trans 是上述属性的证明。即，证明该二元关系 r，满足等价关系的三个条件。

        对于前集（Preset）来说，定义两前集等价（或直接称相等），为，第一个前集的任一元素等于第二个前集中的一个元素，以及，第二个前集的任一元素等于第一个前集中的一个元素。

        在LEAN中的定义如下图：

有了此定义后，可以证明该等价关系是，自反的、对称的、传递的，如下图：

其中：Equiv.euc 如下：

        那么，根据数学家 Bishop 对集合的要求，LEAN中，定义了PSet的构建，PSet的相等关系，以及证明了PSet相等关系满足等价关系。那么，就可以基于PSet定义ZFC中的集合。

        后续，就继续分析ZFC中的集合，在LEAN里是如何定义的。