From 2dc6ec0db2156431948014a6498c9901f8759e39 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Aug 2009 08:29:25 +0000 Subject: [PATCH] ... --- .../matita/nlibrary/sets/partitions.ma | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index e588fd2bc..6b81ce60b 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -19,6 +19,7 @@ include "nat/minus.ma". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". +alias symbol "eq" = "setoid eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -58,4 +59,21 @@ nlemma partition_splits_card: | #x; #x'; nnormalize in ⊢ (? → ? → %); nelim daemon ] +nqed. + +(************** equivalence relations vs partitions **********************) + +ndefinition partition_of_compatible_equivalence_relation: + ∀A:setoid. compatible_equivalence_relation A → partition A. + #A; #R; napply mk_partition + [ napply (quotient ? R) + | napply Full_set + | #a; napply mk_qpowerclass + [ napply {x | R x a} + | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon] +##| #x; #_; nnormalize; napply (ex_intro … x); napply conj; napply refl + | #x; #x'; #_; #_; nnormalize; *; #x''; *; #H1; #H2; napply (trans ?????? H2); + napply sym; nassumption + | nnormalize; napply conj + [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##] nqed. \ No newline at end of file -- 2.39.2