From fc577dad1529b2d90c40dad8e6e3429281107c99 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 16 Jan 2009 01:19:23 +0000 Subject: [PATCH] basic topologies are trivially o-basic topologies the same for their morphisms --- .../basic_topologies_to_o-basic_topologies.ma | 13 ++++++------- .../matita/contribs/formal_topology/overlap/depends | 10 +++++----- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma index 282519dc7..6b6469f27 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies_to_o-basic_topologies.ma @@ -16,11 +16,10 @@ include "basic_topologies.ma". include "o-basic_topologies.ma". include "relations_to_o-algebra.ma". -(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic_topologies/basic_topology.ind#xpointer(1/1) → basic_topology. intro; constructor 1; - [ apply (SUBSETS (carrbt b)); + [ apply (SUBSETS b); | apply (A b); | apply (J b); | apply (A_is_saturation b); @@ -28,12 +27,12 @@ definition o_basic_topology_of_basic_topology: cic:/matita/formal_topology/basic | apply (compatibility b); ] qed. -definition o_relation_pair_of_relation_pair: - ∀S,T.cic:/matita/formal_topology/basic_topologies/continuous_relation.ind#xpointer(1/1) S T → - continuous_relation (o_basic_topology_of_basic_topology S) (o_basic_topology_of_basic_topology T). +definition o_continuous_relation_of_continuous_relation: + ∀BT1,BT2.cic:/matita/formal_topology/basic_topologies/continuous_relation.ind#xpointer(1/1) BT1 BT2 → + continuous_relation (o_basic_topology_of_basic_topology BT1) (o_basic_topology_of_basic_topology BT2). intros; constructor 1; - [ apply (orelation_of_relation ?? (cont_rel ?? c)); + [ apply (orelation_of_relation ?? c); | apply (reduced ?? c); | apply (saturated ?? c); ] -qed. \ No newline at end of file +qed. diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 63392b5b3..8b334f1f6 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -1,22 +1,22 @@ o-basic_pairs.ma o-algebra.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma -saturations.ma relations.ma basic_pairs.ma relations.ma +saturations.ma relations.ma o-algebra.ma categories.ma o-formal_topologies.ma o-basic_topologies.ma -formal_topologies.ma basic_topologies.ma categories.ma cprop_connectives.ma +formal_topologies.ma basic_topologies.ma saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma -basic_topologies.ma relations.ma saturations.ma subsets.ma categories.ma +basic_topologies.ma relations.ma saturations.ma concrete_spaces.ma basic_pairs.ma relations.ma subsets.ma concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma -basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma +basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma cprop_connectives.ma logic/connectives.ma relations_to_o-algebra.ma o-algebra.ma relations.ma -o-basic_pairs_to_o-basic_topologies.ma concrete_spaces.ma o-basic_pairs.ma o-basic_topologies.ma +o-basic_pairs_to_o-basic_topologies.ma o-basic_pairs.ma o-basic_topologies.ma logic/connectives.ma -- 2.39.2