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 lemma pippo: ∀S:OA.∀p,q,r:S. p ≤ q → p >< r → q >< r.
  19  intros;
  20  cut (r = binary_meet ? r r); (* la notazione non va ??? *)
  21   [ apply (. (#‡Hcut));
  22     apply oa_overlap_preservers_meet;
  23   |
  24   ]
  25
  26 (* Part of proposition 9.9 *)
  27 lemma lemmax: ∀S,T.∀R:arrows2 OA S T.∀p,q. p ≤ q → R p ≤ R q.
  28  intros;
  29  apply oa_density; intros;
  30  apply (. (or_prop3 : ?) ^ -1);
  31  apply
  32
  33 (* Lemma 10.2, to be moved to OA *)
  34 lemma lemma_10_2_a: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R⎻* (R⎻ p).
  35  intros;
  36  apply (. (or_prop2 : ?));
  37  apply oa_leq_refl.
  38 qed.
  39
  40 lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
  41  intros;
  42  apply (. (or_prop2 : ?) ^ -1);
  43  apply oa_leq_refl.
  44 qed.
  45
  46 lemma lemma_10_3: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
  47  intros; apply oa_leq_antisym;
  48   [ lapply (lemma_10_2_b ?? R p);
  49
  50   | apply lemma_10_2_a;]
  51 qed.
  52
  53
  54
  55 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
  56 definition o_basic_topology_of_basic_pair: BP → BTop.
  57  intro;
  58  constructor 1;
  59   [ apply (form t);
  60   | apply (□_t ∘ Ext⎽t);
  61   | apply (◊_t ∘ Rest⎽t);
  62   | intros 2;
  63     lapply depth=0 (or_prop1 ?? (rel t));
  64     lapply depth=0 (or_prop2 ?? (rel t));
  65
  66   |
  67   |
  68   ]
  69 qed.
  70
  71 definition o_convergent_relation_pair_of_convergent_relation_pair:
  72  ∀BP1,BP2.cic:/matita/formal_topology/concrete_spaces/convergent_relation_pair.ind#xpointer(1/1) BP1 BP2 →
  73   convergent_relation_pair (o_concrete_space_of_concrete_space BP1) (o_concrete_space_of_concrete_space BP2).
  74  intros;
  75  constructor 1;
  76   [ apply (orelation_of_relation ?? (r \sub \c));
  77   | apply (orelation_of_relation ?? (r \sub \f));
  78   | lapply (commute ?? r);
  79     lapply (orelation_of_relation_preserves_equality ???? Hletin);
  80     apply (.= (orelation_of_relation_preserves_composition (concr BP1) ??? (rel BP2)) ^ -1);
  81     apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
  82     apply (orelation_of_relation_preserves_composition ?? (form BP2)  (rel BP1) ?); ]
  83 qed.