]> matita.cs.unibo.it Git - helm.git/commitdiff
The functor from BP to OBP has been defined (but no property proved yet).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Jan 2009 14:10:51 +0000 (14:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Jan 2009 14:10:51 +0000 (14:10 +0000)
helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma

index 071892f6bd3b7605f1892f450bd684915507e333..058176f4ce4556e07a5d10dc08049f05d59948c9 100644 (file)
@@ -203,6 +203,9 @@ definition o_relation_pair_of_relation_pair:
  constructor 1;
   [ apply (orelation_of_relation ?? (r \sub \c));
   | apply (orelation_of_relation ?? (r \sub \f));
-  |
-  ]
+  | lapply (commute ?? r);
+    lapply (orelation_of_relation_preserves_equality ???? Hletin);
+    apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1);
+    apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
+    apply (orelation_of_relation_preserves_composition ?? (form BP2)  (rel BP1) ?); ]
 qed.
\ No newline at end of file