From 6e75e2415b0433a134e0050d63d627a66efea7a4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 22 Dec 2008 22:36:20 +0000 Subject: [PATCH] Just copied here from formal_topologies.ma. --- .../contribs/formal_topology/overlap/depends | 1 + .../overlap/o-formal_topologies.ma | 121 ++++++++++++++++++ 2 files changed, 122 insertions(+) create mode 100644 helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends index 0d85e86c2..0032b3151 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/depends +++ b/helm/software/matita/contribs/formal_topology/overlap/depends @@ -2,6 +2,7 @@ o-basic_pairs.ma datatypes/categories.ma o-algebra.ma o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma o-saturations.ma o-algebra.ma o-algebra.ma datatypes/categories.ma logic/cprop_connectives.ma +o-formal_topologies.ma o-concrete_spaces.ma o-basic_topologies.ma o-algebra.ma o-saturations.ma datatypes/categories.ma logic/cprop_connectives.ma diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma new file mode 100644 index 000000000..1693b55f6 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "o-concrete_spaces.ma". + +definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o). + +coercion btop_carr. + +definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o. + +coercion btop_carr'. + +definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S). + intros; constructor 1; + [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)}); + intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w] + split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption + | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split; + try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption] +qed. + +interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a). + +definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S). + intros; constructor 1; + [ apply (λU,V. ↓U ∩ ↓V); + | intros; apply (.= (†H)‡(†H1)); apply refl1] +qed. + +interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V). + +record formal_topology: Type ≝ + { bt:> BTop; + converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V + }. + +definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o. + +coercion bt'. + +definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S). + intros; constructor 1; + [ apply (λb,c:S. (singleton S b) ↓ (singleton S c)); + | intros; apply (.= (†H)‡(†H1)); apply refl1] +qed. + +interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V). + +record formal_map (S,T: formal_topology) : Type ≝ + { cr:> continuous_relation_setoid S T; + C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c; + C2: extS ?? cr T = S + }. + +definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝ + λFT1,FT2,c. cr FT1 FT2 c. + +coercion cr'. + +definition formal_map_setoid: formal_topology → formal_topology → setoid1. + intros (S T); constructor 1; + [ apply (formal_map S T); + | constructor 1; + [ apply (λf,f1: formal_map S T.f=f1); + | simplify; intros 1; apply refl1 + | simplify; intros 2; apply sym1 + | simplify; intros 3; apply trans1]] +qed. + +definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝ + λFT1,FT2,c.cr ?? c. + +coercion cr''. + +definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝ + λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c). + +coercion cr'''. + +axiom C1': + ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T. + extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V. + +definition formal_map_composition: + ∀o1,o2,o3: formal_topology. + binary_morphism1 + (formal_map_setoid o1 o2) + (formal_map_setoid o2 o3) + (formal_map_setoid o1 o3). + intros; constructor 1; + [ intros; whd in c c1; constructor 1; + [ apply (comp1 BTop ??? c c1); + | intros; + apply (.= (extS_com ??? c c1 ?)); + apply (.= †(C1 ?????)); + apply (.= (C1' ?????)); + apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1)))); + apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1); + apply (.= (extS_singleton ????)‡(extS_singleton ????)); + apply refl1; + | apply (.= (extS_com ??? c c1 ?)); + apply (.= (†(C2 ???))); + apply (.= (C2 ???)); + apply refl1;] + | intros; simplify; + change with (comp1 BTop ??? a b = comp1 BTop ??? a' b'); + apply prop1; assumption] +qed. + -- 2.39.2