From c88511384a331d5583fb665f3f08c731c7ebe036 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Jul 2010 18:48:10 +0000 Subject: [PATCH] ... --- .../overlap/basic_pairs_to_o-basic_pairs.ma | 1 - .../basic_topologies_to_o-basic_topologies.ma | 57 +++++++++++++++++++ 2 files changed, 57 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma index 3e2fe8f35..65709f465 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma @@ -16,7 +16,6 @@ include "basic_pairs.ma". include "o-basic_pairs.ma". include "relations_to_o-algebra.ma". -(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *) definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair. intro b; constructor 1; 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 f00abe8f4..bea3207b6 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 @@ -27,4 +27,61 @@ definition o_continuous_relation_of_continuous_relation: Ocontinuous_relation (o_basic_topology_of_basic_topology BT1) (o_basic_topology_of_basic_topology BT2). intros (BT1 BT2 c); constructor 1; [ apply (orelation_of_relation ?? c) | apply (reduced ?? c) | apply (saturated ?? c) ] +qed. + +axiom daemon: False. + +lemma o_continuous_relation_of_continuous_relation_morphism : + ∀S,T:category2_of_category1 BTop. + unary_morphism2 (arrows2 (category2_of_category1 BTop) S T) + (arrows2 OBTop (o_basic_topology_of_basic_topology S) (o_basic_topology_of_basic_topology T)). +intros (S T); + constructor 1; + [ apply (o_continuous_relation_of_continuous_relation S T); + | cases daemon (*apply (o_relation_pair_of_relation_pair_is_morphism S T)*)] +qed. + +definition BTop_to_OBTop: carr3 (arrows3 CAT2 (category2_of_category1 BTop) OBTop). + constructor 1; + [ apply o_basic_topology_of_basic_topology; + | intros; apply o_continuous_relation_of_continuous_relation_morphism; + | cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_id*); + | cases daemon (*apply o_relation_topology_of_relation_topology_morphism_respects_comp*);] +qed. + +(* +alias symbol "eq" (instance 2) = "setoid1 eq". +alias symbol "eq" (instance 1) = "setoid2 eq". +theorem BTop_to_OBTop_faithful: + ∀S,T.∀f,g:arrows2 (category2_of_category1 BTop) S T. + map_arrows2 ?? BTop_to_OBTop ?? f = map_arrows2 ?? BTop_to_OBTop ?? g → f=g. + intros; change with (∀b.A ? (ext ?? f b) = A ? (ext ?? g b)); + apply (POW_faithful); + apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T)); + apply sym2; + apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) g \sub \c (⊩ \sub T)); + apply sym2; + apply e; +qed. +*) + +include "notation.ma". + +theorem BTop_to_OBTop_full: + ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? BTop_to_OBTop S T g = f). + intros; + cases (POW_full (carrbt S) (carrbt T) (Ocont_rel ?? f)) (g Hg); + exists[ + constructor 1; + [ apply g + | apply hide; intros; lapply (Oreduced ?? f ? e); + cases Hg; lapply (e3 U) as K; apply (.= K); + apply (.= Hletin); apply rule (†(K^-1)); + | apply hide; intros; lapply (Osaturated ?? f ? e); + cases Hg; lapply (e1 U) as K; apply (.= K); + apply (.= Hletin); apply rule (†(K^-1)); + ] + | simplify; unfold BTop_to_OBTop; simplify; + unfold o_continuous_relation_of_continuous_relation_morphism; simplify; + cases Hg; whd; simplify; intro; qed. \ No newline at end of file -- 2.39.2