]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/library/formal_topology/formal_topologies.ma
fork for Matita version B
[helm.git] / matitaB / matita / library / formal_topology / formal_topologies.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "formal_topology/basic_topologies.ma".
16
17 (*
18 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
19  intros; constructor 1;
20   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
21     intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
22     split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
23   | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
24     try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
25 qed.
26
27 interpretation "downarrow" 'downarrow a = (fun_1 ?? (downarrow ?) a).
28
29 definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
30  intros; constructor 1;
31   [ apply (λU,V. ↓U ∩ ↓V);
32   | intros; apply (.= (†H)‡(†H1)); apply refl1]
33 qed.
34
35 interpretation "ffintersects" 'fintersects U V = (fun1 ??? (ffintersects ?) U V).
36
37 record formal_topology: Type ≝
38  { bt:> BTop;
39    converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
40  }.
41
42
43 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
44  intros; constructor 1;
45   [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
46   | intros; apply (.= (†H)‡(†H1)); apply refl1]
47 qed.
48
49 interpretation "ffintersects'" 'fintersects U V = (fun1 ??? (ffintersects' ?) U V).
50
51 record formal_map (S,T: formal_topology) : Type ≝
52  { cr:> continuous_relation_setoid S T;
53    C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
54    C2: extS ?? cr T = S
55  }.
56
57 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
58  intros (S T); constructor 1;
59   [ apply (formal_map S T);
60   | constructor 1;
61      [ apply (λf,f1: formal_map S T.f=f1);
62      | simplify; intros 1; apply refl1
63      | simplify; intros 2; apply sym1
64      | simplify; intros 3; apply trans1]]
65 qed.
66
67 axiom C1':
68  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
69   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
70
71 definition formal_map_composition:
72  ∀o1,o2,o3: formal_topology.
73   binary_morphism1
74    (formal_map_setoid o1 o2)
75    (formal_map_setoid o2 o3)
76    (formal_map_setoid o1 o3).
77  intros; constructor 1;
78   [ intros; whd in c c1; constructor 1;
79      [ apply (comp1 BTop ??? c c1);
80      | intros;
81        apply (.= (extS_com ??? c c1 ?));
82        apply (.= †(C1 ?????));
83        apply (.= (C1' ?????));
84        apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
85        apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
86        apply (.= (extS_singleton ????)‡(extS_singleton ????));
87        apply refl1;
88      | apply (.= (extS_com ??? c c1 ?));
89        apply (.= (†(C2 ???)));
90        apply (.= (C2 ???));
91        apply refl1;]
92   | intros; simplify;
93     change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
94     apply prop1; assumption]
95 qed.
96
97 *)