helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_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 "o-basic_pairs.ma".
  16 include "o-basic_topologies.ma".
  17
  18
  19
  20 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
  21 definition o_basic_topology_of_o_basic_pair: BP → BTop.
  22  intro t;
  23  constructor 1;
  24   [ apply (form t);
  25   | apply (□_t ∘ Ext⎽t);
  26   | apply (◊_t ∘ Rest⎽t);
  27   | intros 2; split; intro;
  28      [ change with ((⊩) \sup ⎻* ((⊩) \sup ⎻ U) ≤ (⊩) \sup ⎻* ((⊩) \sup ⎻ V));
  29        apply (. (#‡(lemma_10_4_a ?? (⊩) V)^-1));
  30        apply f_minus_star_image_monotone;
  31        apply f_minus_image_monotone;
  32        assumption
  33      | apply oa_leq_trans;
  34         [3: apply f;
  35         | skip
  36         | change with (U ≤ (⊩)⎻* ((⊩)⎻ U));
  37           apply (. (or_prop2 : ?) ^ -1);
  38           apply oa_leq_refl; ]]
  39   | intros 2; split; intro;
  40      [ change with (◊_t ((⊩) \sup * U) ≤ ◊_t ((⊩) \sup * V));
  41        apply (. ((lemma_10_4_b ?? (⊩) U)^-1)‡#);
  42        apply (f_image_monotone ?? (⊩) ? ((⊩)* V));
  43        apply f_star_image_monotone;
  44        assumption;
  45      | apply oa_leq_trans;
  46         [2: apply f;
  47         | skip
  48         | change with ((⊩) ((⊩)* V) ≤ V);
  49           apply (. (or_prop1 : ?));
  50           apply oa_leq_refl; ]]
  51   | intros;
  52     apply (.= (oa_overlap_sym' : ?));
  53     change with ((◊_t ((⊩)* V) >< (⊩)⎻* ((⊩)⎻ U)) = (U >< (◊_t ((⊩)* V))));
  54     apply (.= (or_prop3 ?? (⊩) ((⊩)* V) ?));
  55     apply (.= #‡(lemma_10_3_a : ?));
  56     apply (.= (or_prop3 : ?)^-1);
  57     apply (oa_overlap_sym' ? ((⊩) ((⊩)* V)) U); ]
  58 qed.
  59
  60 definition o_continuous_relation_of_o_relation_pair:
  61  ∀BP1,BP2.arrows2 BP BP1 BP2 →
  62   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
  63  intros (BP1 BP2 t);
  64  constructor 1;
  65   [ apply (t \sub \f);
  66   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  67     apply sym1;
  68     unfold in ⊢ (? ? ? (? ? ? ? %) ?);
  69     apply (.= †(†e));
  70     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
  71     cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
  72       cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
  73     apply (.= †COM);
  74     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
  75     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
  76     apply (.= COM ^ -1);
  77     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
  78     change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
  79     unfold in ⊢ (? ? ? % %); apply (†e^-1);
  80   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
  81     apply sym1;
  82     unfold in ⊢ (? ? ? (? ? ? ? %) ?);
  83     apply (.= †(†e));
  84     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
  85     cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
  86       cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
  87     apply (.= †COM);
  88     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
  89     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
  90     apply (.= COM ^ -1);
  91     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
  92     change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
  93     unfold in ⊢ (? ? ? % %); apply (†e^-1);]
  94 qed.