]> matita.cs.unibo.it Git - helm.git/commitdiff
Some progress: everything works well now.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Jan 2009 01:50:28 +0000 (01:50 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Jan 2009 01:50:28 +0000 (01:50 +0000)
helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma

index b13317c67659c3963a9983b9ac3677b54463ad41..4d467fc26fc3853bb0e18f4e09fc9370dbc068ac 100644 (file)
@@ -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).