From b1dbb34e1e2388a3987710e128e6f19b7d8fe5fc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 16 Jan 2009 01:37:16 +0000 Subject: [PATCH] Sambin's result holds trivially since most of the fields of the objects of the two categories are definitionally equal! --- .../basic_pairs_to_basic_topologies.ma | 43 +++++++++++++++++++ .../contribs/formal_topology/overlap/depends | 1 + 2 files changed, 44 insertions(+) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma 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 -- 2.39.2