1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "formal_topology/notation.ma".
16 include "formal_topology/o-basic_pairs.ma".
17 include "formal_topology/o-basic_topologies.ma".
19 alias symbol "eq" = "setoid1 eq".
21 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
22 definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
26 | apply (□⎽t ∘ Ext⎽t);
27 | apply (◊⎽t ∘ Rest⎽t);
28 | apply hide; intros 2; split; intro;
29 [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
30 apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
31 apply f_minus_star_image_monotone;
32 apply f_minus_image_monotone;
37 | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
38 apply (. (or_prop2 : ?) ^ -1);
40 | apply hide; intros 2; split; intro;
41 [ change with (◊⎽t ((⊩) \sup * U) ≤ ◊⎽t ((⊩) \sup * V));
42 apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
43 apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
44 apply f_star_image_monotone;
49 | change with ((⊩) ((⊩)* V) ≤ V);
50 apply (. (or_prop1 : ?));
53 apply (.= (oa_overlap_sym' : ?));
54 change with ((◊⎽t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊⎽t ((⊩)* V))));
55 apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
56 apply (.= #‡(lemma_10_3_a : ?));
57 apply (.= (or_prop3 : ?)^-1);
58 apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
61 definition o_continuous_relation_of_o_relation_pair:
62 ∀BP1,BP2.BP1 ⇒_\obp2 BP2 →
63 (o_basic_topology_of_o_basic_pair BP1) ⇒_\obt2 (o_basic_topology_of_o_basic_pair BP2).
67 | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros (U e);
70 change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U));
71 cut ((t \sub \f ∘ (⊩)) ((⊩\sub BP1)* U) = ((⊩) ∘ t \sub \c) ((⊩\sub BP1)* U)) as COM;[2:
72 cases (Ocommute ?? t); apply (e3 ^ -1 ((⊩\sub BP1)* U));]
74 change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
75 apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩\sub BP1)* U))));
77 change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩\sub BP1)* ) U));
78 change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
80 | apply hide; unfold o_basic_topology_of_o_basic_pair; simplify; intros;
83 change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U));
84 cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩\sub BP1)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩\sub BP1)⎻ U)) as COM;[2:
85 cases (Ocommute ?? t); apply (e1 ^ -1 ((⊩\sub BP1)⎻ U));]
87 change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
88 apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩\sub BP1)⎻ U))));
90 change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩\sub BP1)⎻ ) U));
91 change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
96 definition OR : carr3 (OBP ⇒_\c3 OBTop).
98 [ apply o_basic_topology_of_o_basic_pair;
99 | intros; constructor 1;
100 [ apply o_continuous_relation_of_o_relation_pair;
102 intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
103 change with ((a \sub \f ⎻* ∘ oA (o_basic_topology_of_o_basic_pair S)) =
104 (a' \sub \f ⎻*∘ oA (o_basic_topology_of_o_basic_pair S)));
105 whd in e; cases e; clear e e2 e3 e4;
106 change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
107 apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
108 change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a\sub\f ∘ ⊩\sub S)⎻*;
109 apply (.= #‡†(Ocommute:?)^-1);
111 change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (⊩\sub T ∘ a'\sub\c)⎻*;
112 apply (.= #‡†(Ocommute:?));
113 change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );
114 apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
116 | intros 2 (o a); apply refl1;
117 | intros 6; apply refl1;]