From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 16 Jan 2009 01:37:16 +0000 (+0000)
Subject: Sambin's result holds trivially since most of the fields of the objects of
X-Git-Tag: make_still_working~4249
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b1dbb34e1e2388a3987710e128e6f19b7d8fe5fc;p=helm.git

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
index 000000000..576fa5ea1
--- /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 8b334f1f6..58e985939 100644
--- 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