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 "o-basic_pairs.ma".
16 include "o-basic_topologies.ma".
18 (* qui la notazione non va *)
19 lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = binary_join ? p q.
22 [ apply oa_density; intros;
24 unfold binary_join; simplify;
25 apply (. (oa_join_split : ?));
26 exists; [ apply false ]
29 | unfold binary_join; simplify;
30 apply (. (oa_join_sup : ?)); intro;
31 cases i; whd in ⊢ (? ? ? ? ? % ?);
32 [ assumption | apply oa_leq_refl ]]
35 lemma overlap_monotone_left: ∀S:OA.∀p,q,r:S. p ≤ q → p >< r → q >< r.
37 apply (. (leq_to_eq_join : ?)‡#);
40 | apply oa_overlap_sym;
41 unfold binary_join; simplify;
42 apply (. (oa_join_split : ?));
48 (* Part of proposition 9.9 *)
49 lemma f_minus_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R⎻ p ≤ R⎻ q.
51 apply (. (or_prop2 : ?));
52 apply oa_leq_trans; [2: apply f; | skip | apply (. (or_prop2 : ?)^ -1); apply oa_leq_refl;]
55 (* Part of proposition 9.9 *)
56 lemma f_minus_star_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R⎻* p ≤ R⎻* q.
58 apply (. (or_prop2 : ?)^ -1);
59 apply oa_leq_trans; [3: apply f; | skip | apply (. (or_prop2 : ?)); apply oa_leq_refl;]
62 (* Part of proposition 9.9 *)
63 lemma f_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R p ≤ R q.
65 apply (. (or_prop1 : ?));
66 apply oa_leq_trans; [2: apply f; | skip | apply (. (or_prop1 : ?)^ -1); apply oa_leq_refl;]
69 (* Part of proposition 9.9 *)
70 lemma f_star_image_monotone: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R* p ≤ R* q.
72 apply (. (or_prop1 : ?)^ -1);
73 apply oa_leq_trans; [3: apply f; | skip | apply (. (or_prop1 : ?)); apply oa_leq_refl;]
76 lemma lemma_10_2_a: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R⎻* (R⎻ p).
78 apply (. (or_prop2 : ?)^-1);
82 lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
84 apply (. (or_prop2 : ?));
88 lemma lemma_10_2_c: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R* (R p).
90 apply (. (or_prop1 : ?)^-1);
94 lemma lemma_10_2_d: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* p) ≤ p.
96 apply (. (or_prop1 : ?));
100 lemma lemma_10_3_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
101 intros; apply oa_leq_antisym;
102 [ apply lemma_10_2_b;
103 | apply f_minus_image_monotone;
104 apply lemma_10_2_a; ]
107 lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = R* p.
108 intros; apply oa_leq_antisym;
109 [ apply f_star_image_monotone;
110 apply (lemma_10_2_d ?? R p);
111 | apply lemma_10_2_c; ]
114 lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
115 intros; apply oa_leq_antisym;
116 [ apply lemma_10_2_d;
117 | apply f_image_monotone;
118 apply (lemma_10_2_c ?? R p); ]
121 lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
122 intros; apply oa_leq_antisym;
123 [ apply f_minus_star_image_monotone;
124 apply (lemma_10_2_b ?? R p);
125 | apply lemma_10_2_a; ]
128 lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
131 lapply (†(lemma_10_3_a ?? R p)); [2: apply (R⎻* ); | skip | apply Hletin ]
135 axiom lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
139 lapply (†(lemma_10_3_b ?? R p)); [2: apply rule R; | skip | apply Hletin ]
142 lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
143 intros; split; intro; apply oa_overlap_sym; assumption.
146 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
147 definition o_basic_topology_of_o_basic_pair: BP → BTop.
151 | apply (□_t ∘ Ext⎽t);
152 | apply (◊_t ∘ Rest⎽t);
153 | intros 2; split; intro;
154 [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
155 apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
156 apply f_minus_star_image_monotone;
157 apply f_minus_image_monotone;
159 | apply oa_leq_trans;
162 | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
163 apply (. (or_prop2 : ?) ^ -1);
164 apply oa_leq_refl; ]]
165 | intros 2; split; intro;
166 [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
167 apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
168 apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
169 apply f_star_image_monotone;
171 | apply oa_leq_trans;
174 | change with ((⊩) ((⊩)* V) ≤ V);
175 apply (. (or_prop1 : ?));
176 apply oa_leq_refl; ]]
178 apply (.= (oa_overlap_sym' : ?));
179 change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
180 apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
181 apply (.= #‡(lemma_10_3_a : ?));
182 apply (.= (or_prop3 : ?)^-1);
183 apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
186 definition o_continuous_relation_of_o_relation_pair:
187 ∀BP1,BP2.arrows2 BP BP1 BP2 →
188 arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
192 | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
194 alias symbol "refl" = "refl1".
195 apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); |
196 lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]]
197 change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U));
198 lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f);
199 apply (.= †(Hletin ?)); clear Hletin;
200 change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
202 [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip]
204 change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
205 apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
206 apply (.= Hcut ^ -1);
207 change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
208 apply (prop11 ?? t \sub \f);
210 | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
212 apply (.= †?); [1: apply (t \sub \f⎻* ((((⊩)⎻* ∘ (⊩)⎻) U))); |
213 lapply (†e); [2: apply rule (t \sub \f⎻* ); | skip | apply Hletin]]
214 change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘(⊩)⎻ ) ((t \sub \f⎻* ∘ ((⊩)⎻*∘(⊩)⎻ )) U));
215 lapply (comp_assoc2 ????? (⊩)⎻ (⊩)⎻* t \sub \f⎻* );
216 apply (.= †(Hletin ?)); clear Hletin;
217 change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
219 [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e1 ^ -1 ((⊩)⎻ U));] | 2,4: skip]
221 change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
222 apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
223 apply (.= Hcut ^ -1);
224 change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
225 apply (prop11 ?? t \sub \f⎻* );