Sambin's result holds trivially since most of the fields of the objects of

the two categories are definitionally equal!

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
new file mode 100644 (file)
index 0000000..576fa5e
--- /dev/null
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_pairs_to_o-basic_pairs.ma".
+include "o-basic_pairs_to_o-basic_topologies.ma".
+include "basic_pairs.ma".
+include "basic_topologies.ma".
+
+definition basic_topology_of_basic_pair: basic_pair → basic_topology.
+ intro bp;
+ letin obp ≝ (o_basic_pair_of_basic_pair bp);
+ letin obt ≝ (o_basic_topology_of_o_basic_pair obp);
+ constructor 1;
+  [ apply (form bp);
+  | apply (A obt);
+  | apply (J obt);
+  | apply (A_is_saturation obt);
+  | apply (J_is_reduction obt);
+  | apply (compatibility obt); ]
+qed.
+
+definition continuous_relation_of_relation_pair:
+ ∀BP1,BP2.relation_pair BP1 BP2 →
+  continuous_relation (basic_topology_of_basic_pair BP1) (basic_topology_of_basic_pair BP2).
+ intros (BP1 BP2 rp);
+ letin orp ≝ (o_relation_pair_of_relation_pair ?? rp);
+ letin ocr ≝ (o_continuous_relation_of_o_relation_pair ?? orp);
+ constructor 1;
+  [ apply (rp \sub \f);
+  | apply (reduced ?? ocr);
+  | apply (saturated ?? ocr); ]
+qed.
\ No newline at end of file

diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends
index 8b334f1f612f274e8df2117c4b688810774ca3dc..58e985939ec0e3193616722dc241e98e1fdab997 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/depends
+++ b/helm/software/matita/contribs/formal_topology/overlap/depends
@@ -1,4 +1,5 @@
 o-basic_pairs.ma o-algebra.ma
+basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
 o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
 o-saturations.ma o-algebra.ma
 basic_pairs.ma relations.ma