include "o-basic_pairs.ma".
include "o-basic_topologies.ma".
+alias symbol "eq" = "setoid1 eq".
+
(* qui la notazione non va *)
-lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = binary_join ? p q.
+lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
intros;
apply oa_leq_antisym;
[ apply oa_density; intros;
| apply lemma_10_2_c; ]
qed.
+lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
+ intros; apply oa_leq_antisym;
+ [ apply lemma_10_2_d;
+ | apply f_image_monotone;
+ apply (lemma_10_2_c ?? R p); ]
+qed.
+
+lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
+ intros; apply oa_leq_antisym;
+ [ apply f_minus_star_image_monotone;
+ apply (lemma_10_2_b ?? R p);
+ | apply lemma_10_2_a; ]
+qed.
+
lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_a ?? R p)); [2: apply (R⎻* ); | skip | apply Hletin ]
+ intros; apply (†(lemma_10_3_a ?? R p));
qed.
-(* VEERY BAD! *)
-axiom lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
-(*
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_b ?? R p)); [2: apply rule R; | skip | apply Hletin ]
-qed. *)
+lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
+intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p));
+qed.
lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
intros; split; intro; apply oa_overlap_sym; assumption.
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
definition o_basic_topology_of_o_basic_pair: BP → BTop.
- intro;
+ intro t;
constructor 1;
[ apply (form t);
| apply (□_t ∘ Ext⎽t);
definition o_continuous_relation_of_o_relation_pair:
∀BP1,BP2.arrows2 BP BP1 BP2 →
arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
- intros;
+ intros (BP1 BP2 t);
constructor 1;
[ apply (t \sub \f);
| unfold o_basic_topology_of_o_basic_pair; simplify; intros;
- lapply (.= †e); [3: apply rule t \sub \f; |4: apply Hletin; |1,2: skip]
- cut ((t \sub \f ∘ (⊩)) ∘ (⊩)* = ?);
- [
-
- lapply (Hcut U); apply Hletin;
- whd in Hcut;: apply rule (rel BP2);
-
- generalize in match U; clear e;
- change with (t \sub \f ((⊩) ((⊩)* U)) =(⊩) ((⊩)* (t \sub \f U)));
- change in ⊢ (? ? ? % ?) with ((t \sub \f ∘ ((⊩) ∘ (⊩)* )) U);
-
-
+ apply sym1;
+ unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+ apply (.= †(†e));
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
+ cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
+ cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+ apply (.= †COM);
+ change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
+ apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
+ apply (.= COM ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
+ change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
+ unfold in ⊢ (? ? ? % %); apply (†e^-1);
| unfold o_basic_topology_of_o_basic_pair; simplify; intros;
- lapply (.= †e); [3: apply rule (t \sub \f ⎻* ); |4: apply Hletin; |1,2: skip]
- change with (t \sub \f ⎻* ((⊩)⎻* ((⊩)⎻ U)) = (⊩)⎻* ((⊩)⎻ (t \sub \f⎻* U)));
-
- ]
+ apply sym1;
+ unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+ apply (.= †(†e));
+ change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
+ cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
+ cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+ apply (.= †COM);
+ change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
+ apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
+ apply (.= COM ^ -1);
+ change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
+ change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
+ unfold in ⊢ (? ? ? % %); apply (†e^-1);]
qed.
\ No newline at end of file