From fd6aeb8cd5ab3859baa1c0ff7274e27dc92a7dc1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 01:50:28 +0000 Subject: [PATCH] Some progress: everything works well now. --- .../formal_topology/overlap/basic_pairs.ma | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma index b13317c67..4d467fc26 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -41,16 +41,25 @@ interpretation "concrete relation" 'concr_rel r = (concr_rel __ r). interpretation "formal relation" 'form_rel r = (form_rel __ r). include "o-basic_pairs.ma". - +(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair. intro; constructor 1; [ apply (SUBSETS (concr b)); | apply (SUBSETS (form b)); - | constructor 1; + | apply (orelation_of_relation ?? (rel b)); ] +qed. + +definition o_relation_pair_of_relation_pair: + ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 → + relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2). + intros; + constructor 1; + [ apply (orelation_of_relation ?? (r \sub \c)); + | apply (orelation_of_relation ?? (r \sub \f)); + | ] qed. - definition relation_pair_equality: ∀o1,o2. equivalence_relation1 (relation_pair o1 o2). -- 2.39.2