From dba85ad7c7510e7bfd01e5721c63dad528b3e0bf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 6 Jan 2009 14:10:51 +0000 Subject: [PATCH] The functor from BP to OBP has been defined (but no property proved yet). --- .../matita/contribs/formal_topology/overlap/basic_pairs.ma | 7 +++++-- 1 file changed, 5 insertions(+), 2 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 071892f6b..058176f4c 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma @@ -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 -- 2.39.2